From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from smtp2.osuosl.org (smtp2.osuosl.org [140.211.166.133]) by lists.linuxfoundation.org (Postfix) with ESMTP id 87B3BC0032 for ; 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 ; 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 ; 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 ; 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 ; 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 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 List-Unsubscribe: , List-Archive: List-Post: List-Help: List-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