Portal de Periódicos da CAPES

Defining the Ethereum Virtual Machine for Interactive Theorem Provers

2017; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-319-70278-0_33

1611-3349

Yoichi Hirai,

Cryptography and Data Security

Smart contracts in Ethereum are executed by the Ethereum Virtual Machine (EVM). We defined EVM in Lem, a language that can be compiled for a few interactive theorem provers. We tested our definition against a standard test suite for Ethereum implementations. Using our definition, we proved some safety properties of Ethereum smart contracts in an interactive theorem prover Isabelle/HOL. To our knowledge, ours is the first formal EVM definition for smart contract verification that implements all instructions. Our definition can serve as a basis for further analysis and generation of Ethereum smart contracts.