SCRIPT Analyser is a tool that infers from a given output script the constraints that must be met by an input script to create a valid transaction. Consider for example a standard P2PKH output script, the tool will report that a correct input script must:
- establish a stack containing 2 entries: X_(0) and X_(-1) (with X_(0) at the head of the stack)
- X_(0) must be a correct hash pre-image of the constant value present in the output script
- X_(-1) must be a correct signature (signing the transaction with the private key that belongs to public key X_(0))
The tool can analyse any partial Bitcoin script. That is, it is not limited to the analysis of the standard types of output scripts. The tool supports the entire SCRIPT language (i.e. all operations that are permitted according the Bitcoin Core implementation are supported by this tool).
Try it out online at: https://vm100.cs.stir.ac.uk/~rkl/home.html
Dependency: Haskell's Stack (https://docs.haskellstack.org/en/stable/install_and_upgrade/)
Dependency: swi-prolog (http://www.swi-prolog.org/Download.html)
In the root directory of this repository run:
# If not already installed, install Happy:
stack install happy
# Install Script Analyser and all of its dependencies (other than Happy)
stack install
The executable (SCRIPTAnalyser-exe) can be executed in any directory of this repository through Stack as follows: stack exec SCRIPTAnalyser-exe -- arguments
Call SCRIPTAnalyser-exe, with the output script in stdin, and optionally passing some arguments (call the tool with first argument 'help' for information regarding arguments)
For example, if file scriptA contains an output script (see below for syntax description, or go to https://vm100.cs.stir.ac.uk/~rkl/docu.php), run the following in Bash: stack exec SCRIPTAnalyser-exe -- < scriptA
The same but with more verbose output: stack exec SCRIPTAnalyser-exe -- 2 < scriptA
Some example output scripts can be found in folder scripts/
(Note: this only describes the default verbosity output mode)
For every unique branch of the supplied output script, the tool will print a verdict under a distinct "--- Symbolic evaluation report of execution branch i" section
In this section, the following information is printed:
- The respective branch's decision points are shown (i.e. for every encountered IF operation, is its True branch traversed or is its False branch traversed?)
- The symbolic stack that the input script must supply
- The inferred constraints (on these supplied variables)
- The final resulting symbolic stack (note, at this point we have already performed an additional OP_VERIFY, thus the constraint that the resulting full execution of this branch must end with a true value on the stack is already in the inferred constraints set)
The supported syntax is described below.
Instructions on how to interpret the description:
- The "*" symbol specifies a repeated parsing of 0 or more times
- The "+" symbol specifies a repeated parsing of 1 or more times
- The "|" specifies an or (either parses following the left hand
side or the right hand side)
- The ".." specifies a range of allowed characters.
Any amount of whitespace is allowed between each instruction and between
the PUSH keyword and the subsequent bytestring. Parsing starts by applying
Start rule. Anything after "#" on a line is treated as a comment (similar to how comments work in Bash).\
Start := Instruction*
Instruction := Push | Mnemonic | Byte
Push := "PUSH" Bytestring | "PUSH" Integer
Integer := "i" Num+ | "i-" Num+
Num := "0".."9"
Bytestring := Byte+
Byte := Hexadecimal Hexadecimal
Hexadecimal := "0".."9" | "a".."z" | "A".."Z"
Mnemonic := "OP_0" | "OP_FALSE" | "OP_PUSHDATA1" | "OP_PUSHDATA2"
| "OP_PUSHDATA4" | "OP_1NEGATE" | "OP_RESERVED" | "OP_1"
| "OP_2" | "OP_3" | "OP_4" | "OP_5"
| "OP_6" | "OP_7" | "OP_8" | "OP_9"
| "OP_10" | "OP_11" | "OP_12" | "OP_13"
| "OP_14" | "OP_15" | "OP_16" | "OP_NOP"
| "OP_VER" | "OP_IF" | "OP_NOTIF" | "OP_VERIF"
| "OP_VERNOTIF" | "OP_ELSE" | "OP_ENDIF" | "OP_VERIFY"
| "OP_RETURN" | "OP_TOALTSTACK" | "OP_FROMALTSTACK" | "OP_2DROP"
| "OP_2DUP" | "OP_3DUP" | "OP_2OVER" | "OP_2ROT"
| "OP_2SWAP" | "OP_IFDUP" | "OP_DEPTH" | "OP_DROP"
| "OP_DUP" | "OP_NIP" | "OP_OVER" | "OP_PICK"
| "OP_ROLL" | "OP_ROT" | "OP_SWAP" | "OP_TUCK"
| "OP_CAT" | "OP_SUBSTR" | "OP_LEFT" | "OP_RIGHT"
| "OP_SIZE" | "OP_INVERT" | "OP_AND" | "OP_OR"
| "OP_XOR" | "OP_EQUAL" | "OP_EQUALVERIFY" | "OP_RESERVED1"
| "OP_RESERVED2" | "OP_1ADD" | "OP_1SUB" | "OP_2MUL"
| "OP_2DIV" | "OP_NEGATE" | "OP_ABS" | "OP_NOT"
| "OP_0NOTEQUAL" | "OP_ADD" | "OP_SUB" | "OP_MUL"
| "OP_DIV" | "OP_MOD" | "OP_LSHIFT" | "OP_RSHIFT"
| "OP_BOOLAND" | "OP_BOOLOR" | "OP_NUMEQUAL" | "OP_NUMEQUALVERIFY"
| "OP_NUMNOTEQUAL" | "OP_LESSTHAN" | "OP_GREATERTHAN" | "OP_LESSTHANOREQUAL"
| "OP_GREATERTHANOREQUAL" | "OP_MIN" | "OP_MAX" | "OP_WITHIN"
| "OP_RIPEMD160" | "OP_SHA1" | "OP_SHA256" | "OP_HASH160"
| "OP_HASH256" | "OP_CODESEPARATOR" | "OP_CHECKSIG" | "OP_CHECKSIGVERIFY"
| "OP_CHECKMULTISIG" | "OP_CHECKMULTISIGVERIFY" | "OP_NOP1" | "OP_CHECKLOCKTIMEVERIFY"
| "OP_CHECKSEQUENCEVERIFY" | "OP_NOP4" | "OP_NOP5" | "OP_NOP6"
| "OP_NOP7" | "OP_NOP8" | "OP_NOP9" | "OP_NOP10"