Options
Formally Verified EVM Block-Optimizations
Kirchner, Daniel; Genaim, Samir; Albert, Elvira; u. a. (2023): „Formally Verified EVM Block-Optimizations“. In: Cham: Springer Nature Switzerland S. 176–189, doi: 10.1007/978-3-031-37709-9_9.
Title of the compilation:
Computer Aided Verification : 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part III
Editors:
Enea, Constantin
Lal, Akash
Conference:
35th International Conference, CAV 2023, July 17–22, 2023 ; Paris, France
Publisher Information:
Year of publication:
2023
Pages:
ISBN:
978-3-031-37709-9
Series ; Volume:
Lecture Notes in Computer Science ; 13966
Language:
English
Abstract:
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.
GND Keywords: ; ; ; ;
Ethereum
Virtuelle Maschine
Smart contract
Optimierung
Automatisches Beweisverfahren
Keywords: ; ; ; ;
Coq
Ethereum Virtual Machine
Smart Contracts
Optimization
Theorem Proving
DDC Classification:
RVK Classification:
Peer Reviewed:
Yes:
International Distribution:
Yes:
Type:
Conferenceobject
Activation date:
July 31, 2023
Versioning
Question on publication
Permalink
https://fis.uni-bamberg.de/handle/uniba/89789