本文是Gauntlet和Peteris Erins（Auditless）在形式验证和激励模拟领域合作的结果。我们感谢Haseeb Qureshi和Charlie Noyes的反馈。 我们相信基于代理的模拟可以帮助分析智能合约和协议行为。但还有其他方法，例如形式验证。形式验证使逻辑保证强于模拟的统计保证。在回答我们关心的安全问题时，它是否比刺激模拟更好？在本文中，我们将探讨形式验证，并将其视为模拟的有力补充。 我们将介绍: 第1部分.Uniswap合同的高级概述 第2部分。如何测试区块链系统的安全性 第3部分Uniswap智能合约的官方验证历史 第4部分。我们如何应用形式验证 第5部分。我们的结果以及为什么我们认为正式验证不是测试安全性的完整解决方案 概观 正式验证提供了对智能合约逻辑和安全性的独特见解。但是，在试图说明智能合约的财务结果时，形式是不够的。 基于代理的模拟允许一组模拟代理与合同进行交互。我们的目标是应用形式验证技术在Uniswap交易所自动发现有效合约操作并分析一系列交易。 使用代理有两个目的。它允许我们预测协议设计阶段的实际使用并在实施阶段支持验证。代理模拟允许我们在与合同交互时预测真实用户的行为。 随后的博客文章将展示如何在激励模拟中使用更有效的随机技术，以获得对Uniswap的一些了解。

第1部分.Uniswap合同的高级概述

