[bitcoin-dev] Announcing B'SST: Bitcoin-like Script Symbolic Tracer

From: Dmitry Petukhov <dp@simplexum•com>
To: bitcoin-dev@lists•linuxfoundation.org
Subject: [bitcoin-dev] Announcing B'SST: Bitcoin-like Script Symbolic Tracer
Date: Wed, 30 Aug 2023 14:07:53 +0200	[thread overview]
Message-ID: <20230830140753.574d2ab9@simplexum.com> (raw)

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