Oddbean new post about | logout
▲ ▼
Bitcoin Mailing List | 1 years ago (raw) | export | reply | flag 
 🔖 Title: Announcing B'SST: Bitcoin-like Script Symbolic Tracer
🏷️ Categories: bitcoin-dev
 nostr:naddr1qqjxyerz8p3n2ety94jr2v3c956xgenz943rvves94nrqdekxsck2e3ex3nrvqg5waehxw309aex2mrp0yhxgctdw4eju6t0qy2hwumn8ghj7etyv4hzumn0wd68ytnvv9hxgqguwaehxw309ahx7um5wghx6at5d9h8jampd3kx2apwvdhk6q3q2llycjh8gg2lhy4aph9c5au8ch5s0km5axrlxrc6e24dnsaqyu0sxpqqqp65wza0d5x 
⚠️ Heads up! We've now started linking to replaceable long-form events (NIP-23), which allow for dynamic display of thread details like summaries, authors, and more. If you're unable to see this, your client may not support this feature yet.
▲ ▼
78f5a82a | 1 years ago (raw) | root | parent | reply | flag 
 📅 Original date posted:2023-08-30
🗒️ Summary of this message: B'SST is a Bitcoin-like Script Symbolic Tracer that analyzes Bitcoin and Elements scripts, providing a detailed report based on the analysis. It uses the Z3 theorem prover for more thorough analysis. B'SST is more comprehensive than previous projects and supports custom opcodes. It is released under the Prosperity Public License 3.0.0.
📝 Original message:
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