智能合约测试：形式验证与符号执行

智能合约形式验证和符号执行测试

我们与两位Trail of Bits Web3安全团队的成员讨论了形式验证和符号执行。此外，我们还回顾了这些技术带来的价值并将其与其他工具进行比较。

‍

符号执行和形式验证 | Trail Of Bits区块链工程主管 - YouTube

引言

形式验证是使用数学模型证明或反驳系统的给定属性的行为。

符号执行是一种用于形式验证的技术。符号执行探索程序中的不同路径，为每个路径创建数学表示。

简而言之，符号执行就是把你的代码转换为一组数学表达式。更简单地说，就是把你的代码变成数学。

这是否是你审计旅程的万灵药？让我们一探究竟。

团队

我非常高兴地采访了Trail of Bits的区块链工程主管乔斯林以及Trail of Bits的安全工程师Troy，讨论测试方法和形式验证。如果你想观看，我提供了他们的完整采访链接（Troy, Josselin）！

要了解形式验证和符号执行究竟是什么，我们需要快速回顾一下Web3中的一些测试。如果你还没有看过我关于不变性测试的视频，请务必先观看它再阅读这篇文章。

在测试时，我们使用哪些工具来高度保证我们的程序按预期工作？

层级 0 | 人工审查

每个审计员和智能合约工程师都应能够手动审查自己的代码。ChatGPT不够好。人工审查很不错，但我们需要确保不完全依赖人类进行结果，我们需要自动化流程，以便更有保障地发现错误。

层级 1 | 单元测试

显然，你必须有单元测试，用于测试非常具体的内容。为你的每行代码编写单元测试将会提供良好的代码覆盖率。这也是测试的最低要求。

示例Solidity函数

例如，如果上述代码是我们的Solidity代码，而我们的setNumber函数应将number设置为newNumber。单元测试能够捕获这一点。

Foundry单元测试输出

如果我们使用Foundry，我们可能得到输出，如上所示。

如果测试失败，这意味着我们的测试捕获了一个问题，我们可以回过头来修复我们的代码。

像Foundry、Hardhat、Apeworx、Truffle和Brownie等大多数框架都具备单元测试能力。

‍

层级 2 | 模糊测试

模糊测试是指通过将随机输入传递给程序进行运行。因此，你必须在代码中定义一些始终希望为真的内容。

— Troy

模糊测试是Web3安全的新最低要求。

因为我说是这样。

如果你还没有观看我关于模糊测试的视频…… 那就去看吧！

对于模糊测试/不变性/属性测试，你需要理解系统的属性或不变性，然后进行模糊测试。一旦定义了属性，你就会随机生成数据，试图打破该属性。如果发现某个数据打破了它，就知道你有一个需要重构来处理的边缘情况。

Foundry、Echidna和Consensys Diligence都有模糊测试工具。

‍

层级 3 | 静态分析

单元测试和模糊测试被称为动态测试。动态测试意味着你实际上是在执行一些操作，比如实际上运行我们的代码。

• Troy

在静态分析中，我们只是查看我们的代码或让某些工具查看我们的代码。例如，这段代码在我们的提款功能中存在典型的重入漏洞。

存在漏洞的代码

如果我们运行一个静态分析工具，如Slither，它将自动检测到这个错误。这对于快速发现已知的坏实践代码特定部分非常有用。

即使Solidity编译器也可以被视为一种静态分析工具。

层级 4 | 形式验证

形式验证将是证明或反驳系统给定属性的行为。这通常通过系统和属性的数学模型完成。

— Josselin

又提到那个词，属性。你会发现，无论你在测试中做什么，你几乎都需要理解系统的属性，就在那里，Josselin给了我们模糊测试与形式验证之间的一些钥匙。

• 模糊测试通过向系统抛出随机数据来试图破坏属性。
• 形式验证通过使用数学证明来试图破坏属性。

进行形式验证有许多不同的方法，如：

• 符号执行
• 抽象解释
• 模型检查

在这篇文章中，我们将重点关注符号执行，因为这是目前Web3中最流行的方法之一。

符号执行

路径探索示例

你可以从这段MIT视频中了解更多关于符号执行的一般信息。

符号执行是一种技术，你试图探索程序的不同路径，并将这些路径表示为数学表达式，以试图证明某些内容。对于每条执行路径，你将创建一个数学表示。因此，我们需要做的第一件事是弄清楚我们想证明或反驳的内容。

示例代码

在我们上面的演示中，假设我们的不变式是f永远不应回退，我们将尝试证明或反驳这一点。当然，这可能看起来是个傻例子，但你可以想象这只是一个称为“提取资金”的函数，而你希望用户能够始终提取他们的钱。这将显得更不愚蠢。

在符号执行中，我们将把这个函数转换为每条执行路径的数学/逻辑表示。一旦我们有了一组数学函数，我们可以将其输入到一个求解器中，它将告诉我们属性是真还是假，或者我们的不变式是真还是假的。要利用符号执行进行形式验证，我们遵循以下步骤：

1. 探索所有可能的路径
2. 将路径转换为数学表达
3. 将数学表达发送到SMT/SAT求解器

探索路径

使用符号执行的形式验证过程可视化

在这个例子中，我们有两个路径：

• 路径1：我们返回(a + 1)
• 路径2：a + 1溢出并且我们回退

如果我们传递最大uint256值，并尝试加1，Solidity将在0.8版本时回退。这是我们的代码可以选择的两条路径。软件工具可以自动找到这些路径，但稍后我们会展示给你。

