Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam, Rinetzky, Mooly Sagiv, and Yoni Zohar

TL;DR
This paper introduces the concept of Effectively Callback Free (ECF) objects to enable modular reasoning in programming, especially in smart contracts, by allowing callbacks without losing reasoning capabilities, and demonstrates its practical feasibility in Ethereum.
Contribution
The paper defines ECF objects, studies their decidability, and shows how to verify ECF dynamically and statically, improving understanding and security of smart contracts.
Findings
Most Ethereum contracts are ECF, excluding known vulnerable ones like DAO.
Dynamic ECF verification in Ethereum is feasible and can be performed online.
ECF enables modular reasoning about objects with encapsulated state.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
