Hello list, I have released B'SST: Bitcoin-like Script Symbolic Tracer
It can be found at https://github.com/dgpv/bsst B'SST analyses Bitcoin and Elements scripts by symbolically executing all possible execution paths, and tracking constraints that opcodes impose on values they operate on. It then outputs a report based on this analysis. It can do analysis with the help of Z3 theorem prover [1]. With Z3 enabled, analysis will take more time, but all the features that depend on SMT solver can be employed. By default, the analysis does not use Z3, so it is fast, but not nearly as thorough. Regarding the analysis performed, there are limitations and caveats. Please refer to README.md in the repo at [0] for details. I am aware of only one project that has aimed to do this type of analysis before - the "SCRIPT Analyser" [2], but it had no updates in its github repo for 5 years. Compared to [2], B'SST is more thorough in its effort to match the reference interpreter closely, and it also uses SMT solver, while [2] has used prolog for constraints solving. Elements script interpreter [3], which is an extension of Bitcoin script interpreter, was used as reference. As an illustration of what information the analysis can provide, for this rather contrieved example script: 7 ADD DUP 3 5 WITHIN IF 0x00 ELSE 0 ENDIF EQUALVERIFY 2DUP EQUALVERIFY SUB 0 EQUAL The analysis report will show that: - The first branch of IF will always fail - Witness 0 must be -7 for script to succeed, - Possible values for witness 1 and 2 are -1 - Result of last EQUAL is always true (because this condition was already checked by second EQUALVERIFY) For more extensive example, please look at the report [5] for a rather complex Elements script [4] Plugins to implement custom opcodes are supported, please see "Custom opcodes" section in README.md B'SST is released under Prosperity Public License 3.0.0, which is a "Free for non-commercial use" license, with a trial period for commercial use and exemptions for educational institutions, public research organizations, etc. Please refer to LICENSE.md file in the repo at [0] for details. [0] https://github.com/dgpv/bsst [1] https://github.com/Z3Prover/z3 [2] https://github.com/RKlompUU/SCRIPTAnalyser [3] https://github.com/ElementsProject/elements/blob/master/src/script/interpreter.cpp [4] https://github.com/fuji-money/tapscripts/blob/with-annotations-for-bsst/beta/mint-mint.tapscript [5] https://gist.github.com/dgpv/b57ecf4d9e3d0bfdcc2eb9147c9b9abf _______________________________________________ bitcoin-dev mailing list bitcoin-dev@lists.linuxfoundation.org https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
