Dafny中以太坊虚拟机的形式和可执行语义
Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny
摘要：
以太坊协议实现了一个复制的状态机。网络参与者通过以下方式跟踪系统状态：1）商定要处理的事务序列; 2）计算与事务序列对应的状态转换。以太坊交易是程序，称为智能合约，计算状态转换需要执行一些代码。以太坊虚拟机（EVM）提供了这种能力，并可以执行以EVM字节码编写的程序。我们提出了一个正式的和可执行的语义的EVM编写的验证友好的语言Dafny：它提供了（一）一个可读的，正式的和验证规范的EVM的语义;（ii）一个框架，正式原因字节码。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
