CHAUSSETTE: A Symbolic Verification of Bitcoin Scripts

The Bitcoin protocol relies on scripts written in SCRIPT, a simple Turing-incomplete stack-based language, for locking the money carried over the Bitcoin network. This paper explores the usage of symbolic execution for finding transactions that permit to redeem the money without being the legitimate owner. In particular, we show in detail how using insecure scripts could have led to security breaches, resulting in bitcoins theft. Our contributions include (i) a quantification of the vulnerable script instances over the full Bitcoin history up to Feburary, 4th 2023; (ii) the development and open source publication of a symbolic execution tool, called CHAUSSETTE; (iii) the description of how to use CHAUSSETTE to perform the attack; and, (iv) a discussion around a way to secure vulnerable money.