ABSTRACT
Smart contracts---stateful executable objects hosted on blockchains like Ethereum---carry billions of dollars worth of coins and cannot be updated once deployed. We present a new systematic characterization of a class of trace vulnerabilities, which result from analyzing multiple invocations of a contract over its lifetime. We focus attention on three example properties of such trace vulnerabilities: finding contracts that either lock funds indefinitely, leak them carelessly to arbitrary users, or can be killed by anyone. We implemented Maian, the first tool for specifying and reasoning about trace properties, which employs interprocedural symbolic analysis and concrete validator for exhibiting real exploits. Our analysis of nearly one million contracts flags 34, 200 (2, 365 distinct) contracts vulnerable, in 10 seconds per contract. On a subset of 3, 759 contracts which we sampled for concrete validation and manual analysis, we reproduce real exploits at a true positive rate of 89%, yielding exploits for 3, 686 contracts. Our tool finds exploits for the infamous Parity bug that indirectly locked $200 million US worth in Ether, which previous analyses failed to capture.
- Anthony Akentiev. 2018. Parity Multisig Github. https://github.com/paritytech/parity/issues/6995Google Scholar
- JD Alois. 2017. Ethereum Parity Hack May Impact ETH 500,000 or $146 Million.Google Scholar
- Sidney Amani, Myriam Bégel, Maksym Bortin, and Mark Staples. 2018. Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL. In CPP. ACM, 66--77. Google ScholarDigital Library
- Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli. 2017. A Survey of Attacks on Ethereum Smart Contracts (SoK). In POST (LNCS), Vol. 10204. Springer, 164--186. Google ScholarDigital Library
- Massimo Bartoletti, Salvatore Carta, Tiziana Cimoli, and Roberto Saia. 2017. Dissecting Ponzi schemes on Ethereum: identification, analysis, and impact. CoRR abs/1703.03779 (2017).Google Scholar
- Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, and Santiago Zanella-Béguelin. 2016. Formal Verification of Smart Contracts: Short Paper. In PLAS. ACM, 91--96. Google ScholarDigital Library
- Ting Chen, Xiaoqi Li, Xiapu Luo, and Xiaosong Zhang. 2017. Under-optimized smart contracts devour your money. In IEEE 24th International Conference on Software Analysis, Evolution and Reengineering, SANER. 442--446.Google ScholarCross Ref
- ConsenSys Diligence. 2018. Ethereum Smart Contract Security Best Practices. https://consensys.github.io/smart-contract-best-practicesGoogle Scholar
- Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In TACAS (LNCS), Vol. 4963. Springer, 337--340. Google ScholarDigital Library
- Michael del Castillo. June 17, 2016. The DAO Attacked: Code Issue Leads to $60 Million Ether Theft.Google Scholar
- Kevin Delmolino, Mitchell Arnett, Ahmed E. Kosba, Andrew Miller, and Elaine Shi. 2016. Step by Step Towards Creating a Safe Smart Contract: Lessons and Insights from a Cryptocurrency Lab. In FC 2016 International Workshops (LNCS), Vol. 9604. Springer, 79--94.Google ScholarCross Ref
- Etherscan 2018. https://etherscan.io/Google Scholar
- Etherscan verified source codes 2018. Etherscan verified source codes. https://etherscan.io/contractsVerifiedGoogle Scholar
- Jean-Christophe Filliâtre and Andrei Paskevich. 2013. Why3 - Where Programs Meet Provers. In ESOP (LNCS), Vol. 7792. Springer, 125--128. Google ScholarDigital Library
- Go-ethereum 2018. https://github.com/ethereum/go-ethereumGoogle Scholar
- Patrice Godefroid. 2011. Higher-order Test Generation. In PLDI. ACM, 258--269. Google ScholarDigital Library
- Governmental bug 2018. GovernMental's 1100ETH jackpot payout is stuck because it uses too much gas. https://www.reddit.com/r/ethereum/comments/4ghzhv/Google Scholar
- Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind. 2018. A Semantic Framework for the Security Analysis of Ethereum Smart Contracts. In POST (LNCS), Vol. 10804. Springer, 243--269.Google Scholar
- Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar. 2018. Online detection of effectively callback free objects with applications to smart contracts. PACMPL 2, POPL (2018), 48:1--48:28. Google ScholarDigital Library
- Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHorn Verification Framework. In CAV, Part I (LNCS), Vol. 9206. Springer, 343--361.Google Scholar
- Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Daejun Park, Yi Zhang, Brandon Moore, and Grigore Rosu. 2018. KEVM: A Complete Semantics of the Ethereum Virtual Machine. In CSF. IEEE. To appear.Google Scholar
- Yoichi Hirai. 2017. Defining the Ethereum Virtual Machine for Interactive Theorem Provers. In 1st Workshop on Trusted Smart Contracts (LNCS), Vol. 10323. Springer, 520--535.Google Scholar
- Yoichi Hirai. 2017. Ethereum Virtual Machine for Coq (v0.0.2). Published online on 5 March 2017. https://goo.gl/DxYFwKGoogle Scholar
- Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma. 2018. Zeus: Analyzing Safety of Smart Contracts. In NDSS. To appear.Google Scholar
- Johannes Krupp and Christian Rossow. 2018. teEther: Gnawing at Ethereum to Automatically Exploit Smart Contracts. In 27th USENIX Security Symposium (USENIX Security 18). USENIX Association, Baltimore, MD, 1317--1333. https://www.usenix.org/conference/usenixsecurity18/presentation/krupp Google ScholarDigital Library
- Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. 2016. Making Smart Contracts Smarter. In CCS. ACM, 254--269. Google ScholarDigital Library
- Manticore 2018. https://github.com/trailofbits/manticoreGoogle Scholar
- Kenneth L. McMillan. 2007. Interpolants and Symbolic Model Checking. In VMCAI (LNCS), Vol. 4349. Springer, 89--90. Google ScholarDigital Library
- Mortal 2018. Contract mortal. https://etherscan.io/address/0x4671ebe586199456ca28ac050cc9473cbac829eb#codeGoogle Scholar
- Bernhard Mueller. January 2018. How Formal Verification Can Ensure Flawless Smart Contracts. https://goo.gl/9wUFE1Google Scholar
- Mythril 2018. https://github.com/b-mueller/mythril/Google Scholar
- Satoshi Nakamoto. 2008. Bitcoin: A peer-to-peer electronic cash system. http://bitcoin.org/bitcoin.pdfGoogle Scholar
- Oyente 2018. Oyente: An Analysis Tool for Smart Contracts. https://github.com/melonproject/oyenteGoogle Scholar
- Parity bug 2018. The guy who blew up Parity didn't know what he was doing. https://www.reddit.com/r/CryptoCurrency/comments/7beos3/Google Scholar
- Jack Pettersson and Robert Edström. 2016. Safer Smart Contracts through Type-Driven Development. Master's thesis. Chalmers University of Technology, Sweden.Google Scholar
- George Pîrlea and Ilya Sergey. 2018. Mechanising blockchain consensus. In CPP. ACM, 78--90. Google ScholarDigital Library
- Christian Reitwiessner. 2015. Formal Verification for Solidity Contracts. https://forum.ethereum.org/discussion/3779/formal-verification-for-solidity-contractsGoogle Scholar
- Grigore Rosu. December 2017. ERC20-K: Formal Executable Specification of ERC20. https://runtimeverification.com/blog/?p=496Google Scholar
- Securify 2018. Securify: Formal Verification of Ethereum Smart Contracts. http://securify.ch/Google Scholar
- Ilya Sergey and Aquinas Hobor. 2017. A Concurrent Perspective on Smart Contracts. In 1st Workshop on Trusted Smart Contracts (LNCS), Vol. 10323. Springer, 478--493.Google ScholarCross Ref
- Emin Gün Sirer. 2016. Reentrancy Woes in Smart Contracts. http://hackingdistributed.com/2016/07/13/reentrancy-woes/Google Scholar
- Solidity 2018. Solidity: High-Level Language for Implementing Smart Contracts. http://solidity.readthedocs.io/Google Scholar
- Gavin Wood. 2014. Ethereum: A Secure Decentralised Generalised Transaction Ledger. https://ethereum.github.io/yellowpaper/paper.pdfGoogle Scholar
Recommendations
ContractFuzzer: fuzzing smart contracts for vulnerability detection
ASE '18: Proceedings of the 33rd ACM/IEEE International Conference on Automated Software EngineeringDecentralized cryptocurrencies feature the use of blockchain to transfer values among peers on networks without central agency. Smart contracts are programs running on top of the blockchain consensus protocol to enable people make agreements while ...
From Contracts to E-Contracts: Modeling and Enactment
Contracts are complex to understand, represent and process electronically. Usually, contracts involve various entities such as parties, activities and clauses. An e-contract is a contract modeled, specified, executed and enacted (controlled and ...
Security Vulnerabilities in Ethereum Smart Contracts
iiWAS2018: Proceedings of the 20th International Conference on Information Integration and Web-based Applications & ServicesSmart contracts (SC) are one of the most appealing features of blockchain technologies facilitating, executing, and enforcing predefined terms of coded contracts without intermediaries. The steady adoption of smart contracts on the Ethereum blockchain ...
Comments