{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T05:36:14Z","timestamp":1773552974553,"version":"3.50.1"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["321174"],"award-info":[{"award-number":["321174"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001742","name":"United States-Israel Binational Science Foundation","doi-asserted-by":"crossref","award":["2016260"],"award-info":[{"award-number":["2016260"]}],"id":[{"id":"10.13039\/501100001742","id-type":"DOI","asserted-by":"crossref"}]},{"name":"The Pazy Foundation","award":["347719737"],"award-info":[{"award-number":["347719737"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>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.<\/jats:p>\n          <jats:p>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.<\/jats:p>","DOI":"10.1145\/3158136","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":135,"title":["Online detection of effectively callback free objects with applications to smart contracts"],"prefix":"10.1145","volume":"2","author":[{"given":"Shelly","family":"Grossman","sequence":"first","affiliation":[{"name":"Tel Aviv University, Israel"}]},{"given":"Ittai","family":"Abraham","sequence":"additional","affiliation":[{"name":"VMware, USA"}]},{"given":"Guy","family":"Golan-Gueta","sequence":"additional","affiliation":[{"name":"VMware, USA"}]},{"given":"Yan","family":"Michalevsky","sequence":"additional","affiliation":[{"name":"Stanford University, USA"}]},{"given":"Noam","family":"Rinetzky","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel \/ VMware, USA"}]},{"given":"Yoni","family":"Zohar","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"2017. Validity Labs. https:\/\/validitylabs.org . [Online].  2017. Validity Labs. https:\/\/validitylabs.org . [Online]."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39038-8_16"},{"key":"e_1_2_2_3_1","volume-title":"Ethereum Asset Platform. https:\/\/www.ambisafe.co\/ . [Online","year":"2017","unstructured":"Ambisafe. 2017. Ethereum Asset Platform. https:\/\/www.ambisafe.co\/ . [Online ; accessed 1- July - 2017 ]. Ambisafe. 2017. Ethereum Asset Platform. https:\/\/www.ambisafe.co\/ . [Online; accessed 1-July-2017]."},{"key":"e_1_2_2_4_1","unstructured":"B9Lab. 2017. ING hack challenge. [Online].  B9Lab. 2017. ING hack challenge. [Online]."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1101821.1101824"},{"key":"e_1_2_2_6_1","volume-title":"Concurrency Control and Recovery in Database Systems","author":"Bernstein Philip A.","unstructured":"Philip A. Bernstein , Vassos Hadzilacos , and Nathan Goodman . 1987. Concurrency Control and Recovery in Database Systems . Addison-Wesley . Philip A. Bernstein, Vassos Hadzilacos, and Nathan Goodman. 1987. Concurrency Control and Recovery in Database Systems. Addison-Wesley."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2993600.2993611"},{"key":"e_1_2_2_8_1","volume-title":"The DAO ETC Drains. https:\/\/github.com\/bokkypoobah\/TheDAOETCDrains . [Online","author":"Consulting Bok","year":"2017","unstructured":"Bok Consulting . 2016a. The DAO ETC Drains. https:\/\/github.com\/bokkypoobah\/TheDAOETCDrains . [Online ; accessed 2- July - 2017 ]. Bok Consulting. 2016a. The DAO ETC Drains. https:\/\/github.com\/bokkypoobah\/TheDAOETCDrains . [Online; accessed 2-July-2017]."},{"key":"e_1_2_2_9_1","volume-title":"Ethereum Network Attacker\u2019s IP Address Is Traceable. https:\/\/www.bokconsulting.com.au\/blog\/ ethereum-network-attackers-ip-address-is-traceable\/ . [Online","author":"Consulting Bok","year":"2017","unstructured":"Bok Consulting . 2016b. Ethereum Network Attacker\u2019s IP Address Is Traceable. https:\/\/www.bokconsulting.com.au\/blog\/ ethereum-network-attackers-ip-address-is-traceable\/ . [Online ; accessed 30- June - 2017 ]. Bok Consulting. 2016b. Ethereum Network Attacker\u2019s IP Address Is Traceable. https:\/\/www.bokconsulting.com.au\/blog\/ ethereum-network-attackers-ip-address-is-traceable\/ . [Online; accessed 30-June-2017]."},{"key":"e_1_2_2_10_1","volume-title":"Reachability analysis of pushdown automata: Application to model-checking. CONCUR\u201997: Concurrency Theory","author":"Bouajjani Ahmed","year":"1997","unstructured":"Ahmed Bouajjani , Javier Esparza , and Oded Maler . 1997. Reachability analysis of pushdown automata: Application to model-checking. CONCUR\u201997: Concurrency Theory ( 1997 ), 135\u2013150. Ahmed Bouajjani, Javier Esparza, and Oded Maler. 1997. Reachability analysis of pushdown automata: Application to model-checking. CONCUR\u201997: Concurrency Theory (1997), 135\u2013150."},{"key":"e_1_2_2_11_1","volume-title":"CRITICAL UPDATE Re: DAO Vulnerability. https:\/\/blog.ethereum.org\/2016\/06\/17\/ critical-update-re-dao-vulnerability\/ . [Online","author":"Buterin Vitalik","year":"2017","unstructured":"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 ]. 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]."},{"key":"e_1_2_2_12_1","unstructured":"Phil Daian. 2016. (2016). http:\/\/hackingdistributed.com\/2016\/06\/18\/analysis-of-the-dao-exploit\/  Phil Daian. 2016. (2016). http:\/\/hackingdistributed.com\/2016\/06\/18\/analysis-of-the-dao-exploit\/"},{"key":"e_1_2_2_13_1","first-page":"460","article-title":"Step by Step Towards Creating a Safe Smart Contract: Lessons and Insights from a Cryptocurrency Lab","volume":"2015","author":"Delmolino Kevin","year":"2015","unstructured":"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 . 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.","journal-title":"IACR Cryptology ePrint Archive"},{"key":"e_1_2_2_14_1","volume-title":"Ethereum - Serpent Tutorial and Smart Contract Lab. https:\/\/github.com\/mc2-umd\/ethereumlab\/blob\/master\/Examples\/RPS_v2_new.py . [Online","author":"Delmolino Kevin","year":"2017","unstructured":"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 ]. 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]."},{"key":"e_1_2_2_15_1","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","unstructured":"Edsger W. Dijkstra . 1976. A Discipline of Programming . Prentice-Hall . Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall."},{"key":"e_1_2_2_16_1","volume-title":"https:\/\/etcchain.com\/ . [Online","author":"Classic Ethereum","year":"2017","unstructured":"Ethereum Classic . 2017. Ethereum Classic . https:\/\/etcchain.com\/ . [Online ; accessed 2- July - 2017 ]. Ethereum Classic. 2017. Ethereum Classic. https:\/\/etcchain.com\/ . [Online; accessed 2-July-2017]."},{"key":"e_1_2_2_17_1","volume-title":"https:\/\/github.com\/ethereum\/go-ethereum\/wiki\/geth . [Online","author":"Foundation Ethereum","year":"2017","unstructured":"Ethereum Foundation . 2017a. Geth. https:\/\/github.com\/ethereum\/go-ethereum\/wiki\/geth . [Online ; accessed 30- June - 2017 ]. Ethereum Foundation. 2017a. Geth. https:\/\/github.com\/ethereum\/go-ethereum\/wiki\/geth . [Online; accessed 30-June-2017]."},{"key":"e_1_2_2_18_1","volume-title":"https:\/\/solidity.readthedocs.io\/en\/develop\/ . [Online","author":"Foundation Ethereum","year":"2017","unstructured":"Ethereum Foundation . 2017b. Solidity. https:\/\/solidity.readthedocs.io\/en\/develop\/ . [Online ; accessed 5- July - 2017 ]. Ethereum Foundation. 2017b. Solidity. https:\/\/solidity.readthedocs.io\/en\/develop\/ . [Online; accessed 5-July-2017]."},{"key":"e_1_2_2_19_1","unstructured":"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].  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]."},{"key":"e_1_2_2_20_1","volume-title":"https:\/\/etherscan.io\/address\/ 0xbfbea57d87e15529a30b6634c1c13f1a12fa4d09 . [Online","year":"2017","unstructured":"Etherscan. 2017. 0xbfBeA57d87E15529a30B6634C1C13F1A12Fa4d09. https:\/\/etherscan.io\/address\/ 0xbfbea57d87e15529a30b6634c1c13f1a12fa4d09 . [Online ; accessed 1- July - 2017 ]. Etherscan. 2017. 0xbfBeA57d87E15529a30B6634C1C13F1A12Fa4d09. https:\/\/etherscan.io\/address\/ 0xbfbea57d87e15529a30b6634c1c13f1a12fa4d09 . [Online; accessed 1-July-2017]."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22012-8_36"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_2_2_24_1","unstructured":"J.E. Hopcroft R. Motwani and J.D. Ullman. 2006. Introduction to automata theory languages and computation. Addisonwesley.  J.E. Hopcroft R. Motwani and J.D. Ullman. 2006. Introduction to automata theory languages and computation. Addisonwesley."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_2_27_1","volume-title":"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\u201342","author":"K. Rustan","unstructured":"K. Rustan M. Leino and Peter M\u00fcller. 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\u201342 . K. Rustan M. Leino and Peter M\u00fcller. 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\u201342."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/570886.570888"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2005.01.001"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_2_2_31_1","volume-title":"https:\/\/oyente.melonport.com . [Online","year":"2017","unstructured":"Melonport. 2017. Oyente. https:\/\/oyente.melonport.com . [Online ; accessed 6- July - 2017 ]. Melonport. 2017. Oyente. https:\/\/oyente.melonport.com . [Online; accessed 6-July-2017]."},{"key":"e_1_2_2_32_1","volume-title":"Bitcoin: A peer-to-peer electronic cash system. https:\/\/bitcoin.org\/bitcoin.pdf .","author":"Nakamoto Satoshi","year":"2008","unstructured":"Satoshi Nakamoto . 2008 . Bitcoin: A peer-to-peer electronic cash system. https:\/\/bitcoin.org\/bitcoin.pdf . Satoshi Nakamoto. 2008. Bitcoin: A peer-to-peer electronic cash system. https:\/\/bitcoin.org\/bitcoin.pdf ."},{"key":"e_1_2_2_33_1","volume-title":"The rise of the Dark DAO. https:\/\/medium.com\/@oaeee\/the-rise-of-the-dark-dao-72b21a2212e3 . [Online","author":"Pfeffer Johannes","year":"2017","unstructured":"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 ]. 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]."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384716.2384720"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70278-0_30"},{"key":"e_1_2_2_36_1","unstructured":"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].  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]."},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.5210\/fm.v2i9.548"},{"key":"e_1_2_2_38_1","unstructured":"Validity Labs. 2017. Recursive call exploit. [Online].  Validity Labs. 2017. Recursive call exploit. [Online]."},{"key":"e_1_2_2_39_1","unstructured":"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].  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]."},{"key":"e_1_2_2_40_1","volume-title":"Ethereum: A Secure Decentralised Generalised Transaction Ledger","author":"Wood Gavin","year":"2016","unstructured":"Gavin Wood . 2016 . Ethereum: A Secure Decentralised Generalised Transaction Ledger . http:\/\/gavwood.com\/paper.pdf . [Online; accessed 5-July-2017]. Gavin Wood. 2016. Ethereum: A Secure Decentralised Generalised Transaction Ledger. http:\/\/gavwood.com\/paper.pdf . [Online; accessed 5-July-2017]."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158136","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158136","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158136"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":40,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158136"],"URL":"https:\/\/doi.org\/10.1145\/3158136","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}