为什么说形式验证不是测试安全性的完整解决方案

我们相信基于代理的仿真可以帮助分析智能合约和协议行为。但也存在其他方法，比如形式验证。形式验证使逻辑保证比模拟的统计保证更强。在回答我们关心的安全问题方面，它是否优于激励模拟？在这篇文章中，我们探讨了形式化验证，并认为它是对模拟的有力补充。

概述

形式验证可以提供对智能合约逻辑和安全性的独特见解。然而，当试图对一份智能合约的财务结果进行陈述时，形式是不够的。

基于代理的模拟允许一组模拟代理与合约交互。们的目标是应用形式验证技术来自动发现Uniswap交换上的有效合约操作，并分析一系列交易。

使用代理的目的有两方面：它允许我们预测协议设计阶段的实际使用，并支持在实现阶段进行验证。代理模拟允许我们预测真实用户与合约交互时的行为。

后续的博客文章将展示如何在激励模拟中使用更有效的随机技术来获得关于Uniswap的一些见解。

第1部分。Uniswap合约的高级概览

Uniswap exchange是一组智能合约，允许任何人在不向订单簿提交订单的情况下交易以太币和ERC20代币。单个Uniswap交换合约支持特定的以太币/ERC20代币，任何人都可以使用Uniswap合约创建新的代币对。一旦交易所成立，它就会自主运作：

· 流动性的创造。流动资金提供者将首先按当前汇率提供以太币和代币。可以在任何时候添加/删除更多。

· 交易。然后，市场参与者可以直接使用Uniswap交易所合同进行交易。

· 定价算法。给定交易的价格是使用“常数产品做市商”模型自动确定的。在给定的贸易期间，Uniswap将设置价格，以便保存产品（x * y = k）的以太币量和给定的代币。

· 流动性的费用。小额费用被征收并分配给流动性提供者。

第2部分。如何测试区块链系统的安全性

要想知道Uniswap这样的系统是否安全，我们需要回答两个问题：

· 正确性。代码是否遵循我们预期的模型（作为规范或其他形式编写）？

· 有效性。我们想要的模型会激励我们想要的行为吗？

形式验证只对前者有一些帮助，而对后者几乎没有帮助。像“我们应该如何设置费率”这样的问题根本无法通过形式验证来回答。

第3部分。Uniswap智能合约的形式验证历史

形式验证

许多项目都尝试使用形式验证技术来证明他们的合约是正确的。对于相对简单的智能合约，这是非常可行的。形式验证和程序分析技术可以确定代码是否遵循给定的规范，而且常常会出现致命的反例。

之前的工作

Uniswap现有的轻量级形式验证就是使用这些技术可以实现的一个很好的例子。利用KEVM框架验证了做市商（x * y = k）模型及其通过addLiquidity、removeliquity、ethToTokenSwapInput和ethToTokenSwapOutput的实现。假设现有的ERC20合约“表现良好”。

在共识系统调查公司（consensus sys Diligence）的后续审计中，该团队能够推断出如果打破这一假设会发生什么。他们发现，ERC20代币的恶意实现可以用来欺骗市场参与者，让攻击者重新进入Uniswap合约，以同样的成本消耗更多的资金。

原则上，可以将此扩展规范捕获为代码模板。可以表示和调用一个半ERC20兼容的合约（相同的接口，但不一定是ERC20行为），并尝试使用形式验证来发现攻击。在实践中，这使得形式验证问题在计算上更加复杂，因为当用于发现任意程序时，底层SMT解决程序中的分支会增加。这种技术有时被称为“程序综合”。微软研究院的这项调查是了解更多信息的良好起点。

这些挑战说明了与形式验证（包括程序综合）相关的另外两个限制：

· 完整的规范在编写和表达方面可能具有挑战性。

· 目前的形式验证器只适用于简单的合约和简单的规范。

第4部分。我们如何应用形式验证

制定问题

为了测试合约在一组代理的影响下的行为，我们首先尝试使用符号分析将其应用于自动化操作发现。符号分析将代码转换成一组可以由SMT求解器求解的公式。SMT求解器是SAT求解器的扩展，它超越了布尔公式（对简单命题进行陈述）到包含inte的公式

符号分析将代码转换成一组可以由SMT求解器求解的公式。SMT求解器是SAT求解器的扩展，它超越了布尔公式（对简单命题进行陈述），涉及整数、位向量、数组和编程中常见的其他数据形式的公式。

一种看待符号分析的简单方法是，它可以被用来正式指定一个关于给定的智能合约的假设，证明假设为真，或者生成一个反例。

