Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny

【Author】 Cassez, Franck; Fuller, Joanne; Ghale, Milad K.; Pearce, David J.; Quiles, Horacio M. A.

【Source】FORMAL METHODS, FM 2023

【影响因子】

【Abstract】The Ethereum protocol implements a replicated state machine. The network participants keep track of the system state by: 1) agreeing on the sequence of transactions to be processed and 2) computing the state transitions that correspond to the sequence of transactions. Ethereum transactions are programs, called smart contracts, and computing a state transition requires executing some code. The Ethereum Virtual Machine (EVM) provides this capability and can execute programs written in EVM bytecode. We present a formal and executable semantics of the EVM written in the verification-friendly language Dafny: it provides (i) a readable, formal and verified specification of the semantics of the EVM; (ii) a framework to formally reason about bytecode.

【Keywords】

【发表时间】2023

【收录时间】2023-06-26

【文献类型】实验仿真

【主题类别】

区块链技术-核心技术-扩展方案