Formally Verified EVM Block-Optimizations

Simple item page
dc.conference.titleComputer Aided Verification. CAV 2023.
dc.contributor.authorKirchner, Daniel
dc.contributor.authorAlbert Albiol, Elvira María
dc.contributor.authorGenaim, Samir
dc.contributor.authorMartín Martín, Enrique
dc.date.accessioned2026-02-27T16:44:30Z
dc.date.available2026-02-27T16:44:30Z
dc.date.issued2023-07-17
dc.description.abstractThe efficiency and the security of smart contracts 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 EVM (Ethereum Virtual Machine) block-optimizations, 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 EVM block-optimizations on smart contracts using the Coq proof assistant. This amounts to the challenging problem of proving semantic equivalence of two blocks of EVM instructions, which is realized by means of three novel Coq components: a symbolic execution engine which can execute an EVM 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 EVM blocks under comparison.
dc.description.departmentDepto. de Sistemas Informáticos y Computación
dc.description.facultyFac. de Informática
dc.description.refereedTRUE
dc.description.statuspub
dc.identifier.citationAlbert, E., Genaim, S., Kirchner, D., Martin-Martin, E. (2023). Formally Verified EVM Block-Optimizations. In: Enea, C., Lal, A. (eds) Computer Aided Verification. CAV 2023. Lecture Notes in Computer Science, vol 13966. Springer, Cham. https://doi.org/10.1007/978-3-031-37709-9_9
dc.identifier.doi10.1007/978-3-031-37709-9_9
dc.identifier.isbn9783031377082
dc.identifier.isbn9783031377099
dc.identifier.issn0302-9743
dc.identifier.issn1611-3349
dc.identifier.officialurlhttps://doi.org/10.1007/978-3-031-37709-9_9
dc.identifier.urihttps://hdl.handle.net/20.500.14352/133537
dc.language.isoeng
dc.page.final189
dc.page.initial176
dc.rightsAttribution 4.0 Internationalen
dc.rights.accessRightsopen access
dc.rights.urihttp://creativecommons.org/licenses/by/4.0/
dc.subject.keywordCoq
dc.subject.keywordEthereum Virtual Machine
dc.subject.keywordSmart Contracts
dc.subject.keywordOptimization
dc.subject.keywordTheorem Proving
dc.subject.ucmLenguajes de programación
dc.subject.unesco1203.17 Informática
dc.titleFormally Verified EVM Block-Optimizations
dc.typeconference paper
dspace.entity.typePublication
relation.isAuthorOfPublication1b41e88a-837f-414a-af5d-9105b5c0e7c5
relation.isAuthorOfPublication9d982c6c-9e4f-4459-bd6e-1866104f03f6
relation.isAuthorOfPublication8c7dbac8-1093-454e-a0cf-e7b2f316cf09
relation.isAuthorOfPublication.latestForDiscovery1b41e88a-837f-414a-af5d-9105b5c0e7c5

Download

Original bundle

Now showing 1 - 1 of 1
Thumbnail Image
Name:
Formally_Verified_EVM.pdf
Size:
714.15 KB
Format:
Adobe Portable Document Format
Download Download

Collections

Artículos