现在我们有了这两条路径，我们将它们转换为数学表达式。其中一种最流行的表达形式是将它们转换为一组布尔值，如下所示：

路径 1

• a < type(uint256).max

路径 2

• a == type(uint256).max
• a + 1 < a

路径2 仅在 a > a + 1 时才能实现，因为当1加到 a 上时，我们会回退。这组布尔值将被放入SAT求解器中，SAT求解器将尝试为a找到满足所有布尔值为真的值。如果它能够找到一个值，则将该布尔组视为“可解”或sat。

通过这个小示例，你可以发现构建一组布尔值是多么简单，但如果我们得到更复杂的函数，则难度会增加。我们希望将此布尔列表转换为SMT-LIB语言以供SAT求解器使用，以上示例可以重新写为SMTLIB如下：

; 声明一个符号整数变量'a'作为256位整数

(declare-const a (_ BitVec 256))

; 为路径1创建上下文

(push)

; 添加路径1的断言

; 断言a不等于uint256.max

(assert (distinct a #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff))

(check-sat)

; 移除路径1的上下文

(pop)

; 为路径2创建上下文

(push)

; 添加路径2的断言

; 断言a等于uint256.max

(assert (= a #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff))

; bvult是“位向量无符号小于”，所以我们确认a + 1小于a

(assert (bvult (bvadd a (_ bv1 256)) a))

; 检查路径2是否可满足

(check-sat)

现在，如果你将这段代码粘贴到像Z3这样的工具中，或在你的计算机上本地运行它，它会给出一条输出，看起来就像这样：

Z3输出示例

两个sat输出意味着它们能够找到输入来使每条路径的布尔集合为真——由于路径2回退，而我们的不变式是永远不应回退，因此我们证明了我们的不变式被破坏了！

现在我在ChatGPT的帮助下手动创建了这段SMTLIB代码。但是，像Manticore、HEVM甚至Solidity SMT检查器这样的符号执行工具可以为你提供类似的输出。但是所有这些工具都自带内置的Z3。因此它们甚至可以跳过转换为布尔值的步骤，直接给你SMT求解器的输出。

如果你想看到关于许多进行符号执行的工具的比较，可以查看Palina的这一篇文章。

即使Solidity编译器本身也能在后台处理整个过程：

• 探索路径
• 将路径转换为布尔值集合
• 检查这些路径是否可到达

使用solc编译器，我们可以运行模型检查引擎，并寻找溢出。

运行solc SMT检查器的示例

如果我们运行这个，你会看到Solidity编译器能够进行符号执行。现在，回退检测相对容易，但我们可以看被回退的assert。即a不等于1，重新运行这个，但一定要寻找断言问题，而不是溢出。

我们首先将一个断言添加到代码中

添加断言

然后运行solc检查器以查找破损的断言（不变式）。

Solidity断言检查器

这样我们将再次看到它能够找到输入以数学方式破坏我们的断言。

回顾

所以这里发生了很多事情。让我们回顾一下。

1. 我们构建了一些Solidity代码。
2. 我们理解了不变式。
3. 我们使用符号执行工具（如Solidity内置工具）创建了一组布尔表达，表示我们代码的每个执行路径（这自动完成）。
4. 然后，我们将它们发送到求解器如Z3进行处理（在后台）。

在与Josselin的采访中，我们对此示例进行了全面的讲解，因此如果你想了解更多，请务必查看。

如果这看起来有点复杂，不要害怕；请务必提出问题并在描述中留言。

限制

和Troy的采访缩略图

这是一剂灵药吗？

不。

有时服务器可能无法解决问题，比如问题过于复杂。我们通常会给服务器提供超时，因为，比如，如果你需要反转一个哈希函数，你知道，祝你好运。

• Josselin

和任何技术一样，这些并不是一刀切的方法。使用符号执行可能会遇到称为路径爆炸问题的事情；在合理的时间内，计算机无法探索太多路径，求解器也无法完成。

实践中的应用

采取这些步骤的实用性如何？这真的难做吗？

使用该技术需要显著的努力。你需要了解它们的工作原理，以及如何帮助它们，也需要付出持续的努力。我认为真正重要的是属性。如果你想知道错误是否会发生，以及属性是否可能被破坏，那么你并不一定需要正式的方法，你可以使用模糊测试，这更易用并提供相似的价值。

• Josselin

Trail of Bits团队创建了secure-contracts.com来帮助开发人员理解属性，以便他们可以以基于属性的测试方法来构建和测试代码。

有时，足够强大的模糊测试工具就是你所需要的，而符号执行和形式验证则显得有些过度。

此外，即使形式验证也不能证明你的代码没有错误。它仅仅是数学证明的特定操作正确定义。

我希望随着人工智能的发展，很多工作会变得更加容易，接下来我们拭目以待。

结论

但希望现在你至少了解了符号执行的基础知识。如果你想了解更多，请留下评论和赞赏。

😸😸关注Patrick！😸😸

YouTube

Twitch直播上传与短视频

与Trail Of Bits的形式验证

非常感谢Trail of Bits的 Troy 和 Josselin 拨冗接受这次采访。此外，特别感谢 Hari , Runtime Verification , Leo Alt 和 Palina 对于理解这些概念以及他们在该领域的工作所提供的帮助。

‍

• 原文链接： cyfrin.io/blog/solidity-...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～