[en] 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.
Disciplines :
Computer science
Author, co-author :
Jacquot, Vincent ; Université de Liège - ULiège > Montefiore Institute of Electrical Engineering and Computer Science
Donnet, Benoît ; Université de Liège - ULiège > Département d'électricité, électronique et informatique (Institut Montefiore) > Algorithmique des grands systèmes
Language :
English
Title :
CHAUSSETTE: A Symbolic Verification of Bitcoin Scripts
Publication date :
September 2023
Event name :
International Workshop on Cryptocurrencies and Blockchain Technology (CBT)
Event place :
La Haye, Netherlands
Event date :
28 Septembre 2023
Audience :
International
Main work title :
Proc. International Workshop on Cryptocurrencies and Blockchain Technology (CBT)
