期刊
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL
卷 2, 期 -, 页码 -出版社
ASSOC COMPUTING MACHINERY
DOI: 10.1145/3158136
关键词
Program analysis; Modular reasoning; Smart contracts
资金
- European Research Council under the European Union's Seventh Framework Programme (FP7/2007-2013)/ERC grant [321174]
- Len Blavatnik and the Blavatnik Family foundation
- Blavatnik Interdisciplinary Cyber Research Center at Tel Aviv University
- Pazy Foundation
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.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据