引用
Hildenbrandt E, Saxena M, Zhu X, et al. Kevm: A complete semantics of the ethereum virtual machine[R]. 2017.
16.1摘要
分布式系统和应用密码学社区感兴趣的一个发展领域是智能合约——它是通过区块链来同步其状态的自执行性金融工具。以太坊（Ethereum）就是这样一种智能合约系统，目前已得到广泛的实际采用，以太坊已经发展成为可确保约300亿美元币值和每日超过300,000笔交易的系统。
不幸的是，这些技术的兴起被一系列重复的安全漏洞和引人注目的合同失败案例所破坏。为了解决这些问题，以太坊社区已经开展形式验证和程序分析的研究。尽管如此，目前尚不存在关于EVM（以太坊虚拟机）正式、严格、全面和可执行的语义学，使得无法基于语义来构建研究工具。
在这项工作中，我们介绍了KEVM，EVM的第一个完全可执行的形式语义，即执行智能合约的字节码语言。我们在可执行语义的框架K中创建此语义。我们的语义不仅通过了官方提供用于EVM实现的40,683个测试压力测试套件，而且还揭示了基于现有的EVM语义的纸上形式化的歧义和潜在的错误源，这些特性使KEVM成为理想的正式可参考实现。
我们继续为EVM合约寻求一种语义优先的形式验证方法，并通过使用KEVM验证示例智能合约的算术运算和第二个合约中的令牌传递函数的正确运算，来证明其实用性。我们证明了我们的方法是可行的，并且在计算上没有限制。我们希望我们的工作可以为以太坊开发各种有用的正式衍生工具提供基础，包括模型检查器，经认证的编译器和程序等效检查器。
16.2介绍
比特币是早期的加密货币之一，在实践和学术上都取得了成功，因此引发了人们对区块链技术潜在应用的广泛搜索。以太坊就是这样一个系统，它使用准Turing完整编程语言实现了通用的复制“世界计算机”。以太坊的一个目标是允许开发在区块链交易中执行的任意应用程序和脚本，使用区块链以一种可以被系统中任何参与者验证的方式在全球范围内同步其状态。以太坊系统中的参与者和合约以称为Ether的分布式货币进行交易。以太坊网络上的账户可以与基于虚拟机的语言（称为EVM）关联。这些程序称为“智能合约”，在交易调用帐户时执行。
智能合约的日益普及已导致对其安全性的审查越来越严格。但是，智能合约中存在许多细微的错误，从交易顺序依赖到处理不当的异常。EVM支持合同间执行，从而使丰富的网络动态成为可能，因为合同将其计算的一部分卸载到其他合同中，这进一步使获得这些合同的严格保证的问题变得更加复杂。
为了应对高保证要求和丰富的对抗模型之间的这种复杂混合，以太坊基金会特别呼吁“以人机可读、可执行的形式对EVM进行规范化”，“以EVM字节码或Solidity开发经过正式验证的库”和“用小语言开发经过正式验证的编译器”。在我们的工作中，直接处理了前两个问题，并为第三个问题打下基础。
16.3EVM的K语义（KEVM）
16.3.1逻辑语义结构
KEVM在逻辑上分为三个模块，每个模块涉及不同级别的语义。
- data.k：低级EVM客户端代码中使用的数据表示形式及其关联的数据结构，以及它们根据K本机数据结构的定义。
- evm.k：K中的EVM语义的形式化，包括各种操作码的执行语义、世界和网络状态、气体语义以及在执行过程中可能发生的各种错误。
- ethereum.k：额外的运行EVM代码的执行环境/驱动程序，具有解析用于测试参考EVM实现的JSON测试文件的模式。
在本节的其余部分，我们将重点关注evm.k，并描述如何将一些重要或困难的EVM操作形式化为K规则。
16.3.2EVM执行状态（配置）
在K中，使用一种配置来指定系统的潜在状态，以便转换规则可以轻松访问和更新该状态的不同组件。 每个过渡规则代表一个执行步骤，并将一个配置重写为另一个。 EVM的状态分为两个部分：活动交易的状态（执行智能合约）和整个网络的状态（帐户信息）。 为了反映这一点，我们的配置包括两部分——执行子状态和网络状态。
执行子状态：每次执行EVM都有一个关联的帐户，一个程序计数器，当前程序，一个字堆栈和一个易失性本地内存。
网络状态：区块链对应于一组帐户状态。
16.3.3EVM硬件
KEVM以当前操作码上的一条命令管道的形式提供EVM执行周期，每条命令都会更新状态的某些部分。 在此过程中，可能会引发异常，并且在捕获异常时可能会还原状态。 在这里，我们描述了随后定义EVM的“硬件”。
具体“异常”的表现和相应的控制流、处理方式可以阅读原文获取。
16.3.4EVM程序和执行
EVM操作码：EVM程序是与EVM操作码相对应的字节序列；每个操作码都有一个英文助记符。
自变量加载：执行操作码时，将从中解压缩正确数量的自变量。
执行周期：EVM的执行周期首先对异常状态进行多次检查，然后实际执行状态更新。总体而言，它包括三个宏步骤：
- 在给定当前状态的情况下，检查操作码是否异常。
- 执行与操作相关的状态更新。
- 将程序计数器递增到给定运算符的正确值。
燃料（gas）语义：将#exec运算符转换为两个连续的状态更新。 首先，应用#gas更新，然后应用对执行状态的更新。 由于在EVM模型中计算和内存都会产生成本，因此，为了计算#gas，我们将计算由于执行导致的内在气体，再计算内存消耗成本。
操作码语义：最后，扣除费用后，我们准备让操作码在worldstate上执行。 运算符#exec将操作码直接放在单元格的前面，并加载了中的参数。
请注意，我们利用了K的配置抽象，它允许每个规则仅指定与其操作相关的配置部分。 正如我们所展示的，这使我们的规则简洁，易于阅读，并精确且专有地捕获了它们定义的相关计算的语义性质。 这也使语义更新/维护更加简单。单元结构的变化只能影响提及该单元的规则。
16.4语义评估
为了评估我们的语义，我们专注于测量正确性、性能和可扩展性。
16.4.1正确性和性能
我们将KEVM的具体评估重点放在以太坊基金会发布的官方VMTests测试套件上。 EVM的先前语义工作，包括当前唯一可用的可执行语义，已使用该测试套件作为语义完整性的基准。该测试套件包含40,683个测试，KEVM通过了所有格式良好的测试。下表显示了KEVM、Lem语义和以太坊基金会分配的C ++参考实现之间的性能比较。通过与C ++参考实现进行比较，我们展示了使用KEVM形式语义进行原型设计，开发和测试套件评估的可行性。所有执行时间均以完整的CPU时间给出。
通过使用功能强大的硬件，进一步改进了功能；利用测试固有的并行性和为持续集成（CI）建造的机器，我们能够在7分钟内通过KEVM运行完整的测试套件（包括压力测试）（不将压力测试的时间缩短至3分钟） 。这将KEVM定位于高保证CI环境的可行性。用于语言规范的相同语义可以合理地用于快速测试。我们相信这些有希望的经验结果支持KEVM的长期愿景：交易执行时间的中位数不到40毫秒，并且性能接近本机参考实现，因此我们的语义理论上能够每天处理单笔数百万笔交易线程商品硬件，高于以太坊网络当前的每日交易量。我们认为，这些结果证实了以太坊的正式参考客户的未来工作方向，其中派生的KEVM解释器可以实时处理以太坊交易，为需要它的用户提供最大可能的保证，并补充为性能而设计的现有实现。除了在开发/原型制作过程中运行测试之外，从我们的语义中衍生的其他工具还可以用于调试EVM和以EVM编写的智能合约中的新功能，以及用于智能合约的形式分析。
16.4.2可扩展性
我们在设计语义时考虑了可扩展性。通过异常和条件分支提供控制流的简单命令式语言使我们可以添加更多基元来扩展KEVM。为了在语义的执行中具有更大的灵活性，我们在一个额外的单元格上将执行参数化。当前支持三种模式：NORMAL执行，VMTESTS执行和GASANALYZE模式。
16.5衍生分析工具
开发用于K定义的形式化分析工具可以通过以下两种方式之一进行：设计和实现独立于语言的分析工具，该工具可以处理所有K定义，或者使用执行分析的执行驱动程序/监视器来扩展现有的语义。在本节中，我们将介绍直接和自动地从形式语义派生的两个工具：KEVM语义调试器和KEVM程序验证器。
16.5.1语义调试器
在命令中添加--debugger选项，可将用户放入KDebug shell。在此Shell中，许多调试命令向用户公开，包括step，peek和back。给定编程语言的语义，这些命令可用于手动探索目标程序的执行。还要注意，语义调试器只是K符号执行引擎的包装，使它能够处理符号状态以及具体状态。我们的KEVM调试器在定义EVM的语义方面被证明非常有用，因为当测试失败时，调试器可以逐步执行其相关部分以精确定位故障。既然语义已经完成并通过了测试，调试器仍然可以通过逐步执行各个EVM程序来分析各个EVM程序，除提供具体调试器提供的传统状态信息外，还提供丰富的语义状态信息。这可以用来确保EVM程序的行为，甚至可以与传统的调试工具集成在一起，以进一步扩展调试环境。
16.5.2程序验证
为K开发的一种特别有用的形式分析工具是可达性逻辑证明。 该证明接受K定义和一组逻辑可达性证明作为输入作为证明。然后，证明将假设语义，尝试在语言的执行空间上自动证明可达性定理。
16.6结论
本文的主要贡献如下：
- K中的EVM语义：我们在K框架中定义了形式上严格的EVM语义的可执行实例，涵盖了所有EVM指令。
- EVM参考解释器：使用我们的形式语义，我们自动生成一个能够执行EVM事务并相应更新EVM世界状态的EVM参考解释器。
- EVM程序验证程序：我们使用上述内容创建了程序验证程序，并演示了根据规范对示例EVM程序的完整验证。
- 统一的工具集：以太坊生态系统存在许多软件分析工具，每个软件分析工具都对自己的EVM模型和语义进行编码，他们都可以从我们的单一形式参考语义自动生成，从而减少由不同模型引起的工具错误的可能性。
所有这些工作都是开源的，并在https://github.com/kframework/evm-semantics上提供，我们希望以太坊社区将采用我们的方法来制定更严格，更安全的合同。
本文由南京大学软件学院2016级本科生曹佳玮转述
本文来自投稿，不代表本人立场，如若转载，请注明出处：http://www.souzhinan.com/kj/296201.html