例如，在形式验证中，假设通常是关于合约的断言，例如，“double函数返回的值总是偶数”。

pragma solidity ^0.5.1

contract Doubler {

function double（uint x） pure public returns （uint） {

uint y = 2 * x;

require （y % 2 == 0）; // This assertion could be checked via FV

return y;

}

我们正在寻找在某些交易集中给定断言是否为true的验证。

为了使用符号分析进行操作发现，我们设置了以下假设：“Uniswap合约不支持有效的交易”。如果这被证明是错误的，那么反例将是生成有效合约交易的一组输入。

具有象征意义的分析

我们提供了一个黑盒符号解释器，其中包含一个经过修改的Uniswap交换合约、一个可用资金支持的一条缝帐户代理池和一组受限制的操作（与合约功能匹配）。在两个测试链上重播完成的操作——一致测试链和一个纯EVM副本（为了保存对契约存储的更改而进行维护）。目标是发现一组有效的参数来完成交易并推进当前状态。

第5部分。我们的结果以及为什么我们不认为形式正式的验证是测试安全性的完整解决方案

这种方法是站住脚的，但是我们发现了这个特殊合同的三个限制，这表明了符号分析和一般形式验证的挑战：

1. 表现不佳

2. 应用优化来选择操作的难度

3. 修改合同/设置的必要性，在这种情况下是为了执行：内联调用、删除截止日期考虑事项和发送操作

我们相信挑战1-2可以通过使用随机模拟来克服，因此我们得出结论，符号分析最好用于战术上验证合约/模型的某些方面，或者支持其理解。下面我们详细介绍我们的方法并解释我们的发现。

1. 表现不佳

我们使用一个基于重写的有界模型检查器来进行符号分析，它在EVM字节码级别上运行。它与Mythril和Manticore等基于状态的符号解释器的不同之处在于，它在合约块完全扩展之后一次性应用SMT-solver，而不是在发现每个块时增量地应用。另一个区别是，假阴性是不能容忍的。我们使用的底层SMT解决程序是Z3。解释器包含几个优化，我们将在下面详细介绍。

作为输出，我们提取了参数数组（也称为CALLDATA）并使用合约接口，将其转换为相关合约函数的一组有效的高级参数。

我们从字节码合约直开始，并实现了几个优化：

· 一个多级反编译器与块修剪

· Z3上的自定义包装器，带有用于非决定论的操作符

· 公共数据的模块化表示

· EVM级别的二进制类型

· 先进的具体化

为什么说形式验证不是测试安全性的完整解决方案

这是每个功能/动作的性能：

［所有时间在2013年MacBook Air上测量，i7 8GB］

为什么说形式验证不是测试安全性的完整解决方案

最后一个加星的例子是直接实现Z3的流动性函数，例如，一个代表性的“理论最小值”。操作空间表示哪些合约函数可用作代理的操作。Add代表addLiquidity，等等。

为了解释这些结果，我们必须解释符号分析器的性能特征。在我们的示例中，超过90%的计算时间直接花费在SMT求解程序中。因此，性能优化的大部分工作都花在优化如何重写SMT求解程序的合约上。

不幸的是，位向量乘法对目前的SMT求解器是一个挑战。让我们假设SMT求解器的性能（非常）松散地与所需的命题项数量相关。为了说明这一点，EVM中的每个数字都表示为一个256位的单词。在Z3中，这些单词进一步“分解”为表示每个位的256个命题变量。表示位向量乘法需要多达256个部分和，每个部分和表示另一个256位单词，需要65，000个变量。移除性函数包含四个乘法

这些单词被进一步“分解”为表示每个位的256个命题变量。表示位向量乘法需要多达256个部分和，每个部分和表示另一个256位单词，需要65，000个变量。流动性函数总共包含四次乘法。

虽然SMT求解器的性能无法以任何直接或算术的方式预测，但是乘法和除法对该契约的影响也通过从源中删除它得到了独立的验证（产生的运行时可以忽略不计）。

这是一个很好的例子，在这个例子中，概念简单的合约可能需要不可预测的大量解决方案时间。一般来说，非专业人员很难预测SMT-solver的性能，正如我们所看到的，它并不一定与所使用的代码行或其他容易识别的指标相关。

2. 应用优化来选择操作的难度

使SMT解决方案对这个应用程序具有吸引力的是它发现最优操作的潜力。优化SMT求解器“vZ”作为Z3的一部分，支持根据优化的变量求解有效的最优反例。它结合了各种子问题的优化算法。

为什么说形式验证不是测试安全性的完整解决方案