KEVM: A Complete Semantics of the Ethereum Virtual Machine
KEVM: A Complete Semantics of the Ethereum Virtual Machine
复制标题
DOI：
--
复制
发表时间：
2017-08
期刊：
影响因子：
--
通讯作者：
Everett Hildenbrandt;M. Saxena;Xiaoran Zhu;Nishant Rodrigues;Philip Daian;Dwight Guth;Grigore Roşu
中科院分区：
文献类型：
--
作者：
Everett Hildenbrandt;M. Saxena;Xiaoran Zhu;Nishant Rodrigues;Philip Daian;Dwight Guth;Grigore Roşu
分布式系统和应用密码学社区感兴趣的一个发展中领域是智能合约：自动执行的金融工具，通常通过区块链同步其状态。其中一个已经被广泛采用的智能合约系统是以太坊，它已经发展到保护大约300亿美元的货币价值和超过30万的日常交易。不幸的是，这些技术的兴起被一系列反复出现的安全漏洞和高调的合同失败所破坏。为了解决这些问题，以太坊社区转向了形式化验证和程序分析，由于智能合约固有的计算简单性和有限时间执行，这些方法显示出很大的前景。尽管如此，目前还没有完全正式、严格、全面和可执行的EVM（以太坊虚拟机）语义，这使得这些工具缺乏严谨性。在这项工作中，我们提出了KEVM，EVM的第一个完全可执行的形式语义，EVM是执行智能合约的字节码语言。我们在可执行语义的框架K框架中创建此语义。我们表明，我们的语义不仅通过了EVM实现的官方40，683测试压力测试套件，而且还揭示了我们工作所基于的现有EVM语义的书面形式化中的歧义和潜在错误来源[45]。这些属性使KEVM成为一个理想的正式参考实现，可以根据它来评估其他实现。我们继续为EVM合约的语义优先形式化验证方法进行论证，并通过使用KEVM验证示例智能合约的算术运算和第二合约中令牌传递函数的正确操作的实际重要属性来证明其实用性。我们表明，我们的方法是可行的，而不是计算上的限制。我们希望我们的工作可以作为以太坊开发各种有用的形式化衍生工具的基础，包括模型检查器，认证编译器和程序等价检查器。
A developing field of interest for the distributed systems and applied cryptography community is that of smart contracts: self-executing financial instruments that synchronize their state, often through a blockchain. One such smart contract system that has seen widespread practical adoption is Ethereum, which has grown to secure approximately 30 billion USD of currency value and in excess of 300,000 daily transactions. Unfortunately, the rise of these technologies has been marred by a repeated series of security vulnerabilities and high profile contract failures. To address these failures, the Ethereum community has turned to formal verification and program analysis which show great promise due to the computational simplicity and boundedtime execution inherent to smart contracts. Despite this, no fully formal, rigorous, comprehensive, and executable semantics of the EVM (Ethereum Virtual Machine) currently exists, leaving a lack of rigor on which to base such tools. In this work, we present KEVM, the first fully executable formal semantics of the EVM, the bytecode language in which smart contracts are executed. We create this semantics in a framework for executable semantics, the K framework. We show that our semantics not only passes the official 40,683-test stress test suite for EVM implementations, but also reveals ambiguities and potential sources of error in the existing on-paper formalization of EVM semantics [45] on which our work is based. These properties make KEVM an ideal formal reference implementation against which other implementations can be evaluated. We proceed to argue for a semantics-first formal verification approach for EVM contracts, and demonstrate its practicality by using KEVM to verify practically important properties over the arithmetic operation of an example smart contract and the correct operation of a token transfer function in a second contract. We show that our approach is feasible and not computationally restrictive. We hope that our work serves as the base for the development of a wide range of useful formally derived tools for Ethereum, including model checkers, certified compilers, and program equivalence checkers.