Petar Tsankov
ABSTRACT
Permissionless blockchains allow the execution of arbitrary programs (called smart contracts), enabling mutually untrusted entities to interact without relying on trusted third parties. Despite their potential, repeated security concerns have shaken the trust in handling billions of USD by smart contracts. To address this problem, we present Securify, a security analyzer for Ethereum smart contracts that is scalable, fully automated, and able to prove contract behaviors as safe/unsafe with respect to a given property. Securify's analysis consists of two steps. First, it symbolically analyzes the contract's dependency graph to extract precise semantic information from the code. Then, it checks compliance and violation patterns that capture sufficient conditions for proving if a property holds or not. To enable extensibility, all patterns are specified in a designated domain-specific language. Securify is publicly released, it has analyzed >18K contracts submitted by its users, and is regularly used to conduct security audits by experts. We present an extensive evaluation of Securify over real-world Ethereum smart contracts and demonstrate that it can effectively prove the correctness of smart contracts and discover critical violations.
Supplemental Material
- 2016. The DAO Attacked: Code Issue Leads to 60 Million Ether Theft. (2016).Google Scholar
- 2016. Etherdice. (2016). Available from: https://etherdice.io/.Google Scholar
- 2016. King of Ether. (2016). Available from: https://github.com/kieranelby/ KingOfTheEtherThrone/blob/v0.4.0/contracts/KingOfTheEtherThrone.sol.Google Scholar
- 2016. King of Ether, Postmortem. (2016). Available from: https://www. kingoftheether.com/postmortem.html.Google Scholar
- 2016. Reentrancy Woes in Smart Contracts. (2016). Available from: http: //hackingdistributed.com/2016/07/13/reentrancy-woes/.Google Scholar
- 2016. theDAO. (2016). Available from: https://etherscan.io/address/ 0xbb9bc244d798123fde783fcc1c72d3bb8c189413.Google Scholar
- 2017. Accidental bug may have frozen $280 million worth of digital coin ether in a cryptocurrency wallet. (2017). Available from: https://www.cnbc.com/2017/11/ 08/accidental-bug-may-have-frozen...Google Scholar
- 2017. Blockchain is empowering the future of insurance. (2017). Available from: https://techcrunch.com/2016/10/29/ blockchain-is-empowering-the-future-of-insurance/.Google Scholar
- 2017. ETHLance. (2017). Available from: http://ethlance.com/.Google Scholar
- 2017. An In-Depth Look at the Parity Multisig Bug. (2017). Available from: http://hackxingdistributed.com/2017/07/22/deep-dive-parity-bug.Google Scholar
- 2017. Northern Trust uses blockchain for private equity recordkeeping. (2017). Available from: http://www.reuters.com/article/ nthern-trust-ibm-blockchain-idUSL1N1G61TX.Google Scholar
- 2017. Parity Ethereum Client. (2017). Available from: https://github.com/ paritytech/parity.Google Scholar
- 2017. Security Alert. (2017). Available from: https://paritytech.io/blog/ security-alert.html.Google Scholar
- 2017. Submarine Sends: IC3's Plan to Clamp Down on ICO Cheats. (2017). Available from: https://www.coindesk.com/ submarine-sends-inside-ic3s-plan-to-clamp-...Google Scholar
- 2018. Ethereum Smart Contract Security Best Practices. (2018). Available from: https://consensys.github.io/smart-contract-best-practices/.Google Scholar
- 2018. Mythril. (2018). Available from: https://github.com/ConsenSys/mythril.Google Scholar
- 2018. Parity Wallet Library. (2018). Available from: https://github.com/ paritytech/parity/blob/4d08e7b0aec46443bf26547b17d10cb302672835/js/src/ contracts/snippets/enhanced-wallet.sol.Google Scholar
- 2018. Solidity, high-level language for writing smart contracts. (2018). Available from: https://solidity.readthedocs.io/en/develop/.Google Scholar
- Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli. 2017. A Survey of Attacks on Ethereum Smart Contracts (SoK). In Principles of Security and Trust - 6th International Conference, POST. 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 Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security (PLAS). 91--96. Google ScholarDigital Library
- Giancarlo Bigi, Andrea Bracciali, Giovanni Meacci, and Emilio Tuosto. 2015. Validation of Decentralised Smart Contracts Through Game Theory and Formal Methods. In Programming Languages with Applications to Biology and Security. 142--161.Google Scholar
- Martin Bravenboer and Yannis Smaragdakis. 2009. Strictly Declarative Specification of Sophisticated Points-to Analyses. In Proceedings of the 24th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). 243--262. Google ScholarDigital Library
- Vitalik Buterin. 2013. Ethereum: a next generation smart contract and decentralized application platform. (2013). Available from: https://github.com/ethereum/ wiki/wiki/White-Paper.Google Scholar
- Vitalik Buterin. 2016. Thinking About Smart Contract Security. (2016). Available from: https://blog.ethereum.org/2016/06/19/thinking-smart-contract-security/.Google Scholar
- Pawel Bylica. 2017. How to Find $10M Just by Reading the Blockchain. (Apr 2017). Available from: https://blog.golemproject.net/ how-to-find-10m-by-just-reading-blockchain-6ae9d39fcd95.Google Scholar
- Ting Chen, Xiaoqi Li, Xiapu Luo, and Xiaosong Zhang. 2017. Under-optimized smart contracts devour your money. In Software Analysis, Evolution and Reengineering (SANER). 442--446.Google Scholar
- Kevin Delmolino, Mitchell Arnett, Ahmed Kosba, Andrew Miller, and Elaine Shi. 2016. Step by Step Towards Creating a Safe Smart Contract: Lessons and Insights from a Cryptocurrency Lab. In Financial Cryptography and Data Security (FC). 79--94.Google Scholar
- Yoshihiko Futamura. 1999. Partial Evaluation of Computation Process - An Approach to a Compiler-Compiler. Higher-Order and Symbolic Computation 12, 4 (1999), 381--391. Google ScholarDigital Library
- Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind. 2018. A Semantic Framework for the Security Analysis of Ethereum Smart Contracts. In Principles of Security and Trust - 7th International Conference (POST). 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
- Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Brandon M. Moore, Daejun Park, Yi Zhang, Andrei Stefanescu, and Grigore Rosu. 2018. KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. In 31st IEEE Computer Security Foundations Symposium (CSF). 204--217.Google Scholar
- Yoichi Hirai. 2016. Formal verification of Deed contract in Ethereum name service. Technical Report. Available from: https://yoichihirai.com/deed.pdf.Google Scholar
- Yoichi Hirai. 2017. Defining the Ethereum Virtual Machine for Interactive Theorem Provers. In Financial Cryptography and Data Security (FC). 520--535.Google Scholar
- Andrew Johnson, LucasWaye, Scott Moore, and Stephen Chong. 2015. Exploring and Enforcing Security Guarantees via Program Dependence Graphs. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 291--302. Google ScholarDigital Library
- Herbert Jordan, Bernhard Scholz, and Pavle Subotic. 2016. Soufflé: On Synthesis of Program Analyzers. In Computer Aided Verification - 28th International Conference (CAV). 422--430.Google Scholar
- Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma. 2018. ZEUS: Analyzing Safety of Smart Contracts. In 25th Annual Network and Distributed System Security Symposium (NDSS).Google Scholar
- Ahmed E. Kosba, Andrew Miller, Elaine Shi, Zikai Wen, and Charalampos Papamanthou. 2016. Hawk: The Blockchain Model of Cryptography and Privacy- Preserving Smart Contracts. In IEEE Symposium on Security and Privacy (SP). 839--858.Google Scholar
- Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. 2016. Making Smart Contracts Smarter. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS). 254--269. Google ScholarDigital Library
- Magnus Madsen, Ming-Ho Yee, and Ondrej Lhoták. 2016. From Datalog to flix: a declarative language for fixed points on lattices. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 194--208. Google ScholarDigital Library
- Ravi Mangal, Xin Zhang, Aditya V. Nori, and Mayur Naik. 2015. A user-guided approach to program analysis. In Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering (ESEC/FSE). 462--473. Google ScholarDigital Library
- Michael C. Martin, V. Benjamin Livshits, and Monica S. Lam. 2005. Finding application errors and security flaws using PQL: a program query language. In Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). 365--383. Google ScholarDigital Library
- Satoshi Nakamoto. 2008. Bitcoin: A peer-to-peer electronic cash system. (2008).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).Google Scholar
- Todd A. Proebsting and Scott A.Watterson. 1997. Krakatoa: Decompilation in Java (Does Bytecode Reveal Source?). In Third USENIX Conference on Object-Oriented Technologies and Systems (COOTS). 185--198. Google ScholarDigital Library
- Grigore Roşu and Traian Florin Şerbănută. 2010. An Overview of the K Semantic Framework. Journal of Logic and Algebraic Programming 79, 6 (2010), 397--434.Google ScholarCross Ref
- Pablo Lamela Seijas, Simon Thompson, and Darryl McAdams. 2016. Scripting smart contracts for distributed ledger technology. IACR Cryptology ePrint Archive 2016 (2016).Google Scholar
- Gagandeep Singh, Markus Püschel, and Martin Vechev. 2017. Fast Polyhedra Abstract Domain. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). 46--59. Google ScholarDigital Library
- Yannis Smaragdakis and Martin Bravenboer. 2010. Using Datalog for Fast and Easy Program Analysis. In Datalog Reloaded - First International Workshop, Datalog. 245--251. Google ScholarDigital Library
- Jeffrey D. Ullman. 1988. Principles of Database and Knowledge-base Systems, Vol. I. Principles of computer science series, Vol. 14. Google ScholarDigital Library
- Raja Vallee-Rai and Laurie J. Hendren. 1998. Jimple: Simplifying Java Bytecode for Analyses and Transformations. (1998).Google Scholar
- Gavin Wood. 2014. Ethereum: A secure decentralised generalised transaction ledger. Ethereum Project Yellow Paper (2014).Google Scholar
- Xin Zhang, Ravi Mangal, Radu Grigore, Mayur Naik, and Hongseok Yang. 2014. On abstraction refinement for program analyses in Datalog. In ACM SIGPLAN Conference on Programming Language Design and Implementation, (PLDI). 239-- 248. Google ScholarDigital Library
Index Terms
- Securify: Practical Security Analysis of Smart Contracts
Recommendations
eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts
CCS '20: Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications SecurityEthereum has emerged as the most popular smart contract platform, with hundreds of thousands of contracts stored on the blockchain and covering diverse application scenarios, such as auctions, trading platforms, or elections. Given the financial nature ...
Security Analysis of Smart Contracts in Datalog
Leveraging Applications of Formal Methods, Verification and Validation. Industrial PracticeAbstractSmart contracts enable mutually untrusted entities to interact without relying on trusted third parties. Despite their potential, repeated security concerns have shaken the trust in handling billions of USD by smart contracts. To address this ...
Formal Modeling and Verification of Smart Contracts
ICSCA '18: Proceedings of the 2018 7th International Conference on Software and Computer ApplicationsSmart contracts can automatically perform the contract terms according to the received information, and it is one of the most important research fields in digital society. The core of smart contracts is algorithm contract, that is, the parties reach an ...
Comments