Uniswap交换是一组智能合约，允许任何人交易以太坊和ERC20代币而无需向订单提交订单。单个Uniswap交换合约支持特定的以太坊/ERC20令牌，任何人都可以使用Uniswap合约创建新的令牌对。一旦建立了交换，它将自动运行: ·创造流动性。流动性提供者将首先以当前汇率提供以太坊和代币。您可以随时添加/删除更多内容。 ·交易。然后，市场参与者可以使用Uniswap交易合约直接进行交易。 ·定价算法。使用“恒定产品做市商”模型自动确定给定交易的价格。在给定的交易期间，Uniswap将设定价格以保持产品的以太坊（x * y=k）和给定的代币。 ·流动性成本。收取小额费用并分发给流动性提供者。 第2部分。如何测试区块链系统的安全性 要知道像Uniswap这样的系统是否安全，我们需要回答两个问题: ·正确。代码是否遵循我们预期的模型（作为规范或其他形式编写）？ ·有效性。我们想要的模型会激发我们想要的行为吗？ 正式验证只能帮助前者，但它对后者没什么帮助。像“我们应该如何设定费率”这样的问题根本无法通过形式验证来回答。 第3部分Uniswap智能合约的正式验证历史 正式验证 许多项目试图使用形式验证技术来证明他们的合同是正确的。这对于相对简单的智能合约来说非常可行。形式验证和程序分析技术可以确定代码是否遵循给定的规范并且通常具有致命的反例。 之前的工作 Uniswap现有的轻量级表单验证是如何实现这些技术的一个很好的例子。 KEVM框架用于通过addLiquidity，removequityy，ethToTokenSwapInput和ethToTokenSwapOutput来验证做市商（x * y=k）模型及其实现。假设现有的ERC20合同“表现良好”。 在对共识系统尽职调查的后续审计中，该团队能够推断出如果这一假设被打破会发生什么。他们发现ERC20令牌的恶意实施可以用来欺骗市场参与者，允许攻击者重新进入Uniswap合同并以相同的成本消耗更多的钱。 原则上，可以将此扩展规范捕获为代码模板。它可以表示和调用半ERC20兼容合同（相同的接口，但不一定是ERC20行为）并尝试使用形式验证来发现攻击。在实践中，这使得形式验证问题在计算上更复杂，因为当用于发现任意程序时，底层SMT解析器中的分支增加。这种技术有时被称为“程序集成”。 Microsoft Research调查是获取更多信息的良好起点。 这些挑战说明了与形式验证（包括程序集成）:相关的其他两个限制 ·完整的规范可能难以编写和表达。 ·目前的正式验证器仅适用于简单合同和简单规范。 第4部分。我们如何应用形式验证 制定问题 为了在一组代理的影响下测试合同的行为，我们首先尝试使用符号分析将其应用于自动化操作发现。符号分析将代码转换为一组可由SMT求解器求解的方程。 SMT求解器是SAT求解器的扩展，超出了布尔公式（简单命题的陈述）到包含inte的公式 符号分析将代码转换为一组可由SMT求解器求解的方程。 SMT求解器是SAT求解器的扩展，超出了布尔公式（针对简单命题所述），涉及整数，位向量，数组和编程中常见的其他形式的数据。 查看符号分析的一种简单方法是，它可以用于正式指定关于给定智能合约的假设，证明假设是真的，或者生成反例。 例如，在形式验证中，假设通常是关于合同的断言，例如，“双重函数返回的值始终是偶数”。 Pragma solidity ^ 0.5.1 合同倍增{ 函数double（uint x）pure public returns（uint）{ Uint y=2 * x; 要求（y％2==0）; //可以通过FV检查此断言 回归y; } } 我们正在寻找验证，断言断言在某些事务集中是正确的。 为了使用符号分析找出操作，我们设置以下假设:“Uniswap契约不支持有效事务”。如果证明这是错误的，则反例将是一组产生有效合同交易的输入。 符号分析 我们提供黑盒符号解释器，其中包括修改后的Uniswap交换合同，可用于资助的插槽帐户代理池以及一组受限制的操作（匹配合同功能）。重播在两个测试链上完成的操作——一致的测试链和纯EVM副本（维护以保留对合同存储的更改）。目标是找到一组有效参数来完成事务并提前当前状态。 第5部分。我们的结果以及为什么我们认为正式的形式验证不是测试安全性的完整解决方案 这种方法是停滞不前的，但是我们发现了这个特定合同的三个局限性，它证明了符号分析和一般形式验证的挑战。 表现不佳 2.应用优化选择操作难度 3.需要修改合同/设置，在这种情况下执行:内联调用，删除截止时间考虑因素和发送操作 我们相信挑战1-2可以通过使用随机模拟来克服，因此我们得出结论，符号分析最好用于战术验证合同/模型的某些方面或支持其理解。下面我们详细说明我们的方法并解释我们的发 表现不佳 我们使用重写的有界模型检查器进行符号分析，该检查器在EVM字节码级别运行。它与基于状态的符号解释器（例如Mythril和Manticore）的不同之处在于，它在合同块完全扩展后应用SMT求解器一次，而不是在找到每个块时递增。另一个区别是假阴性是无法忍受的。我们使用的基础SMT解决方案是Z3。解释器包含几个优化，我们将在下面详细介绍。 作为输出，我们提取参数数组（也称为CALLDATA）并使用契约接口将其转换为相关合同函数的一组有效高级参数。

我们直接从字节码合约开始，并实现了几个优化。 ·具有块修剪的多级反编译器 ·Z3上的自定义包装器，具有不确定性的操作符 ·公共数据的模块化表示 ·EVM级二进制类型 ·高级实现

这是每个函数/动作:的性能 [所有时间都在2013款MacBook Air上测量，i7 8GB]

星形加法的最后一个例子是直接实现Z3的流动性函数，例如代表性的“理论最小值”。操作空间表示哪些合同功能可用作代理的操作。为addLiquidity添加代表，依此类推。 为了解释这些结果，我们必须解释符号分析器的性能特征。在我们的示例中，超过90％的计算时间直接用于SMT求解器。因此，性能优化的大部分工作都花在优化重写SMT求解器的合同上。 不幸的是，位向量乘法对于当前的SMT求解器来说是一个挑战。让我们假设SMT求解器的性能（非常）松散地与所需命题的数量相关。为了说明这一点，EVM中的每个数字都表示为256位字。在Z3中，这些词被进一步“分解”成代表每个比特的256个命题变量。表示位向量乘法需要多达256个部分和，每个部分代表另一个256位字，需要65,000个变量。删除功能包含四次乘法 这些词被进一步“分解”成代表每个比特的256个命题变量。表示位向量乘法需要多达256个部分和，每个部分代表另一个256位字，需要65,000个变量。流动性函数包含总共四次乘法。 尽管SMT求解器的性能无法以任何直接或算术的方式预测，但乘法和除法对合同的影响也通过从源中删除而独立验证（产生的运行时间可忽略不计）。 这是一个很好的例子。在这种情况下，简单的合同可能需要大量不可预测的解决方案时间。通常，非专业人员很难预测SMT求解器的性能。正如我们所看到的，它不一定与使用的代码行或其他易于识别的指标有关。 2.应用优化选择操作难度 使SMT解决方案对该应用具有吸引力的是它有可能找到最佳操作。优化的SMT求解器“vZ”是Z3的一部分，支持基于优化变量的高效最佳反例。它结合了各种子问题的优化算法。

优化vZ的求解器接口 - Bjørner等人的优化SMT求解器。

我们完成了实验，以确定是否可以使用优化求解器根据给定的价格表来查找最优交易，但不幸的是，求解程序将运行超过24小时。 我们认为，在某些情况下，优化仍然在计算上是可行的。例如，契约更简单，优化问题可以很容易地映射到“vZ”中可用的算法，例如线性问题的单纯形法。 3.需要修改合同 在形式验证中，降低合同复杂性（特别是在字节码级别）对性能至关重要，或者是应用依赖于输入结构的正式验证器的先决条件。 我们对Uniswap合同做出的关键改变是消除与子调和外部调用相关的复杂性，并专注于交换逻辑: ·删除合同中的内部和外部子呼叫，内联内部呼叫以及ERC20帐户持有模型 ·删除发送行为 ·删除时间戳截止日期约束 符号分析在刺激模拟中的作用 在这篇博文中，我们展示了如何使用不完整的符号分析来分析像Uniswap这样的复杂系统与基于代理的模拟。换句话说，形式验证是一个重要而有力的工具。但它最好在战术上与更广泛的刺激模拟:互补 ·模型验证。验证简化的仿真模型 ·提取模型。通过验证操作帮助自动从代码中提取模型 ·官方建议。为模拟提供新的或极端的启动状态 ·局部优化。使用内置优化程序验证有关局部最优性的假设