Shelly Grossman
Noam Rinetzky
Abstract
Callbacks are essential in many programming environments, but drastically complicate program understanding and reasoning because they allow to mutate object's local states by external objects in unexpected fashions, thus breaking modularity. The famous DAO bug in the cryptocurrency framework Ethereum, employed callbacks to steal $150M. We define the notion of Effectively Callback Free (ECF) objects in order to allow callbacks without preventing modular reasoning.
An object is ECF in a given execution trace if there exists an equivalent execution trace without callbacks to this object. An object is ECF if it is ECF in every possible execution trace. We study the decidability of dynamically checking ECF in a given execution trace and statically checking if an object is ECF. We also show that dynamically checking ECF in Ethereum is feasible and can be done online. By running the history of all execution traces in Ethereum, we were able to verify that virtually all existing contract executions, excluding these of the DAO or of contracts with similar known vulnerabilities, are ECF. Finally, we show that ECF, whether it is verified dynamically or statically, enables modular reasoning about objects with encapsulated state.
Supplemental Material
- 2017. Validity Labs. https://validitylabs.org . [Online].Google Scholar
- Karim Ali and Ondřej Lhoták. 2013. Averroes: Whole-program Analysis Without the Whole Program. In Proceedings of the 27th European Conference on Object-Oriented Programming (ECOOP’13). Springer-Verlag, Berlin, Heidelberg, 378–400. Google ScholarDigital Library
- Ambisafe. 2017. Ethereum Asset Platform. https://www.ambisafe.co/ . [Online; accessed 1-July-2017].Google Scholar
- B9Lab. 2017. ING hack challenge. [Online].Google Scholar
- Anindya Banerjee and David A. Naumann. 2005. Ownership confinement ensures representation independence for objectoriented programs. J. ACM 52, 6 (2005), 894–960. Google ScholarDigital Library
- Philip A. Bernstein, Vassos Hadzilacos, and Nathan Goodman. 1987. Concurrency Control and Recovery in Database Systems. Addison-Wesley.Google ScholarDigital Library
- 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
- Bok Consulting. 2016a. The DAO ETC Drains. https://github.com/bokkypoobah/TheDAOETCDrains . [Online; accessed 2-July-2017].Google Scholar
- Bok Consulting. 2016b. Ethereum Network Attacker’s IP Address Is Traceable. https://www.bokconsulting.com.au/blog/ ethereum-network-attackers-ip-address-is-traceable/ . [Online; accessed 30-June-2017].Google Scholar
- Ahmed Bouajjani, Javier Esparza, and Oded Maler. 1997. Reachability analysis of pushdown automata: Application to model-checking. CONCUR’97: Concurrency Theory (1997), 135–150.Google Scholar
- Vitalik Buterin. 2016. CRITICAL UPDATE Re: DAO Vulnerability. https://blog.ethereum.org/2016/06/17/ critical-update-re-dao-vulnerability/ . [Online; accessed 2-July-2017].Google Scholar
- Phil Daian. 2016. (2016). http://hackingdistributed.com/2016/06/18/analysis-of-the-dao-exploit/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
- Kevin Delmolino, Mitchell Arnett, Ahmed E. Kosba, Andrew Miller, and Elaine Shi. 2016. Ethereum - Serpent Tutorial and Smart Contract Lab. https://github.com/mc2-umd/ethereumlab/blob/master/Examples/RPS_v2_new.py . [Online; accessed 2-July-2017].Google Scholar
- Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall.Google ScholarDigital Library
- Ethereum Classic. 2017. Ethereum Classic. https://etcchain.com/ . [Online; accessed 2-July-2017].Google Scholar
- Ethereum Foundation. 2017a. Geth. https://github.com/ethereum/go-ethereum/wiki/geth . [Online; accessed 30-June-2017].Google Scholar
- Ethereum Foundation. 2017b. Solidity. https://solidity.readthedocs.io/en/develop/ . [Online; accessed 5-July-2017].Google Scholar
- Ethereum Reddit. 2016. From the MAKER DAO slack: "Today we discovered a vulnerability in the ETH token wrapper which would let anyone drain it.". https://www.reddit.com/r/ethereum/comments/4nmohu/from_the_maker_dao_slack_ today_we_discovered_a/ . [Online; accessed 2-July-2017].Google Scholar
- Etherscan. 2017. 0xbfBeA57d87E15529a30B6634C1C13F1A12Fa4d09. https://etherscan.io/address/ 0xbfbea57d87e15529a30b6634c1c13f1a12fa4d09 . [Online; accessed 1-July-2017].Google Scholar
- Jean-Christophe Filliâtre and Andrei Paskevich. 2013. Why3 — Where Programs Meet Provers. In Proceedings of the 22nd European Symposium on Programming (Lecture Notes in Computer Science), Matthias Felleisen and Philippa Gardner (Eds.), Vol. 7792. Springer, 125–128.Google ScholarDigital Library
- Alexey Gotsman and Hongseok Yang. 2011. Liveness-Preserving Atomicity Abstraction. In Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II. 453–465. Google ScholarCross Ref
- C. A. R. Hoare. 1972. Proof of Correctness of Data Representations. Acta Inf. 1 (1972), 271–281.Google ScholarDigital Library
- J.E. Hopcroft, R. Motwani, and J.D. Ullman. 2006. Introduction to automata theory, languages, and computation. Addisonwesley.Google Scholar
- Leslie Lamport. 1978. Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM 21, 7 (July 1978), 558–565. Google ScholarDigital Library
- K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning: 16th International Conference, LPAR-16, Dakar, Senegal, April 25–May 1, 2010, Revised Selected Papers, Edmund M. Clarke and Andrei Voronkov (Eds.). Springer, Berlin, Heidelberg, 348–370. Google ScholarCross Ref
- K. Rustan M. Leino and Peter Müller. 2005. Modular Verification of Static Class Invariants. In FM 2005: Formal Methods, International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005, Proceedings. 26–42.Google Scholar
- K. Rustan M. Leino and Greg Nelson. 2002. Data Abstraction and Information Hiding. ACM Trans. Program. Lang. Syst. 24, 5 (Sept. 2002), 491–553. Google ScholarDigital Library
- Francesco Logozzo. 2009. Class Invariants As Abstract Interpretation of Trace Semantics. Comput. Lang. Syst. Struct. 35, 2 (July 2009), 100–142. Google ScholarDigital Library
- 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 ’16). ACM, New York, NY, USA, 254–269. Google ScholarDigital Library
- Melonport. 2017. Oyente. https://oyente.melonport.com . [Online; accessed 6-July-2017].Google Scholar
- Satoshi Nakamoto. 2008. Bitcoin: A peer-to-peer electronic cash system. https://bitcoin.org/bitcoin.pdf .Google Scholar
- Johannes Pfeffer. 2016. The rise of the Dark DAO. https://medium.com/@oaeee/the-rise-of-the-dark-dao-72b21a2212e3 . [Online; accessed 2-July-2017].Google Scholar
- Rob Pike. 2012. Go at Google. In Proceedings of the 3rd Annual Conference on Systems, Programming, and Applications: Software for Humanity (SPLASH ’12). ACM, New York, NY, USA, 5–6. Google ScholarDigital Library
- Ilya Sergey and Aquinas Hobor. 2017. A Concurrent Perspective on Smart Contracts. In 1st Workshop on Trusted Smart Contracts. Google ScholarCross Ref
- Ethereum StackExchange. 2017. Why is my node synchronization stuck/extremely slow at block 2,306,843? https://ethereum. stackexchange.com/questions/9883/why-is-my-node-synchronization-stuck-extremely-slow-at-block-2-306-843 . [Online; accessed 30-June-2017].Google Scholar
- Nick Szabo. 1997. Formalizing and securing relationships on public networks. First Monday 2, 9 (1997). Google ScholarCross Ref
- Validity Labs. 2017. Recursive call exploit. [Online].Google Scholar
- Peter Vessenes. 2016. More Ethereum Attacks: Race-To-Empty is the Real Deal. http://vessenes.com/ more-ethereum-attacks-race-to-empty-is-the-real-deal/ . [Online; accessed 2-July-2017].Google Scholar
- Gavin Wood. 2016. Ethereum: A Secure Decentralised Generalised Transaction Ledger. http://gavwood.com/paper.pdf . [Online; accessed 5-July-2017].Google Scholar
Index Terms
- Online detection of effectively callback free objects with applications to smart contracts
Recommendations
Formal Verification of Smart Contracts: Short Paper
PLAS '16: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for SecurityEthereum is a framework for cryptocurrencies which uses blockchain technology to provide an open global computing platform, called the Ethereum Virtual Machine (EVM). EVM executes bytecode on a simple stack machine. Programmers do not usually write EVM ...
Annotary: A Concolic Execution System for Developing Secure Smart Contracts
Computer Security – ESORICS 2019AbstractEthereum smart contracts are executable programs, deployed on a peer-to-peer network and executed in a consensus-based fashion. Their bytecode is public, immutable and once deployed to the blockchain, cannot be patched anymore. As smart contracts ...
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