{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,24]],"date-time":"2026-03-24T03:11:01Z","timestamp":1774321861448,"version":"3.50.1"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T00:00:00Z","timestamp":1605225600000},"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":[[2020,11,13]]},"abstract":"<jats:p>Static analysis of smart contracts as-deployed on the Ethereum blockchain has received much recent attention. However, high-precision analyses currently face significant challenges when dealing with the Ethereum VM (EVM) execution model. A major such challenge is the modeling of low-level, transient \u201cmemory\u201d (as opposed to persistent, on-blockchain \u201cstorage\u201d) that smart contracts employ. Statically understanding the usage patterns of memory is non-trivial, due to the dynamic allocation nature of in-memory buffers. We offer an analysis that models EVM memory, recovering high-level concepts (e.g., arrays, buffers, call arguments) via deep modeling of the flow of values. Our analysis opens the door to Ethereum static analyses with drastically increased precision. One such analysis detects the extraction of ERC20 tokens by unauthorized users. For another practical vulnerability (redundant calls, possibly used as an attack vector), our memory modeling yields analysis precision of 89%, compared to 16% for a state-of-the-art tool without precise memory modeling. Additionally, precise memory modeling enables the static computation of a contract\u2019s gas cost. This gas-cost analysis has recently been instrumental in the evaluation of the impact of the EIP-1884 repricing (in terms of gas costs) of EVM operations, leading to a reward and significant publicity from the Ethereum Foundation.<\/jats:p>","DOI":"10.1145\/3428258","type":"journal-article","created":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:36:06Z","timestamp":1606260966000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Precise static modeling of Ethereum \u201cmemory\u201d"],"prefix":"10.1145","volume":"4","author":[{"given":"Sifis","family":"Lagouvardos","sequence":"first","affiliation":[{"name":"University of Athens, Greece"}]},{"given":"Neville","family":"Grech","sequence":"additional","affiliation":[{"name":"University of Athens, Greece"}]},{"given":"Ilias","family":"Tsatiris","sequence":"additional","affiliation":[{"name":"University of Athens, Greece"}]},{"given":"Yannis","family":"Smaragdakis","sequence":"additional","affiliation":[{"name":"University of Athens, Greece"}]}],"member":"320","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Automated Technology for Verification and Analysis (ATVA)","author":"Albert Elvira"},{"key":"e_1_2_2_2_1","volume-title":"Ethainter: A Smart Contract Security Analyzer for Composite Vulnerabilities. In Conf. on Programming Language Design and Implementation (PLDI). ACM.","author":"Brent Lexi","year":"2020"},{"key":"e_1_2_2_3_1","volume-title":"Vandal: A Scalable Security Analysis Framework for Smart Contracts. arXiv:cs.PL\/","author":"Brent Lexi","year":"2018"},{"key":"e_1_2_2_4_1","unstructured":"ChainSecurity. 2019. Dangerous Repeated Calls to Untrusted Contracts. https:\/\/medium.com\/chainsecurity\/dangerousrepeated-calls-to-untrusted-contracts-3c97d614744b  ChainSecurity. 2019. Dangerous Repeated Calls to Untrusted Contracts. https:\/\/medium.com\/chainsecurity\/dangerousrepeated-calls-to-untrusted-contracts-3c97d614744b"},{"key":"e_1_2_2_5_1","unstructured":"ChainSecurity. 2020. Securify2. https:\/\/github.com\/eth-sri\/ securify2  ChainSecurity. 2020. Securify2. https:\/\/github.com\/eth-sri\/ securify2"},{"key":"e_1_2_2_6_1","unstructured":"ConsenSys. 2020. ConsenSys Quorum. https:\/\/consensys.net\/quorum\/  ConsenSys. 2020. ConsenSys Quorum. https:\/\/consensys.net\/quorum\/"},{"key":"e_1_2_2_7_1","unstructured":"Dedaub. 2019. Contract Library. https:\/\/contract-library.com\/  Dedaub. 2019. Contract Library. https:\/\/contract-library.com\/"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/WETSEB.2019.00008"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00120"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2764967.2764974"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276486"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363230"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00022"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238177"},{"key":"e_1_2_2_15_1","volume-title":"Soufl\u00e9: On Synthesis of Program Analyzers","author":"Jordan Herbert","year":"2016"},{"key":"e_1_2_2_16_1","unstructured":"Tomasz Kolinko. 2018. Eveem\/Panoramix-Showing Contract Sources since 2018. http:\/\/eveem.org\/  Tomasz Kolinko. 2018. Eveem\/Panoramix-Showing Contract Sources since 2018. http:\/\/eveem.org\/"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330560"},{"key":"e_1_2_2_18_1","first-page":"1317","volume-title":"27th USENIX Security Symposium (USENIX Security 18)","author":"Krupp Johannes","year":"2018"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4059797"},{"key":"e_1_2_2_20_1","unstructured":"Adam Levi. 2019. A Technical Analysis of the Genesis Alpha Hack. https:\/\/medium.com\/daostack\/a-technical-analysis-ofthe-genesis-alpha-hack-f8e34433c14b  Adam Levi. 2019. A Technical Analysis of the Genesis Alpha Hack. https:\/\/medium.com\/daostack\/a-technical-analysis-ofthe-genesis-alpha-hack-f8e34433c14b"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_2_2_22_1","doi-asserted-by":"crossref","unstructured":"Anastasia Mavridou and Aron Laszka. 2018. Designing Secure Ethereum Smart Contracts: A Finite State Machine Based Approach. http:\/\/aronlaszka.com\/papers\/mavridou2018designing.pdf  Anastasia Mavridou and Aron Laszka. 2018. Designing Secure Ethereum Smart Contracts: A Finite State Machine Based Approach. http:\/\/aronlaszka.com\/papers\/mavridou2018designing.pdf","DOI":"10.1007\/978-3-662-58387-6_28"},{"key":"e_1_2_2_23_1","volume-title":"Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts. arXiv e-prints, Article arXiv","author":"Mossberg Mark","year":"2019"},{"key":"e_1_2_2_24_1","volume-title":"Smashing Ethereum Smart Contracts for Fun and Real Profit. https:\/\/github.com\/b-mueller\/ smashing-smart-contracts\/raw\/master\/smashing-smart-contracts-1of1.pdf The 9th annual HITB Security Conference","author":"Mueller Bernhard"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274743"},{"key":"e_1_2_2_26_1","doi-asserted-by":"crossref","unstructured":"Anton Permenev Dimitar Dimitrov Petar Tsankov Dana Drachsler-Cohen and Martin Vechev. 2019. VerX: Safety Verification of Smart Contracts. https:\/\/files.sri.inf.ethz.ch\/website\/papers\/sp20-verx.pdf.  Anton Permenev Dimitar Dimitrov Petar Tsankov Dana Drachsler-Cohen and Martin Vechev. 2019. VerX: Safety Verification of Smart Contracts. https:\/\/files.sri.inf.ethz.ch\/website\/papers\/sp20-verx.pdf.","DOI":"10.1109\/SP40000.2020.00024"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3359591.3359739"},{"key":"e_1_2_2_28_1","unstructured":"Martin Holst Swende. 2019. Security considerations for EIP-1884. URLomittedforanonymity canbesearchedbasedontitle  Martin Holst Swende. 2019. Security considerations for EIP-1884. URLomittedforanonymity canbesearchedbasedontitle"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243780"},{"key":"e_1_2_2_30_1","unstructured":"Various. 2015. Hyperledger \u00e2\u0102\u015e\u00c2\u0103Open Source Blockchain Technologies. https:\/\/www.hyperledger.org\/  Various. 2015. Hyperledger \u00e2\u0102\u015e\u00c2\u0103Open Source Blockchain Technologies. https:\/\/www.hyperledger.org\/"},{"key":"e_1_2_2_31_1","unstructured":"Various. 2018. Rattle-An EVM Binary Static Analysis Framework. https:\/\/github.com\/trailofbits\/rattle  Various. 2018. Rattle-An EVM Binary Static Analysis Framework. https:\/\/github.com\/trailofbits\/rattle"},{"key":"e_1_2_2_32_1","unstructured":"Various. 2018. TRON Decentralize The Web. https:\/\/tron.network\/  Various. 2018. TRON Decentralize The Web. https:\/\/tron.network\/"},{"key":"e_1_2_2_33_1","unstructured":"Various. 2019. GitHub-ewasm design-metering. https:\/\/github.com\/ewasm\/design\/blob\/master\/metering.md  Various. 2019. GitHub-ewasm design-metering. https:\/\/github.com\/ewasm\/design\/blob\/master\/metering.md"},{"key":"e_1_2_2_34_1","volume-title":"Targeted Greybox Fuzzing with Static Lookahead Analysis. In International Conference on Software Engineering (ICSE).","author":"W\u00c3\u0133stholz Valentin","year":"2020"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428258","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428258","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:57Z","timestamp":1750197777000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428258"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,13]]},"references-count":34,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2020,11,13]]}},"alternative-id":["10.1145\/3428258"],"URL":"https:\/\/doi.org\/10.1145\/3428258","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11,13]]},"assertion":[{"value":"2020-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}