Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
复制标题
DOI：
10.1145/3158136
复制
发表时间：
2018-01-01
影响因子：
1.8
通讯作者：
Zohar, Yoni
中科院分区：
文献类型：
--
作者：
Grossman, Shelly;Abraham, Ittai;Zohar, Yoni
回调在许多编程环境中是必不可少的，但由于它们允许外部对象以意想不到的方式改变对象的本地状态，从而破坏了模块化，因此使程序理解和推理变得非常复杂。加密货币框架Ethereum中著名的DAO漏洞，利用回调窃取了1.5亿美元。我们定义了有效无回调（ECF）对象的概念，以便在不妨碍模块化推理的情况下允许回调。如果一个对象在每个可能的执行跟踪中都是ECF，则该对象是ECF。我们研究了动态检查ECF在一个给定的执行跟踪和静态检查，如果一个对象是ECF的可判定性。我们还证明了在以太坊中动态检查ECF是可行的，并且可以在线完成。通过运行以太坊中所有执行跟踪的历史记录，我们能够验证几乎所有现有的合约执行（不包括DAO或具有类似已知漏洞的合约）都是ECF。最后，我们表明，ECF，无论是动态或静态验证，使模块化推理封装状态的对象。
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 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.