CHAUSSETTE: A Symbolic Verification of Bitcoin Scripts

[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)

Publisher :

Springer

Peer reviewed :

Peer reviewed

Funders :

Région wallonne [BE]

Funding number :

Cyber Excellence 2110186

Data Set :

CHAUSSETTE

CHAUSSETTE Code source and Blockchain analysis code source

Available on ORBi :

since 21 August 2023

Statistics

Number of views

188 (18 by ULiège)

Number of downloads

131 (13 by ULiège)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

Bibliography

Andresen, G.: Bitcoin core release notes 0.9.0. https://github.com/bitcoin/bitcoin/blob/master/doc/release-notes/release-notes-0.9.0.md. Accessed20 Apr 2023
Andresen, G.: Pay to script hash. BIP 16, Bitcoin (January 2012)
Andrychowicz, M., Dziembowski, S., Malinowski, D., Mazurek, L.: Fair two-party computations via bitcoin deposits. In: Proceedings of the Financial Cryptography and Data Security (FC) (March 2014)
Andrychowicz, M., Dziembowski, S., Malinowski, D., Mazurek, L.: Modeling bitcoin contracts by timed automata. In: Proceedings of the Formal Modeling and Analysis of Timed Systems (FORMATS) (September 2014)
Antonopoulos, A.: Mastering Bitcoin. O’Reilly Media, Inc. (2014)
Arrieche, A., Henn, P.: Who are the biggest bitcoin mining companies? https://capital.com/biggest-global-crypto-bitcoin-mining-companies-ranking-btc#:~:text=What%20are%20the%20famous%20bitcoin,according%20to%20data %20from%20CompaniesMarketCap. Accessed 08 May 2023
Atzei, N., Bartoletti, M., Cimoli, T., Lande, S., Zunino, R.: Sok: unraveling bitcoin smart contracts. In: Proceedings of the Principles of Security and Trust (POST) (April 2018)
Banasik, W., Dziembowski, S., Malinowski, D.: Efficient zero-knowledge contingent payments in cryptocurrencies without scripts. In: Proceedings of the European Symposium on Research in Computer Security (ESORICS) (September 2016)
Bartoletti, M., Zunino, R.: Constant-deposit multiparty lotteries on bitcoin. In: Proceedings of the Financial Cryptography and Data Security (FC) (April 2017)
Bartoletti, M., Zunino, R.: Verifying liquidity of bitcoin contracts. In: Proceedings of the Principles of Security and Trust (POSRT) (April 2019)
Bentov, I., Kumaresan, R.: How to use bitcoin to design fair protocols. In: Proceedings of the Advances in Cryptology (CRYPTO) (August 2014)
Binance. Binance Coin Whitepaper. https://www.exodus.com/assets/docs/binance-coin-whitepaper.pdf. Accessed 02 May 2023
Bistarelli, S., Mercanti, I., Santini, F.: An analysis of non-standard bitcoin transactions. In: Proceedings of the Crypto Valley Conference on Blockchain Technology (CVCBT) (June 2018)
Bitcoin Community. Bitcoin improvement proposals. https://github.com/bitcoin/bips. Accessed 30 Mar 2023
Bitcoin Community. getrawmempool-bitcoin. https://developer.bitcoin.org/reference/rpc/getrawmempool.html. Accessed 01 June 2023
Bitcoin Community. Op checksig. https://en.bitcoin.it/wiki/OP_CHECKSIG. Accessed 07 Aug 2023
Bitcoin Community. RPC API Reference. https://developer.bitcoin.org/reference/rpc/. Accessed 11 Apr 2023
Bitcoin Community. Running a Full Node. https://bitcoin.org/en/full-node. Accessed 30 Mar 2023
Bitcoin Community. Script. https://en.bitcoin.it/wiki/Script. Accessed 30 Mar 2023
Bitcoin Core Developers. Bitcoin Core-interpreter.cpp. https://github.com/bitcoin/bitcoin/blob/80f4979322b574be29c684b2e106804432420ebf/src/script/interpreter.cpp#L412. Accessed 28 Apr 2023
Bitcoin Core Developers. Dogecoin-script.cpp. https://github.com/dogecoin/dogecoin/blob/master/src/script/script.cpp. Accessed 02 May 2023
Bitcoin Core Developers. Litecoin-script.cpp. https://github.com/litecoin-project/litecoin/blob/master/src/script/script.cpp. Accessed 02 May 2023
blockchain.com: Bitcoin Price. https://www.blockchain.com/explorer/assets/btc. Accessed 26 Apr 2023
blockchain.com. Total hash rate (TH/s). https://www.blockchain.com/fr/explorer/charts/hash-rate. Accessed26 Apr 2023
blockchain.com. Unspent transaction outputs. https://www.blockchain.com/fr/explorer/charts/utxo-count. Accessed18 Apr 2023
Buterin, V.: Ethereum Whitepaper. https://ethereum.org/en/whitepaper/. Accessed 02 May 2023
Chainalysis: 60% of bitcoin is held long term as digital gold. What about the rest?, https://blog.chainalysis.com/reports/bitcoin-market-data-exchanges-trading/. Accessed 13Apr 2023
CoinMarketCap. Coinmarketcap. https://coinmarketcap.com/fr/. Accessed 26 Apr 2023
ConsenSys. Mythril. https://github.com/ConsenSys/mythril. Accessed 12 Apr 2023
Enzyme Finance. Oyente. https://github.com/enzymefinance/oyente. Accessed 12 Apr 2023
Kalodner, H., et al.: Blocksci. https://github.com/citp/BlockSci. Accessed 07 Aug 2023
Kalodner, H., et al.: BlockSci: dsign and applications of a blockchain analysis platform. In: Proceedings of the USENIX Security Symposium (August 2020)
Kessler, S.: Axie infinity’s Ronin blockchain overhauls tech, expands to new game studios a year after $625m hack. https://www.coindesk.com/tech/2023/03/30/axie-infinitys-ronin-blockchain-overhauls-tech-expands-to-new-ip-on-anniversary-of-600m-hack/. Accessed 02 May 2023
Klomp, R., Bracciali, A.: On symbolic verification of bitcoin’s script language. In: Proceedings of the Data Privacy Management, Cryptocurrencies and Blockchain Technology (DPM) (September 2018)
Korn, J.: Another crypto bridge attack: nomad loses $190 million in chaotic hack. https://edition.cnn.com/2022/08/03/tech/crypto-bridge-hack-nomad/index. html. Accessed 02May 2023
Li, Y., Liu, F., Wang, G.: New records in collision attacks on RIPEMD-160 and SHA-256. In: Proceedings of the International Conference on the Theory and Applications of Cryptographic Techniques (EUROCRYPT) (April 2023)
Lombrozo, E., Lau, J., Wuille, P.: Segregated witness (consensus layer). BIP 141, Bitcoin (December 2015)
Maxwell, G.: The first successful zero-knowledge contingent payment. https://bitcoincore.org/en/2016/02/26/zero-knowledge-contingent-payments-announcement/. Accessed 12Apr 2023
Miller, A.K., Bentov, I.: Zero-collateral lotteries in bitcoin and ethereum. In: Proceedings of the IEEE European Symposium on Security and Privacy Workshops (EuroS&PW) (April 2016)
Monniaux, D.: A survey of satisfiability modulo theory. In: Proceedings of the Computer Algebra in Scientific Computing (SASC) (September 2016)
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (March–April 2008)
Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008). http://www. bitcoin.org/bitcoin.pdf
Perry, D., Mattavelli, A., Zhang, X., Cadar, C.: Accelerating array constraints in symbolic execution. In: Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA) (July 2017)
Tang, Y., Li, K., Wang, Y., Chen, J.: Ethical challenges in blockchain network measurement research. In: Proceedings of the Workshop on Ethics in Computer Security (EthiCS) (February 2023)
Todd, P.: Topic: REWARD offered for hash collisions for SHA1, SHA256, RIPEMD160 and other. https://bitcointalk.org/index.php?topic=293382.0. Accessed 26 Apr 2023
Trail of Bits: Manticore. https://github.com/trailofbits/manticore. Accessed 12Apr 2023
TRM Labs. Looking back at 2022 and towards 2023 to see what the future holds for digital assets policy (December 2022). https://www.trmlabs.com/post/looking-back-at-2022-and-towards-2023-to-see-what-the-future-holds-for-digital-assets-policy. Accessed 26 Apr 2023
Tsankov, P., Dan, A., Drachsler-Cohen, D., Gervais, A., Bünzli, F., Vechev, M.: Securify: practical security analysis of smart contracts. In: Proceedings of the ACM SIGSAC Conference on Computer and Communications Security (CCS) (October 2018)