{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,15]],"date-time":"2026-10-15T18:06:02Z","timestamp":1792087562797,"version":"4.4.0"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,10,10]]},"abstract":"<jats:p>The term \u201csmart contracts\u201d has become ubiquitous to describe an enormous number of programs uploaded to the popular Ethereum blockchain system. Despite rapid growth of the smart contract ecosystem, errors and exploitations have been constantly reported from online contract systems, which has put financial stability at risk with losses totaling millions of US dollars. Most existing research focuses on pinpointing specific types of vulnerabilities using known patterns. However, due to the lack of awareness of the inherent nondeterminism in the Ethereum blockchain system and how it affects the funds transfer of smart contracts, there can be unknown vulnerabilities that may be exploited by attackers to access numerous online smart contracts.<\/jats:p>\n          <jats:p>In this paper, we introduce a methodical approach to understanding the inherent nondeterminism in the Ethereum blockchain system and its (unwanted) influence on contract payments. We show that our new focus on nondeterminism-related smart contract payment bugs captures the root causes of many common vulnerabilities without relying on any known patterns and also encompasses recently disclosed issues that are not handled by existing research. To do so, we introduce techniques to systematically model components in the contract execution context and to expose various nondeterministic factors that are not yet fully understood. We further study how these nondeterministic factors impact contract funds transfer using information flow tracking. The technical challenge of detecting nondeterministic payments lies in discovering the contract global variables subtly affected by read-write hazards because of unpredictable transaction scheduling and external callee behavior. We show how to augment and instrument a contract program into a representation that simulates the execution of a large subset of the contract behavior. The instrumented code is then analyzed to flag nondeterministic global variables using off-the-shelf model checkers.<\/jats:p>\n          <jats:p>We implement the proposed techniques as a practical tool named NPChecker (Nondeterministic Payment Checker) and evaluate it on 30K online contracts (3,075 distinct) collected from the Ethereum mainnet. NPChecker has successfully detected nondeterministic payments in 1,111 online contracts with reasonable cost. Further investigation reports high precision of NPChecker (only four false positives in a manual study of 50 contracts). We also show that NPChecker unveils contracts vulnerable to recently-disclosed attack vectors. NPChecker can identify all six new vulnerabilities or variants of common smart contract vulnerabilities that are missed by existing research relying on a \u201ccontract vulnerability checklist.\u201d<\/jats:p>","DOI":"10.1145\/3360615","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":78,"title":["Detecting nondeterministic payment bugs in Ethereum smart contracts"],"prefix":"10.1145","volume":"3","author":[{"given":"Shuai","family":"Wang","sequence":"first","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chengyu","family":"Zhang","sequence":"additional","affiliation":[{"name":"East China Normal University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhendong","family":"Su","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"2018. Etherscan.IO. https:\/\/etherscan.io .  2018. Etherscan.IO. https:\/\/etherscan.io ."},{"key":"e_1_2_1_2_1","unstructured":"2018a. EVMJIT. https:\/\/github.com\/ethereum\/evmjit .  2018a. EVMJIT. https:\/\/github.com\/ethereum\/evmjit ."},{"key":"e_1_2_1_3_1","unstructured":"2018b. Known Attacks of Ethereum Smart Contract. https:\/\/consensys.github.io\/smart-contract-best-practices\/known_ attacks\/ .  2018b. Known Attacks of Ethereum Smart Contract. https:\/\/consensys.github.io\/smart-contract-best-practices\/known_ attacks\/ ."},{"key":"e_1_2_1_4_1","unstructured":"2019. Provable: Provable T M Random Number Generator. http:\/\/provable.xyz\/ .  2019. Provable: Provable T M Random Number Generator. http:\/\/provable.xyz\/ ."},{"key":"e_1_2_1_5_1","unstructured":"2019. RANDAO: A DAO working as RNG of Ethereum. https:\/\/github.com\/randao\/randao\/blob\/master\/README.md .  2019. RANDAO: A DAO working as RNG of Ethereum. https:\/\/github.com\/randao\/randao\/blob\/master\/README.md ."},{"key":"e_1_2_1_6_1","unstructured":"2019. Securify Git Issues. https:\/\/github.com\/eth-sri\/securify\/issues\/98 .  2019. Securify Git Issues. https:\/\/github.com\/eth-sri\/securify\/issues\/98 ."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167084"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2993600.2993611"},{"key":"e_1_2_1_9_1","unstructured":"ChainSecurity. 2019. Constantinople enables new Reentrancy Attack. https:\/\/medium.com\/chainsecurity\/constantinopleenables-new-reentrancy-attack-ace4088297d9 .  ChainSecurity. 2019. Constantinople enables new Reentrancy Attack. https:\/\/medium.com\/chainsecurity\/constantinopleenables-new-reentrancy-attack-ace4088297d9 ."},{"key":"e_1_2_1_10_1","unstructured":"Code4Block. 2018. CVE List Found by Team Code4Block. https:\/\/github.com\/TEAM-C4B\/CVE-LIST .  Code4Block. 2018. CVE List Found by Team Code4Block. https:\/\/github.com\/TEAM-C4B\/CVE-LIST ."},{"key":"e_1_2_1_11_1","unstructured":"ConsenSys. 2018. Mythril Classic. https:\/\/github.com\/ConsenSys\/mythril-classic .  ConsenSys. 2018. Mythril Classic. https:\/\/github.com\/ConsenSys\/mythril-classic ."},{"key":"e_1_2_1_12_1","unstructured":"Yu Feng Emina Torlak and Rastislav Bodik. 2019. Precise Attack Synthesis for Smart Contracts. arXiv: cs.CR\/1902.06067  Yu Feng Emina Torlak and Rastislav Bodik. 2019. Precise Attack Synthesis for Smart Contracts. arXiv: cs.CR\/1902.06067"},{"key":"e_1_2_1_13_1","unstructured":"Geth. 2018. Go Ethereum. https:\/\/geth.ethereum.org\/downloads\/ .  Geth. 2018. Go Ethereum. https:\/\/geth.ethereum.org\/downloads\/ ."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276486"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89722-6_10"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (Lecture Notes in Computer Science)","author":"Haran Arvind","unstructured":"Arvind Haran , Montgomery Carter , Michael Emmi , Akash Lal , Shaz Qadeer , and Zvonimir Rakamari\u0107 . 2015. SMACK+Corral : A Modular Verifier (Competition Contribution) . In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (Lecture Notes in Computer Science) , Christel Baier and Cesare Tinelli (Eds.), Vol. 9035 . Springer , 450\u2013453. Arvind Haran, Montgomery Carter, Michael Emmi, Akash Lal, Shaz Qadeer, and Zvonimir Rakamari\u0107. 2015. SMACK+Corral: A Modular Verifier (Competition Contribution). In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (Lecture Notes in Computer Science), Christel Baier and Cesare Tinelli (Eds.), Vol. 9035. Springer, 450\u2013453."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00022"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70278-0_33"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238177"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2018.23082"},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Aashish Kolluri Ivica Nikolic Ilya Sergey Aquinas Hobor and Prateek Saxena. 2018. Exploiting The Laws of Order in Smart Contracts. arXiv: cs.CR\/1810.11605  Aashish Kolluri Ivica Nikolic Ilya Sergey Aquinas Hobor and Prateek Saxena. 2018. Exploiting The Laws of Order in Smart Contracts. arXiv: cs.CR\/1810.11605","DOI":"10.1145\/3293882.3330560"},{"key":"e_1_2_1_22_1","volume-title":"27th USENIX Security Symposium (USENIX Security 18)","author":"Krupp Johannes","year":"2018","unstructured":"Johannes Krupp and Christian Rossow . 2018 . teEther: Gnawing at Ethereum to Automatically Exploit Smart Contracts . In 27th USENIX Security Symposium (USENIX Security 18) . USENIX Association, 1317\u20131333. Johannes Krupp and Christian Rossow. 2018. teEther: Gnawing at Ethereum to Automatically Exploit Smart Contracts. In 27th USENIX Security Symposium (USENIX Security 18). USENIX Association, 1317\u20131333."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_38"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89722-6_11"},{"key":"e_1_2_1_26_1","volume-title":"Bitcoin: A peer-to-peer electronic cash system.","author":"Satoshi Nakamoto","year":"2008","unstructured":"Satoshi Nakamoto et al. 2008 . Bitcoin: A peer-to-peer electronic cash system. (2008). Satoshi Nakamoto et al. 2008. Bitcoin: A peer-to-peer electronic cash system. (2008)."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274743"},{"key":"e_1_2_1_28_1","unstructured":"Daniel Perez and Benjamin Livshits. 2019. Smart Contract Vulnerabilities: Does Anyone Care? arXiv: cs.CR\/1902.06710  Daniel Perez and Benjamin Livshits. 2019. Smart Contract Vulnerabilities: Does Anyone Care? arXiv: cs.CR\/1902.06710"},{"key":"e_1_2_1_29_1","unstructured":"PNF. 2018. JEB Decompiler. https:\/\/www.pnfsoftware.com\/ .  PNF. 2018. JEB Decompiler. https:\/\/www.pnfsoftware.com\/ ."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996845"},{"key":"e_1_2_1_31_1","volume-title":"SMACK: Decoupling Source Language Details from Verifier Implementations","author":"Rakamari\u0107 Zvonimir","year":"2014","unstructured":"Zvonimir Rakamari\u0107 and Michael Emmi . 2014 . SMACK: Decoupling Source Language Details from Verifier Implementations . In Computer Aided Verification, Armin Biere and Roderick Bloem (Eds.). 106\u2013113. Zvonimir Rakamari\u0107 and Michael Emmi. 2014. SMACK: Decoupling Source Language Details from Verifier Implementations. In Computer Aided Verification, Armin Biere and Roderick Bloem (Eds.). 106\u2013113."},{"key":"e_1_2_1_32_1","volume-title":"Sereum: Protecting Existing Smart Contracts Against Re-Entrancy Attacks. CoRR abs\/1812.05934","author":"Rodler Michael","year":"2018","unstructured":"Michael Rodler , Wenting Li , Ghassan O. Karame , and Lucas Davi . 2018 . Sereum: Protecting Existing Smart Contracts Against Re-Entrancy Attacks. CoRR abs\/1812.05934 (2018). Michael Rodler, Wenting Li, Ghassan O. Karame, and Lucas Davi. 2018. Sereum: Protecting Existing Smart Contracts Against Re-Entrancy Attacks. CoRR abs\/1812.05934 (2018)."},{"key":"e_1_2_1_33_1","unstructured":"SECBIT. 2018. Awesome Buggy ERC20 Tokens. https:\/\/github.com\/sec-bit\/awesome-buggy-erc20-tokens .  SECBIT. 2018. Awesome Buggy ERC20 Tokens. https:\/\/github.com\/sec-bit\/awesome-buggy-erc20-tokens ."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70278-0_30"},{"key":"e_1_2_1_35_1","unstructured":"David Siegel. 2016. Understanding The DAO Attack. https:\/\/www.coindesk.com\/understanding-dao-hack-journalists .  David Siegel. 2016. Understanding The DAO Attack. https:\/\/www.coindesk.com\/understanding-dao-hack-journalists ."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243780"},{"key":"e_1_2_1_37_1","unstructured":"D. Wood. 2014. Ethereum: a secure decentralised generalised transaction ledger.  D. Wood. 2014. Ethereum: a secure decentralised generalised transaction ledger."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360615","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360615","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:59Z","timestamp":1750202579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360615"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":37,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360615"],"URL":"https:\/\/doi.org\/10.1145\/3360615","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}