B'SST: Bitcoin-like Script Symbolic Tracer v0.1.2 released

Implementation
1

A new release of the most powerful analysis tool for Bitcoin and Elements scripts (yes, I want to brag! :smile:)

URL: GitHub - dgpv/bsst: B'SST: Bitcoin-like Script Symbolic Tracer

New features and improvements: Plugins, assertions and assumptions, dynamic PICK/ROLL argument support, features to help with malleability analysis

More detailed description (Full release notes is at bsst/release-notes.md at 35143a90b6e6e1dcd61a2991a4881c04190c5569 · dgpv/bsst · GitHub):

  • Rework plugin system, now plugins are ‘general’ in a sense that they can hook into different stages of analysis to observe or change various things. Also some useful plugins are added

  • Add ability to set assertions on stack values and witnesses, and assumptions for data placeholders. Please see newly added “Assertions” and “Assumptions” sections in README

  • Add ability to analyze opcodes that access the stack differently based on their arguments, like PICK, ROLL, CHECKMULTISIG, even if these arguments are not statically known

  • Add ability to set aliases for witnesses with // bsst-name-alias(wit<N>): alias_name (where is withess number). For example, aliased witnesses 0 will be shown in the report as alias_name<wit0>

  • New setting: --produce-model-values-for. It is a set of glob patterns to specify which model values to produce. Please look at the help text for this setting for details. Data references now are not included in the default set to produce model values for, but can be enabled with $* pattern.

  • More than one model value sample can be generated per analyzed value, if max number of samples is specified after : in the pattern given with --produce-model-values-for setting. The limitation of multiple samples is that samples are generated independently, that means for $a $b ADD VERIFY your can get 1, 0 as possible values for both $a and $b, even if they cannot be both 0 at the same time

  • Byte sizes of model value samples will be shown in the report when --report-model-value-sizes is set to true

There was also other (less prominent) improvements and of course bugfixes.

A note on features to help with malleability analysis:

  • Now that report can contain sizes of the witnesses, it is easier to calculate total witness size.
  • Model values are generated such that values with different sizes are generated first, so it is easier to find out all possible sizes.
  • The model values that are the same in ‘child’ execution paths are now grouped together and is ‘moved up’ in the hierarchy of the execution paths in the report. It is now easier to see which values are the same despite branching.
  • The sizes are ‘moved up’ execution path hierarchy independently of the values themselves. The report can show for example that a witness has the same size in all paths while model values might be different within the execution paths
  • Plugins that might be useful in analyzing malleability: checksig_track_bsst_plugin.py and model_value_usage_track_bsst_plugin.py (please look at plugins/README.md for details)
2

I plan to change how execution paths are shown in the B’SST report.

I think that I came up with better format for that.

But I want to have other opinions on this change, if possible, before merging this

In short, before it was:

IF wit0 @ 0:L1 : True
NOTIF wit1 @ 1:L1 : False
IFDUP wit2 @ 2:L1 : True
-------------------------

After the change, it will be:

When wit0 = 1 :: [IF @ 0:L1]
 And wit1 = 0 :: [NOTIF @ 1:L1]
 And BOOL(wit2) is True :: [IFDUP @ 2:L1]
-----------------------------------------

More details in Use actual conditions to designate paths, instead of opcodes with args by dgpv · Pull Request #33 · dgpv/bsst · GitHub

you can also get that branch from that PR and try yourself on your scripts to see if the change improves the readability / ease of comprehension for the report

Please give your opinion here or in the github PR