1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
Return-Path: <dp@simplexum.com>
Received: from smtp2.osuosl.org (smtp2.osuosl.org [140.211.166.133])
by lists.linuxfoundation.org (Postfix) with ESMTP id 87B3BC0032
for <bitcoin-dev@lists.linuxfoundation.org>;
Wed, 30 Aug 2023 12:14:03 +0000 (UTC)
Received: from localhost (localhost [127.0.0.1])
by smtp2.osuosl.org (Postfix) with ESMTP id 6FA53405F5
for <bitcoin-dev@lists.linuxfoundation.org>;
Wed, 30 Aug 2023 12:14:03 +0000 (UTC)
DKIM-Filter: OpenDKIM Filter v2.11.0 smtp2.osuosl.org 6FA53405F5
Authentication-Results: smtp2.osuosl.org;
dkim=pass (1024-bit key) header.d=simplexum.com header.i=@simplexum.com
header.a=rsa-sha256 header.s=mail header.b=FUBVDHQn
X-Virus-Scanned: amavisd-new at osuosl.org
X-Spam-Flag: NO
X-Spam-Score: -0.203
X-Spam-Level:
X-Spam-Status: No, score=-0.203 tagged_above=-999 required=5
tests=[BAYES_40=-0.001, DKIM_SIGNED=0.1, DKIM_VALID=-0.1,
DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, SPF_HELO_PASS=-0.001,
SPF_PASS=-0.001] autolearn=ham autolearn_force=no
Received: from smtp2.osuosl.org ([127.0.0.1])
by localhost (smtp2.osuosl.org [127.0.0.1]) (amavisd-new, port 10024)
with ESMTP id 0k9Y2VpQRgwN
for <bitcoin-dev@lists.linuxfoundation.org>;
Wed, 30 Aug 2023 12:14:02 +0000 (UTC)
X-Greylist: delayed 309 seconds by postgrey-1.37 at util1.osuosl.org;
Wed, 30 Aug 2023 12:14:02 UTC
DKIM-Filter: OpenDKIM Filter v2.11.0 smtp2.osuosl.org 42C124172C
Received: from mail.ruggedbytes.com (mail.ruggedbytes.com [88.99.30.248])
by smtp2.osuosl.org (Postfix) with ESMTPS id 42C124172C
for <bitcoin-dev@lists.linuxfoundation.org>;
Wed, 30 Aug 2023 12:14:02 +0000 (UTC)
Received: from mail.ruggedbytes.com (localhost [127.0.0.1])
by mail.ruggedbytes.com (Postfix) with ESMTPS id D94D4260016D
for <bitcoin-dev@lists.linuxfoundation.org>;
Wed, 30 Aug 2023 12:08:49 +0000 (UTC)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=simplexum.com;
s=mail; t=1693397329;
bh=Ryl2KNjIMjmEnGUEoVBBgnQ8cjJ+mnNliLD6O1UcImk=;
h=Date:From:To:Subject;
b=FUBVDHQnt6wCaqlENWPvax09z/IKswbrD3bF9hr4eJ3gXl1HuMYxKnqbRZvNzi9EU
dMReQgdlrYXonpmI7snLT3Ri72AKSBtFbYHO85OdlpSxWCeniyScpI7y3oBFXaqqFv
nC0wBQlcLkUCpxTUxzQzZRPHQp4izQNOVutURwqk=
Date: Wed, 30 Aug 2023 14:07:53 +0200
From: Dmitry Petukhov <dp@simplexum.com>
To: bitcoin-dev@lists.linuxfoundation.org
Message-ID: <20230830140753.574d2ab9@simplexum.com>
Organization: simplexum.com
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
X-Mailman-Approved-At: Wed, 30 Aug 2023 22:26:48 +0000
Subject: [bitcoin-dev] Announcing B'SST: Bitcoin-like Script Symbolic Tracer
X-BeenThere: bitcoin-dev@lists.linuxfoundation.org
X-Mailman-Version: 2.1.15
Precedence: list
List-Id: Bitcoin Protocol Discussion <bitcoin-dev.lists.linuxfoundation.org>
List-Unsubscribe: <https://lists.linuxfoundation.org/mailman/options/bitcoin-dev>,
<mailto:bitcoin-dev-request@lists.linuxfoundation.org?subject=unsubscribe>
List-Archive: <http://lists.linuxfoundation.org/pipermail/bitcoin-dev/>
List-Post: <mailto:bitcoin-dev@lists.linuxfoundation.org>
List-Help: <mailto:bitcoin-dev-request@lists.linuxfoundation.org?subject=help>
List-Subscribe: <https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev>,
<mailto:bitcoin-dev-request@lists.linuxfoundation.org?subject=subscribe>
X-List-Received-Date: Wed, 30 Aug 2023 12:14:03 -0000
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
|
