Marescotti M , Blicha M , Antti E. J. Hyvärinen, et al. Computing Exact Worst-Case Gas Consumption for Smart Contracts[J]. 2018.
21.2 摘要以太坊平台是一个公共的，分布式的，基于区块链的数据库，由独立的各方维护。用户通过编写程序与以太网进行交互，并让矿工根据执行的复杂性执行这些程序，并收取费用。以气体消耗量衡量的确切费用一般取决于未知的以太坊状态，即使最坏的情况预测原则上也是不可判定的。天然气消费的不确定性可能导致效率低下，资金损失，并且在极端情况下，资金被锁定一段不确定的时间。该可行性研究提出了两种方法，使用符号模型检查的方法确定有界以太坊执行的确切最坏情况气体消耗。我们给出了需要估算气体消耗的几个具体案例，并提供了两种确定气体消耗的方法，一种基于符号枚举执行路径，另一种基于计算路径，基于程序结构模块化。
21.3 Preliminaries以太坊虚拟机（EVM）是在以太坊区块链中运行的基于分布式共识的计算机。EVM执行智能合约，用基于堆栈的字节码编写的程序提供一小组低级指令。智能合约可以看作包含应用程序函数的已发送函数，这些函数在合同范围内的存储上运行，这些函数在函数调用上是持久的 ，以及仅在函数内可见的局部变量。 我们在以太坊中定义一个函数，无论是在EVM字节代码还是在实体中，都是f（v），其中f是函数的名称，v是函数的形式参数集。 从上下文中清除时，我们省略v。由数组S表示的存储是函数可以访问的存储变量集。 对存储的访问由S [i]表示，其中i是整数
表21-1 一些EVM指令成本。 该表的后半部分列出了指令的示例，其成本取决于执行它们的上下文和提供的参数。
虽然智能合约对应于诸如Java类实例之类的概念，但它们在某些方面却以有趣的方式存在差异。 例如，一旦部署在以太坊中，智能合约就会公开显示，合同代码也无法更改。 任何人都可以通过交易来与EVM进行交互，即创建智能合约或调用他们的功能，通过支付将执行交易的矿工。
交易的复杂性以其天然气消耗量来衡量。 每条EVM指令都有一个相关的气体消耗，这是一种将指令与其存储或执行成本联系起来的措施。 有关某些成本的示例，请参见表21-1。 除了指令特定成本之外，某些指令和声明还会影响函数本地存储器的大小，称为活动存储器。 在执行指令之前和之后，分别使a和b为活动存储器的大小（以字节为单位）。 可能的变更会导致成本或退款
为了通过矿工执行交易，用户提供他或她愿意为称为以太币的货币的气体单位支付的价格，以及交易可能消耗的以太的总量。 假设在运行交易时没有遇到任何错误，并且为实际燃气消耗支付的金额足够，则交易成功执行。 如果进行交易需要的燃气量超过提供的数量，则终止执行而不退款。
由于EVM的存储器模型，在某些情况下，指令的成本取决于指令的参数或执行指令时的合同状态。例如：
- SSTORE指令写入合同存储。特别是如果将非零值写入先前包含零值的存储位置，则该操作是昂贵的。 EVM执行模型包含退款计数器，用于奖励用户执行使EVM更便宜的指令。在SSTORE指令将零值写入先前保持非零值的位置的情况下，这会反映出来，从而导致退款。
- 指令对CALL和CALLVAL的指令成本取决于它们的参数。该指令用于在另一个合同中调用交易。虽然技术上有两种不同的指令，但从高级语言的角度来看，它们可以被解释为单指令。在这种情况下，事务的成本取决于调用中传递的参数的值是否为零。
EVM中完整事务的成本部分取决于EVM状态，参数和功能代码所规定的控制流程。由于参数和环境依赖于指令成本，控制流图不足以确定交易成本。我们通过以自然方式基于指令参数和环境依赖性添加新的边和节点，以及在气体消耗图气体消耗路径（GCP）中调用路径，将控制流图概括为气体消耗图。因此，遵循相同气体消耗路径的功能的所有执行都消耗相等量的气体。我们的方法旨在确定一个GCP，以最大限度地提高所有GCP的天然气消耗量。我们不是直接使用EVM字节码，而是基于更高级别的Solidity语言，可以说是当时编写智能合约的最流行的语言。因此，我们将GCP的概念概括为Solidity GCP。例如，由于EVM可用的低级优化，这些通常不一样。因此，我们不会尝试计算Solidity代码上的气体消耗量，而是使用保证覆盖所有Solidity GCP的具体执行来计算精确的EVM气体消耗量。
我们假设Solidity GCP也涵盖所有EVM GCP。 我们想强调这种方法选择是对结果有效性的潜在威胁，并将在下一节中关于正确性的定理中反映出来。 为了识别潜在不同的GCP，我们采用有界模型检验技术和SMT求解器，通过操作静态单一赋值（SSA）级别的Solidity，其中循环已经解开到 给定的限制。 由于以太坊协议规定了交易的最大耗气量，因此可以通过增加退绕限制来完成该方法。
21.4 气体消耗路径计数我们提出了一种算法，用于根据智能合约的展开SSA表示来枚举符号化的Solidity GCP。 虽然GCP的数量通常是展开的SSA表示的大小的指数，但是由于符号表示，算法在多项式空间中运行。 我们首先将Solidity合同的翻译转换为图21-1中未展开的SSA（USSA）表格，以便改编自[8]的示例程序。 为简洁起见，图21-1（a）使用类似于Solidity语言的伪代码而不是实际的Solidity语言.2契约由函数f和g组成，其中g表示f。 函数g写入存储变量z并使用固态msg.sender.transfer函数，这里简单地抽象为transfer（z）。 函数f对循环内的参数执行操作，将结果存储到局部变量中，并在计算后返回结果。
GCP的搜索是在USSA表格中完成的，如图21-1（b）所示。 该形式由一系列保护指派组成，其形式为c→b = e（x）或c→b = se（x），其中c是布尔值表达式的连接，e（x）是一个操作 变量x。 我们区分了相等的左边是内存中的变量（=）和存储位置（= s）的赋值，因为它们取决于具有不同成本的值（参见表1）。 同样，某些指令的成本取决于他们的论点。 为此，我们定义了将指令映射到其成本条件的函数ArgCond。 例如，ArgCond（a b）=∅，和ArgCond（transfer（x））= {x = 0}。 ΔCmem的结果仅取决于控制流动路径，因此不需要特殊处理。
算法1给出了基于枚举的算法的伪代码。该算法将入口点函数f（v）作为输入，并从f开始构造USSA，递归地嵌入从f（第1行）调用的所有函数。然后遍历USSA以通过在第4-9行中添加来自USSA分配的每个保护c的每个合取来构造一组布尔表达式C.对于每个存储赋值= s（第7行），以及其成本取决于其参数的每条指令（第9行），将附加的布尔表达式添加到C中。函数pre（xi）= xi-1将USSA变量xi映射到其先前的实例化。如果xi是第一个实例（即，i = 1），则pre（xi）是不出现在USSA中的“新”变量。在第二阶段，算法穷举查询USSA表格的SMT编码，用于来自C的每个布尔表达式组合，并获得在满意的情况下覆盖这些情况的v和S的值。然后通过模拟事务来查询v和S的每个值组合的成本，并且返回最高的气体估计值作为确切的最坏情况界限。
算法1.基于计算的算法来计算函数f的GCP。
示例1.在图1（b）的USSA表格上运行Algorithm1给出
其中前两个约束x1≥y1和y1≥0，整个第二行约束函数fij，faj，fbj的局部变量来自if条件; 联合约束（x1 y1 = 0）∧（z0 = 0），（x1 y1 = 0）∧（z0 0）来自SSTORE的参数和环境依赖关系（见表1），约束z1 = 0 来自CALL和CALLVAL的参数依赖，即ArgCond（transfer（z1））; 第三行来自SSTORE的参数和环境依赖性。
然后将约束集C与USSA表单的SMT表示一起提供给SMT解算器。 从USSA表格中查询C中约束的每个真值组合，导致最坏情况211 = 2048个SMT查询。 请注意，由于SMT求解器在实践中的增量实现，查询的数量可能（指数）更小，具体取决于查询的顺序。 在某些情况下，函数的输入v也可能是已知的，将查询数量减少到最坏情况的一小部分。
根据满意的查询结果，算法将提取v和S的具体值，然后将其用于计算相应的气体消耗路径的精确气体消耗。
图21-1中所示的USSA表格不承认不变z≥0，因此比原始合同更宽松。 获得此类合同不变量并非易事，超出了本文的范围。 为了获得确切的最坏情况的天然气消耗，合同不变量需要与USSA联合。
通过构造Algorithm1和GCP的定义，我们立即得到以下定理：
定理1.给定函数f，假设USSA为f，它准确描述了契约行为，并且在它之间存在一对一映射。 Solness和EVM代码，Algorithm1返回f的最坏情况气体消耗。
21.5 小结在本文中，我们基于有限模型检验技术启发的技术，提出了估算以太坊智能合约燃气消耗问题的解决方案。我们已经定义了一种气体消耗路径，它以自然的方式扩展了程序路径，同时考虑到相同操作根据其参数值和当前环境消耗不同量的气体这一事实。我们提出了两种不同的算法来识别给定函数的气体消耗路径。对于每个气体消耗路径，我们能够使用SMT求解器获得强制执行采用给定路径的环境状态。最后，我们可以使用EVM提供的功能来计算在获得的环境状态下功能的精确气体消耗。主要应用是计算最坏情况的气体消耗量，为开发人员提供有用的见解，并可能导致在智能合约的设计中发现问题，或者在两种替代实施方案之间进行选择时可能提供有用的信息。对于想要使用某些参数调用合同方法但是环境状态未知的用户来说，最坏情况下的气体消耗也是有意义的。
本文由南京大学软工系2019硕士生刘芳潇翻译转述。
,
