Neville Grech
Skip Abstract Section
Abstract
Ethereum is a distributed blockchain platform, serving as an ecosystem for smart contracts: full-fledged inter-communicating programs that capture the transaction logic of an account. Unlike programs in mainstream languages, a gas limit restricts the execution of an Ethereum smart contract: execution proceeds as long as gas is available. Thus, gas is a valuable resource that can be manipulated by an attacker to provoke unwanted behavior in a victim's smart contract (e.g., wasting or blocking funds of said victim). Gas-focused vulnerabilities exploit undesired behavior when a contract (directly or through other interacting contracts) runs out of gas. Such vulnerabilities are among the hardest for programmers to protect against, as out-of-gas behavior may be uncommon in non-attack scenarios and reasoning about it is far from trivial.
In this paper, we classify and identify gas-focused vulnerabilities, and present MadMax: a static program analysis technique to automatically detect gas-focused vulnerabilities with very high confidence. Our approach combines a control-flow-analysis-based decompiler and declarative program-structure queries. The combined analysis captures high-level domain-specific concepts (such as "dynamic data structure storage" and "safely resumable loops") and achieves high precision and scalability. MadMax analyzes the entirety of smart contracts in the Ethereum blockchain in just 10 hours (with decompilation timeouts in 8% of the cases) and flags contracts with a (highly volatile) monetary value of over $2.8B as vulnerable. Manual inspection of a sample of flagged contracts shows that 81% of the sampled warnings do indeed lead to vulnerabilities, which we report on in our experiment.
- Sidney Amani, Myriam Bégel, Maksym Bortin, and Mark Staples. 2018. Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018). ACM, New York, NY, USA, 66–77. Google Scholar
Digital Library
- Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli. 2016. A survey of attacks on Ethereum smart contracts. Technical Report. Cryptology ePrint Archive: Report 2016/1007, https://eprint.iacr.org/2016/1007.Google Scholar
- Massimo Bartoletti, Salvatore Carta, Tiziana Cimoli, and Roberto Saia. 2017. Dissecting Ponzi schemes on Ethereum: identification, analysis, and impact. (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 Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security (PLAS ’16). ACM, New York, NY, USA, 91–96. Google ScholarDigital Library
- Martin Bravenboer and Yannis Smaragdakis. 2009. Strictly Declarative Specification of Sophisticated Points-to Analyses. In Proc. of the 24th Annual ACM SIGPLAN Conf. on Object Oriented Programming, Systems, Languages, and Applications (OOPSLA ’09). ACM, New York, NY, USA. Google ScholarDigital Library
- Lexi Brent, Anton Jurisevic, Michael Kong, Eric Liu, Francois Gauthier, Vincent Gramoli, Ralph Holz, and Bernhard Scholz. 2018. Vandal: A Scalable Security Analysis Framework for Smart Contracts. CoRR abs/1802.08660 (2018). arXiv: 1809.03981 https://arxiv.org/abs/1809.03981Google Scholar
- Vitalik Buterin. 2013. A Next-Generation Smart Contract and Decentralized Application Platform. https://github.com/ ethereum/wiki/wiki/White- Paper . (2013).Google Scholar
- T. Chen, X. Li, X. Luo, and X. Zhang. 2017. Under-optimized smart contracts devour your money. In 2017 IEEE 24th International Conference on Software Analysis, Evolution and Reengineering (SANER). 442–446.Google Scholar
- Consensys. 2018a. Consensys logo. (2018). https://new.consensys.net/ Accessed: 2018-04-17.Google Scholar
- Consensys. 2018b. Ethereum Smart Contract Best Practices. (2018). https://consensys.github.io/ smart- contract- best- practices/ Accessed: 2018-04-17.Google Scholar
- Kevin Delmolino, Mitchell Arnett, Ahmed E. Kosba, Andrew Miller, and Elaine Shi. 2015. Step by Step Towards Creating a Safe Smart Contract: Lessons and Insights from a Cryptocurrency Lab. IACR Cryptology ePrint Archive 2015 (2015), 460.Google Scholar
- Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. 2002. Extended static checking for Java. In Proc. of the ACM SIGPLAN 2002 Conf. on Programming Language Design and Implementation. ACM Press, 234–245. Google ScholarDigital Library
- FStarLang. 2018. F*: A Higher-Order Effectful Language Designed for Program Verification. (2018). https://www.fstar- lang. org/ Accessed: 2018-04-17.Google Scholar
- Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind. 2018. A Semantic Framework for the Security Analysis of Ethereum smart contracts. CoRR abs/1802.08660 (2018). arXiv: 1802.08660 http://arxiv.org/abs/1802.08660Google Scholar
- Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar. 2017. Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts. Proc. ACM Program. Lang. 2, POPL, Article 48 (Dec. 2017), 28 pages. Google ScholarDigital Library
- Everett Hildenbrandt, Xiaoran Zhu, and Nishant Rodrigues. 2017. KEVM: A Complete Semantics of the Ethereum Virtual Machine.Google Scholar
- Yoichi Hirai. 2017. Defining the Ethereum Virtual Machine for Interactive Theorem Provers. In Financial Cryptography and Data Security, Michael Brenner, Kurt Rohloff, Joseph Bonneau, Andrew Miller, Peter Y.A. Ryan, Vanessa Teague, Andrea Bracciali, Massimiliano Sala, Federico Pintore, and Markus Jakobsson (Eds.). Springer International Publishing, Cham, 520–535.Google Scholar
- Marco Iansiti and Karim R. Lakhani. 2017. The Truth about Blockchain. Harvard Business Review 95 (Jan. 2017), 118–127. Issue 1.Google Scholar
- Neil Immerman. 1999. Descriptive Complexity. Springer.Google Scholar
- Isabelle. 2018. Isabelle. (2018). https://isabelle.in.tum.de/ Accessed: 2018-04-17.Google Scholar
- Herbert Jordan, Bernhard Scholz, and Pavle Subotić. 2016. Soufflé: On Synthesis of Program Analyzers. In Computer Aided Verification, Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing, Cham, 422–430.Google Scholar
- K Framework. 2018. K Framework. (2018). http://www.kframework.org/index.php/Main_Page Accessed: 2018-04-17.Google Scholar
- Sukrit Kalra, Seep Goel, Seep Goel, and Subodh Sharma. 2018. ZEUS: Analyzing Safety of Smart Contracts. In 25th Annual Network and Distributed System Security Symposium (NDSS’18).Google Scholar
- Michael Kong. 2017. A Scalable Method to Analyze Gas Costs, Loops and Related Security Vulnerabilities on the Ethereum Virtual Machine. https://github.com/usyd- blockchain/vandal/wiki/pubs/MKong17.pdf . (11 2017).Google Scholar
- Benjamin Livshits, Manu Sridharan, Yannis Smaragdakis, Ondřej Lhoták, J. Nelson Amaral, Bor-Yuh Evan Chang, Sam Guyer, Uday Khedker, Anders Møller, and Dimitrios Vardoulakis. 2014. In Defense of Soundiness: A Manifesto. Commun. ACM (2014), to appear. Google ScholarDigital Library
- LLVM. 2018. The LLVM Compiler Infrastructure Project. (2018). https://llvm.org/ Accessed: 2018-04-17.Google Scholar
- Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. 2016a. Making Smart Contracts Smarter. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS ’16). ACM, New York, NY, USA, 254–269. Google ScholarDigital Library
- Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. 2016b. Making Smart Contracts Smarter. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS ’16). ACM, New York, NY, USA, 254–269. Google ScholarDigital Library
- Anastasia Mavridou and Aron Laszka. 2018. Designing Secure Ethereum Smart Contracts: A Finite State Machine Based Approach. (2018). http://aronlaszka.com/papers/mavridou2018designing.pdfGoogle Scholar
- Mayur Naik. 2011. Chord: A Versatile Platform for Program Analysis. In 2011 ACM SIGPLAN Conf. on Programming Language Design and Implementation. Tutorial.Google Scholar
- Mayur Naik, Chang-Seo Park, Koushik Sen, and David Gay. 2009. Effective static deadlock detection. In Proc. of the 31st International Conf. on Software Engineering (ICSE ’09). ACM, New York, NY, USA, 386–396. Google ScholarDigital Library
- Satoshi Nakamoto. 2009. Bitcoin: A Peer-to-Peer Electronic Cash System. https://www.bitcoin.org/bitcoin.pdf . (2009).Google Scholar
- Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek Saxena, and Aquinas Hobor. 2018. Finding The Greedy, Prodigal, and Suicidal Contracts at Scale. CoRR abs/1802.06038 (2018). arXiv: 1802.06038 http://arxiv.org/abs/1802.06038Google Scholar
- SeaHorn. 2018. SeaHorn | A Verification Framework. (2018). http://seahorn.github.io/ Accessed: 2018-04-17.Google Scholar
- Ilya Sergey and Aquinas Hobor. 2017. A Concurrent Perspective on Smart Contracts. CoRR abs/1702.05511 (2017). arXiv: 1702.05511 http://arxiv.org/abs/1702.05511Google Scholar
- Olin Shivers. 1991. Control-Flow Analysis of Higher-Order Languages. Ph.D. Dissertation. Carnegie Mellon University. Google ScholarDigital Library
- Olin Shivers. 2004. Higher-order control-flow analysis in retrospect: lessons learned, lessons abandoned. In Best of PLDI 1988, Kathryn S. McKinley (Ed.), Vol. 39. 257–269.Google ScholarDigital Library
- H. Thielecke. 1999. Continuations, functions and jumps. ACM SIGACT News 30 (Jan. 1999), 33–42. Issue 2. Google ScholarDigital Library
- Raja Vallée-Rai, Phong Co, Etienne Gagnon, Laurie J. Hendren, Patrick Lam, and Vijay Sundaresan. 1999. Soot - a Java bytecode optimization framework. In Proc. of the 1999 Conf. of the Centre for Advanced Studies on Collaborative research (CASCON ’99). IBM Press, 125–135. http://dl.acm.org/citation.cfm?id=781995.782008 Google ScholarDigital Library
- Raja Vallée-Rai, Etienne Gagnon, Laurie J. Hendren, Patrick Lam, Patrice Pominville, and Vijay Sundaresan. 2000. Optimizing Java Bytecode Using the Soot Framework: Is It Feasible?. In Proc. of the 9th International Conf. on Compiler Construction (CC ’00). Springer, 18–34. Google ScholarDigital Library
- Various. {n. d.}a. GovernMental page. ({n. d.}). http://governmental.github.io/GovernMental/ Accessed: 2018-04-14.Google Scholar
- Various. {n. d.}b. Safety - Ethereum Wiki. https://github.com/ethereum/wiki/wiki/Safety . ({n. d.}). Accessed: 2018-04-15.Google Scholar
- Various. 2018a. Documentation for the LLL compiler – LLL Compiler Documentation 0.1 documentation. (2018). http: //lll- docs.readthedocs.io/en/latest/index.html Accessed: 2018-04-17.Google Scholar
- Various. 2018b. GitHub - ethereum/serpent. (2018). https://github.com/ethereum/serpent Accessed: 2018-04-17.Google Scholar
- Various. 2018c. GitHub - ethereum/solidity: The Solidity Contract-Oriented Programming Language. (2018). https: //github.com/ethereum/solidity Accessed: 2018-04-17.Google Scholar
- Various. 2018d. GitHub - ethereum/vyper: New experimental programming language. (2018). https://github.com/ethereum/ vyper Accessed: 2018-04-17.Google Scholar
- Various. 2018. Vandal – A Static Analysis Framework for Ethereum Bytecode. (2018). https://github.com/usyd- blockchain/ vandal/ Accessed: 2018-07-30.Google Scholar
- Peter Vessenes. 2016. Ethereum Griefing Wallets: Send w/Throw Is Dangerous. (2016). http://vessenes.com/ ethereum- griefing- wallets- send- w- throw- considered- harmfulGoogle Scholar
- Why3. 2018. Why3. (2018). http://why3.lri.fr/ Accessed: 2018-04-17.Google Scholar
- Gavin Wood. 2014. Ethereum: A Secure Decentralised Generalised Transaction Ledger. http://gavwood.com/Paper.pdf . (2014).Google Scholar
Index Terms
- MadMax: surviving out-of-gas conditions in Ethereum smart contracts
Recommendations
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 ...
Detecting nondeterministic payment bugs in Ethereum smart contracts
The term “smart contracts” has become ubiquitous to describe an enormous number of programs uploaded to the popular Ethereum blockchain system. Despite rapid growth of the smart contract ecosystem, errors and exploitations have been constantly reported ...
A security framework for Ethereum smart contracts
AbstractThe use of blockchain and smart contracts have not stopped growing in recent years. Like all software that begins to expand its use, it is also beginning to be targeted by hackers who will try to exploit vulnerabilities in both the ...
Comments