[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 :
Sciences informatiques
Auteur, co-auteur :
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
Langue du document :
Anglais
Titre :
CHAUSSETTE: A Symbolic Verification of Bitcoin Scripts
Date de publication/diffusion :
2024
Nom de la manifestation :
International Workshop on Cryptocurrencies and Blockchain Technology (CBT)
Lieu de la manifestation :
La Haye, Pays-Bas
Date de la manifestation :
28 Septembre 2023
Manifestation à portée :
International
Titre de l'ouvrage principal :
Proc. International Workshop on Cryptocurrencies and Blockchain Technology (CBT)
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
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
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)
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)
