19.1引用
Amani, Sidney, et al. "Towards verifying ethereum smart contract bytecode in Isabelle/HOL." Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. ACM, 2018.
19.2摘要
区块链技术在研究和许多行业中越来越受到关注。以太坊区块链提供智能合约，这是在区块链交易历史中定义，执行和记录为交易的小型程序。这些智能合约在以太坊虚拟机（EVM）上运行，可用于编码协议，转移资产以及在各方之间的关系中强制执行完整性条件。智能合约可以带来财务价值，并且越来越多地用于安全，保安或任务关键目的。智能合约中的错误导致并将导致损失或伤害。正式验证可以对智能合约的正确行为提供最高级别的信心。在本文中，我们通过字节码级别的声音程序逻辑扩展了Isabelle / HOL中现有的EVM形式化。我们将字节码序列构造成直线代码块，并创建一个程序逻辑来推理这些。这种抽象是控制EVM智能合约正式验证的成本和复杂性的一步。
关键词 形式验证，区块链，智能合约，以太坊，Isabelle / HOL
19.3 EVM字节码程序的完整正确性
Myreen介绍了一种通用的方法，用于对ARM的特定应用进行机器代码的形式验证。 在本节中，我们将展示如何将此一般方法应用于EVM，并进一步考虑根据气体消耗量的EVM特定属性。
在通用模型中，状态携带执行程序所需的所有信息，包括构成程序本身的指令（具有相应的附图标记），引用当前指令的程序计数器，堆栈等。所有这些元素被统一地处理为所谓的状态元素集合，并使用分离逻辑连接∧*在状态中分离。接下来的函数捕获单个机器步骤，该函数通过程序计数器从状态获取当前指令，并根据指令的指定行为转换状态。当然，接下来可能并不总是能够选择一条指令，因为执行可以正确终止或有异常终止。这在状态内由不连续标志指示，该标志只是状态元素ContinuingElm False的缩写，而不是继续标志缩写ContinuingElm True。如果状态中不存在继续，则接下来保持状态不变
程序c的Hoare风格属性由三重| = {P} c {Q}捕获，其中P和Q是状态的分离逻辑谓词。 对于任何状态s和谓词F，三元组都是真的
存在这样的自然数k
谓词F通常在此上下文中被称为框架，并且保持它允许我们在本地推理部分状态。 代码（c）是另一个指定程序代码存在于状态中的元素，而nextk表示下一个k次迭代。 这样的三元组是非常通用的，我们不能从其中许多结论中得出很多结论，除了在给定的前提条件下程序c将通过满足Q的状态。这在Q为不连续∧* Q 的情况下立即改变，现在 说明c已达到满足Q 的终止状态。 因此，显示| = {P} c {not-Continuing∧* Q }等于显示Q 状态的程序c的终止。
如Hirai 所示，这种通用技术可无缝应用于EVM程序。 然而，我们意识到单独终止合同是一种不必要的负担，因为以太坊的设计使得所有智能合约都能保证终止（成功或由于“天然气”异常）。 更具体地说，为了确保矿工获得通过操作以太坊区块链而产生的成本的补偿，每个EVM指令都有燃气费。 在调用合同时，发起人提供的气体预算与预计执行的计算成本如何成比例，并且每个执行步骤都从预算中扣除。 如果天然气消耗超过预算，则会出现“天然气”异常，矿工将在调用之前保留所有天然气和合同状态。
这些区块链细节为我们提供终止订单。 因此，我们通过函数nextμ增强EVM形式化，函数nextμ尽可能长地在每个状态上迭代，即存在继续标志。 因此，我们显示的关于nextμ的基本属性是，对于任何状态s，存在k≥0，使得（i）nextμ（s）= nextk（s）成立;
（ii）对于任何l，如果0≤l
（iii）对于任何l，使得l≥k，状态nextl（s）包含不继续。
换句话说，nextμ（s）= nextk（s）其中k是最小数，使得nextk（s）到达具有不连续元素的状态。
现在，关于契约正确性，我们将| = {P} c {Q}加强到总输入/输出属性| = [P] c [Q]，如果对于任何状态s和帧F，
则为真。暗示
总而言之，我们迄今取得的成就是将我们一劳永逸地展示的终止部分分解出来，从而彻底消除了验证过程中的这一义务。
在下一节中，我们将介绍我们的程序逻辑处理EVM字节码，它（基于第19.5节中介绍的健全性）将为我们提供一个声音设备来导出形式为| = [P] c [Q]的合同属性的验证条件。 虽然程序逻辑还不支持通用循环，但值得注意的是，分解终止部分意味着我们不需要提供任何循环变体来建立属性，因为气体消耗是任何EVM循环的变体。 另一方面，我们可能需要通过异常条件来增加三元组，以处理在循环迭代期间引发“不合格”异常的情况，从而不会达到循环退出条件。 或者，我们也可以通过检查剩余气体量来增加任何这样的条件，使得如果没有足够的气体可用于执行下一次迭代，任何环路将刚刚退出。然而，这种方法需要很好地近似每次迭代消耗的气体。
19.4 程序逻辑
Hoare风格的程序逻辑包含一系列规则，允许我们从其各部分的属性中导出复合程序的语义属性。例如，在结构化语言的情况下，我们通常会有一条规则告诉我们一个程序，如果C，那么p1，否则p2表现出一定的输入/输出行为，如果p1和p2这样做，但是，附加的前提条件C可用于p1和¬C表示p2。当我们不得不推理EVM字节码时，情况就不那么简单了。在这个级别，条件复合构造只是作为一个跳转指令出现，它将执行流程传递给程序的另一部分。从这个意义上讲，将整个字节码程序简单地视为指令列表的程序逻辑原则上是可行，但错综复杂。为此，可以使用更复杂的技术，例如通过提取控制流图（CFG）进行反编译，特别是应用于Java虚拟机（JVM）代码。 CFG提取的目的是将程序分成基本块，即没有跳转的指令序列，并使用对应于跳转的边连接它们。基本块的基本属性是它们包含直线代码，即控制流总是在其第一条指令处输入它，并且只在最后一条指令执行后才离开。因此，在CFG级别上对字节码的推理类似于在许多方面对结构化程序的推理。特别是，CFG提供了足够的结构来添加注释，例如循环不变量，实现验证条件生成过程的完全自动化。
但是，完整的CFG提取在EVM上下文中提出了比JVM更高级的挑战，尤其是从正式建模的角度来看。 这是因为JVM跳转指令将其目标地址作为可以静态确定的立即值参数，而在EVM中，必须从堆栈中获取跳转目的地，即动态地。 出于这个原因，我们的字节码预处理目前仅解决基本块提取问题，将在下一节中介绍。 然后，第19.4.2,19.4.3和19.4.4节分别介绍了我们的逻辑如何处理程序，块和指令。
19.4.1基本块的提取
我们将EVM指令分为三组：
（i）JUMPDEST表示跳转目的地，因此表示基本块的开始;
（ii）JUMP，JUMPI，UNKNOWN和所有Misc-instructions2表示基本块的结束（UNKNOWN和Miscinstructions中断程序执行）;
（iii）所有剩余指示。
此外，我们使用以下四种类型对基本块进行分类：
（i）终端 - 如果块的最后一条指令中断执行;
（ii）跳跃 - 如果最后一条指令是JUMP;
（iii）Jumpi - 如果最后一条指令是JUMPI;
（iv）接下来 - 否则，即当控制从块的最后一条指令传递到具有后继地址的指令时。
图19-1说明了我们如何将EVM字节码分成不同类型的基本块，从而使用第一条指令的地址索引块，并从块内容中删除所有跳转。 整个提取过程在Isabelle开发中通过函数构建块捕获，该函数构建块将指令列表映射到元组列表（n，xs，t），其中n是块索引，xs是指令列表 块的类型，t是块的类型。
图19-1 程序分为四个基本块，其中灰色指令出现在原始代码中，但从块的指令列表中删除。
通过将字节码拆分为基本块，没有信息丢失，因为我们可以按正确的顺序连接生成的块，并根据块类型插入跳回。 更确切地说，我们还具有连接块功能，使得对于任何字节码程序，
身份都成立
基于这些准备工作，将在以下三个部分中以归纳的方式定义以下不同级别推理的谓词：
其中P，Q是状态谓词，x是指令，xs是指令列表，blocks是基本块列表，（n，xs，t） - 基本块。
19.4.2 计划规则
我们从程序级开始，我们对每种块类型都有以下规则。
也就是说，只需将一个终端块传递给块级别，因为在处理完这些块之后我们不需要查看任何其他块。
Next-block的规则在这方面有所不同：
状态元素pc m在处理xs之后确定程序计数器。 然后我们需要从结构块中检索与索引m相关联的下一个块，其由（m，ys，t）∈blocks表示，并继续（m，ys，t）。
此外，在跳块的情况下，我们还需要在处理块之后从堆栈中检索跳转目的地的地址。 这产生以下，稍微涉及更多的规则：
其中R1和R2缩写条件分别是：
关于堆栈，堆栈高度（h + 1）和堆栈h j指定一个状态，其中索引h指的是包含j的堆栈顶部 - 我们正在寻找的跳转目标。 关于气体，gas-pred将可用的气体量绑定到g，而部分⟨h≤1023∧g≥8⟩是纯条件，即不依赖于状态，并设置堆栈高度的上限 气体量的下限，即8个单位：EVM执行跳跃所需的数量，由gas-pred（g-8）扣除。 请注意，在这里和下面的规则中，我们需要携带连续的状态元素，因为EVM模型[8]强制要求处理指令的状态是继续还是不继续
条件跳转的情况。 也就是说，一个Jumpi-block是类似的，除了我们还需要从堆栈中检索要比较为0的值c并且仅在c0时跳转：
其中R1，R2，R3缩写条件分别是：
19.4.3 块规则
在基本块的级别，我们只需要两个简单的规则来处理非空和空的指令列表：
其中P⇒Q表示P s表示任何状态s的Q s。
19.4.4 指令规则
为了能够验证任何可能的EVM字节码程序，我们需要为70个EVM指令中的每一个提供规则。 目前，我们为36条常用指令提供规则，并逐步“按需”扩展此设置。 但是，仅由EVM状态无法完全捕获涉及以太坊全局状态的指令的行为，例如用于合同间调用的CALL。 因此，在EVM语义中（以及在我们的逻辑中），这些指令会导致必须单独建模的环境操作。
PUSH1的以下规则，即在堆栈上推送一个字节的操作，具有很强的代表性，因为它显示了我们如何指定EVM在前提条件下执行指令的必要条件，以及操作对状态的影响 后置条件中的元素：
其中P代表
和Q为
特别地，我们已经声明堆栈的高度增加1（堆栈高度（h + 1））并且堆栈的顶部索引h指向PUSH1的效果中的值x（堆栈h x）。 由于包括要推送的字节的指令的大小是2个字节，程序计数器增加2.还值得注意的是，我们通过在前置条件和后置条件中携带变量F将帧合并到这样的指令特定规则中，如图所示 以上。 这与更常见的方式形成对比，后者引入了表单的通用框架规则
并从所有特定于指令的规则中删除F. 虽然规则是合理的，但这种处理会在验证过程中产生相当大的开销，因为每次应用特定于指令的规则时我们都需要应用帧规则。
除了框架规则，我们在指令级别仍然有两个通用规则：
规则（i）是通常的“后果”规则，允许我们调整前后条件，而（ii）需要履行具有不可满足前提条件的琐碎证据义务。 这些义务经常来自条件跳转（规则（iv），第19.4.2节），其中条件在实际跳转之前被完全评估，因此我们只需要跟随一个新兴分支。
以下部分通过健全性属性将程序逻辑和第19.3节的结果放在一起，并概述其证明。
19.5本文主要贡献
（i）Isabelle / HOL定理证明器中EVM形式化[8]的扩展，涵盖智能合约正确性属性，并基于以太坊的执行“气体”概念对终止进行单独的通用处理;（ii）在字节码级别验证智能合约的合理程序逻辑; 和（iii）Isabelle策略支持使用逻辑规则自动生成验证条件。
我们的开发在Isabelle中完全正式化，并已被以太坊基金会维护的官方EVM形式化存储库
本文由南京大学软工系2019硕士生刘芳潇翻译转述。
添加新手交流群：币种分析、每日早晚盘分析
添加助理微信，一对一亲自指导：YoYo8abc
