RT Conference Proceedings
T1 Formally Verified EVM Block-Optimizations
A1 Kirchner, Daniel
A1 Albert Albiol, Elvira María
A1 Genaim, Samir
A1 Martín Martín, Enrique
AB The 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.
SN 9783031377082
SN 9783031377099
SN 0302-9743
SN 1611-3349
YR 2023
FD 2023-07-17
LK https://hdl.handle.net/20.500.14352/133537
UL https://hdl.handle.net/20.500.14352/133537
LA eng
NO Albert, 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
DS Docta Complutense
RD 28 mar 2026