{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:29:50Z","timestamp":1770276590697,"version":"3.49.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031377082","type":"print"},{"value":"9783031377099","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T00:00:00Z","timestamp":1689552000000},"content-version":"vor","delay-in-days":197,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The efficiency and the security of <jats:italic>smart contracts<\/jats:italic> are their two fundamental properties, but might come at odds: the use of optimizers to enhance efficiency may introduce bugs and compromise security. Our focus is on  (Ethereum Virtual Machine) <jats:italic>block-optimizations<\/jats:italic>, which enhance the efficiency of jump-free blocks of opcodes by eliminating, reordering and even changing the original opcodes. We reconcile efficiency and security by providing the verification technology to formally prove the correctness of  block-optimizations on smart contracts using the Coq proof assistant. This amounts to the challenging problem of proving semantic equivalence of two blocks of  instructions, which is realized by means of three novel Coq components: a symbolic execution engine which can execute an  block and produce a symbolic state; a number of simplification lemmas which transform a symbolic state into an equivalent one; and a checker of symbolic states to compare the symbolic states produced for the two  blocks under comparison.<\/jats:p><jats:p><jats:bold>Artifact:<\/jats:bold><jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" ext-link-type=\"uri\" xlink:href=\"https:\/\/doi.org\/10.5281\/zenodo.7863483\">https:\/\/doi.org\/10.5281\/zenodo.7863483<\/jats:ext-link><\/jats:p>","DOI":"10.1007\/978-3-031-37709-9_9","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"176-189","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Formally Verified EVM Block-Optimizations"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0048-0705","authenticated-orcid":false,"given":"Elvira","family":"Albert","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7176-1881","authenticated-orcid":false,"given":"Samir","family":"Genaim","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9229-1148","authenticated-orcid":false,"given":"Daniel","family":"Kirchner","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1664-018X","authenticated-orcid":false,"given":"Enrique","family":"Martin-Martin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,17]]},"reference":[{"key":"9_CR1","unstructured":"https:\/\/www.certora.com\/"},{"key":"9_CR2","unstructured":"https:\/\/veridise.com\/"},{"key":"9_CR3","unstructured":"https:\/\/www.apriorit.com\/"},{"key":"9_CR4","unstructured":"https:\/\/consensys.net\/"},{"key":"9_CR5","unstructured":"https:\/\/www.dedaub.com\/"},{"key":"9_CR6","unstructured":"https:\/\/github.com\/ethereum\/solidity\/tree\/develop\/test\/libsolidity\/semanticTests\/externalContracts"},{"key":"9_CR7","unstructured":"Bedrock Bit Vectors (bbv) (2018). https:\/\/github.com\/mit-plv\/bbv"},{"key":"9_CR8","unstructured":"PausableERC20 Contract (2020). https:\/\/etherscan.io\/address\/0x32E6C34Cd57087aBBD59B5A4AECC4cB495924356"},{"key":"9_CR9","unstructured":"The solc optimizer (2021). https:\/\/docs.soliditylang.org\/en\/v0.8.7\/internals\/optimizer.html"},{"key":"9_CR10","unstructured":"Albert, E., Genaim, S., Kirchner, D., Martin-Martin, E.: Formally Verified EVM Block-Optimizations (Extended Version). https:\/\/costa.fdi.ucm.es\/papers\/costa\/AlbertGKMM23_extended.pdf"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-030-99524-9_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Albert","year":"2022","unstructured":"Albert, E., Gordillo, P., Hern\u00e1ndez-Cerezo, A., Rubio, A.: A Max-SMT superoptimizer for EVM handling memory and storage. In: TACAS 2022. LNCS, vol. 13243, pp. 201\u2013219. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_11"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-030-53288-8_10","volume-title":"Computer Aided Verification","author":"E Albert","year":"2020","unstructured":"Albert, E., Gordillo, P., Rubio, A., Schett, M.A.: Synthesis of super-optimized smart contracts using max-SMT. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 177\u2013200. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_10"},{"key":"9_CR13","doi-asserted-by":"publisher","unstructured":"Barri\u00e8re, A., Blazy, S., Fl\u00fcckiger, O., Pichardie, D., Vitek, J.: Formally verified speculation and deoptimization in a JIT compiler. Proc. ACM Program. Lang. 5(POPL), 1\u201326 (2021). https:\/\/doi.org\/10.1145\/3434327","DOI":"10.1145\/3434327"},{"key":"9_CR14","unstructured":"Bernardi, T., et al.: Preventing reentrancy bugs - another use case for formal verification (2020). https:\/\/www.certora.com\/blog\/reentrancy.html"},{"key":"9_CR15","unstructured":"Bizga, A.: A hackers\u2019 dream payday: Ledf.me and uniswap lose \\$25 million worth of cryptocurrency (2020). https:\/\/securityboulevard.com\/2020\/04\/a-hackers-dream-payday-ledf-me-and-uniswap-lose-25-million-worth-of-cryptocurrency\/. [Online; accessed 11-May-2020]"},{"key":"9_CR16","unstructured":"Buterin, V.: CRITICAL UPDATE Re: DAO vulnerability (2016). https:\/\/blog.ethereum.org\/2016\/06\/17\/critical-update-re-dao-vulnerability\/. Accessed 2-July-2017"},{"key":"9_CR17","unstructured":"Daian, P.: Analysis of the DAO exploit (2016). http:\/\/hackingdistributed.com\/2016\/06\/18\/analysis-of-the-dao-exploit\/"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-662-46663-6_12","volume-title":"Compiler Construction","author":"D Demange","year":"2015","unstructured":"Demange, D., Pichardie, D., Stefanesco, L.: Verifying fast and sparse SSA-based optimizations in Coq. In: Franke, B. (ed.) CC 2015. LNCS, vol. 9031, pp. 233\u2013252. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46663-6_12"},{"key":"9_CR19","unstructured":"elexcere: SGT and GT order when parsing. https:\/\/github.com\/costa-group\/gasol-optimizer\/commit\/fd78e126c23f192ed6c54aea713b5c94d3c943f5"},{"key":"9_CR20","unstructured":"Gourdin, L., Boulm\u00e9, S.: Certifying assembly optimizations in Coq by symbolic execution with hash-consing, p. 2 (2021)"},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Hildenbrandt, E., et al.: KEVM: a complete formal semantics of the ethereum virtual machine. In: 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9\u201312, 2018, pp. 204\u2013217. IEEE Computer Society (2018). https:\/\/doi.org\/10.1109\/CSF.2018.00022","DOI":"10.1109\/CSF.2018.00022"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"520","DOI":"10.1007\/978-3-319-70278-0_33","volume-title":"Financial Cryptography and Data Security","author":"Y Hirai","year":"2017","unstructured":"Hirai, Y.: Defining the ethereum virtual machine for interactive theorem provers. In: Brenner, M., Rohloff, K., Bonneau, J., Miller, A., Ryan, P.Y.A., Teague, V., Bracciali, A., Sala, M., Pintore, F., Jakobsson, M. (eds.) FC 2017. LNCS, vol. 10323, pp. 520\u2013535. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-70278-0_33"},{"key":"9_CR23","unstructured":"ivan71kmayshan27: Coq formalisation of the Ethereum Virtual Machine (WIP) (2020). https:\/\/github.com\/ivan71kmayshan27\/coq-evm"},{"key":"9_CR24","doi-asserted-by":"publisher","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009). https:\/\/doi.org\/10.1145\/1538788.1538814","DOI":"10.1145\/1538788.1538814"},{"issue":"2","key":"9_CR25","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/3166064","volume":"61","author":"NP Lopes","year":"2018","unstructured":"Lopes, N.P., Menendez, D., Nagarakatte, S., Regehr, J.: Practical verification of peephole optimizations with alive. Commun. ACM 61(2), 84\u201391 (2018). https:\/\/doi.org\/10.1145\/3166064","journal-title":"Commun. ACM"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Massalin, H.: Superoptimizer - a look at the smallest program. In: Proceedings of the Second International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS II), pp. 122\u2013126 (1987). https:\/\/dl.acm.org\/citation.cfm?id=36194","DOI":"10.1145\/36206.36194"},{"key":"9_CR27","doi-asserted-by":"publisher","unstructured":"Monniaux, D., Six, C.: Simple, light, yet formally verified, global common subexpression elimination and loop-invariant code motion. In: Henkel, J., Liu, X. (eds.) LCTES \u201921: 22nd ACM SIGPLAN\/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems, Virtual Event, Canada, 22 June, 2021, pp. 85\u201396. ACM (2021). https:\/\/doi.org\/10.1145\/3461648.3463850","DOI":"10.1145\/3461648.3463850"},{"issue":"9","key":"9_CR28","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1145\/2692915.2628143","volume":"49","author":"DP Mulligan","year":"2014","unstructured":"Mulligan, D.P., Owens, S., Gray, K.E., Ridge, T., Sewell, P.: Lem: reusable engineering of real-world semantics. ACM SIGPLAN Notices 49(9), 175\u2013188 (2014)","journal-title":"ACM SIGPLAN Notices"},{"key":"9_CR29","unstructured":"Nagele, J., Schett, M.A.: Blockchain superoptimizer. In: Preproceedings of 29th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2019) (2019). https:\/\/arxiv.org\/abs\/2005.05912"},{"key":"9_CR30","unstructured":"Palmer, D.: Spankchain loses \\$40k in hack due to smart contract bug (2018). https:\/\/www.coindesk.com\/spankchain-loses-40k-in-hack-due-to-smart-contract-bug. Accessed 11 May 2020"},{"key":"9_CR31","unstructured":"Sasnauskas, R., et al.: Souper: A Synthesizing Superoptimizer. arXiv:1711.04422 [cs], November 2017"},{"key":"9_CR32","doi-asserted-by":"publisher","unstructured":"Six, C., Boulm\u00e9, S., Monniaux, D.: Certified and efficient instruction scheduling: application to interlocked VLIW processors. Proc. ACM Program. Lang. 4(OOPSLA), 129:1\u2013129:29 (2020). https:\/\/doi.org\/10.1145\/3428197","DOI":"10.1145\/3428197"},{"key":"9_CR33","doi-asserted-by":"publisher","unstructured":"Six, C., Gourdin, L., Boulm\u00e9, S., Monniaux, D., Fasse, J., Nardino, N.: Formally verified superblock scheduling. In: Popescu, A., Zdancewic, S. (eds.) CPP \u201922: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17\u201318, 2022, pp. 40\u201354. ACM (2022). https:\/\/doi.org\/10.1145\/3497775.3503679","DOI":"10.1145\/3497775.3503679"},{"key":"9_CR34","doi-asserted-by":"publisher","unstructured":"Tristan, J., Leroy, X.: Formal verification of translation validators: a case study on instruction scheduling optimizations. In: Necula, G.C., Wadler, P. (eds.) Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7\u201312, 2008, pp. 17\u201327. ACM (2008). https:\/\/doi.org\/10.1145\/1328438.1328444","DOI":"10.1145\/1328438.1328444"},{"key":"9_CR35","doi-asserted-by":"publisher","unstructured":"Tristan, J., Leroy, X.: Verified validation of lazy code motion. In: Hind, M., Diwan, A. (eds.) Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, Dublin, Ireland, June 15\u201321, 2009, pp. 316\u2013326. ACM (2009). https:\/\/doi.org\/10.1145\/1542476.1542512","DOI":"10.1145\/1542476.1542512"},{"key":"9_CR36","doi-asserted-by":"publisher","unstructured":"Tristan, J., Leroy, X.: A simple, verified validator for software pipelining. In: Hermenegildo, M.V., Palsberg, J. (eds.) Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17\u201323, 2010, pp. 83\u201392. ACM (2010). https:\/\/doi.org\/10.1145\/1706299.1706311","DOI":"10.1145\/1706299.1706311"},{"key":"9_CR37","unstructured":"Turley, C.: imBTC uniswap pool drained for \\$300k in ETH (2020). https:\/\/defirate.com\/imbtc-uniswap-hack\/. Accessed 11 May 2020"},{"key":"9_CR38","unstructured":"Wood, G.: Ethereum: A secure decentralised generalised transaction ledger (Berlin version 8fea825 - 2022\u201308-22) (2022)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-37709-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:02:07Z","timestamp":1689501727000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37709-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377082","9783031377099"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37709-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}