Announcing B'SST: Bitcoin-like Script Symbolic Tracer

Summary:

I have released B'SST: Bitcoin-like Script Symbolic Tracer. It can be found at this GitHub repository: https://github.com/dgpv/bsst. B'SST is a tool that analyzes Bitcoin and Elements scripts by symbolically executing all possible execution paths and tracking the constraints imposed by opcodes on the values they operate on. The tool then generates a report based on this analysis.B'SST can perform analysis with the help of the Z3 theorem prover, which enables the use of features dependent on an SMT solver. However, by default, the analysis does not use Z3, resulting in faster but less thorough analysis. Please refer to the README.md file in the repository (link [0]) for more details on the limitations and caveats of the analysis performed.Compared to the "SCRIPT Analyser" project [2], B'SST aims to closely match the reference interpreter and utilizes an SMT solver instead of Prolog for constraint solving. The reference used for the analysis is the Elements script interpreter [3], which is an extension of the Bitcoin script interpreter.To illustrate the kind of information that the analysis can provide, consider the example script provided: "7 ADD DUP 3 5 WITHIN IF 0x00 ELSE 0 ENDIF EQUALVERIFY 2DUP EQUALVERIFY SUB 0 EQUAL". The analysis report for this script shows that the first branch of the "IF" statement will always fail, the witness 0 must be -7 for the script to succeed, and the possible values for witnesses 1 and 2 are -1. Additionally, the result of the last "EQUAL" operation is always true because it has already been checked by the preceding "EQUALVERIFY" operation. For a more extensive example, please refer to the report [5] for a complex Elements script [4].B'SST also supports plugins to implement custom opcodes. Details on how to implement custom opcodes can be found in the "Custom opcodes" section of the README.md file.Lastly, B'SST is released under the Prosperity Public License 3.0.0, which is a "Free for non-commercial use" license. There is a trial period for commercial use, and exemptions are provided for educational institutions and public research organizations. For more information, please consult the LICENSE.md file in the repository (link [0]).

Updated on: 2023-08-31T01:58:04.246464+00:00