智能合约测试：形式验证与符号执行
- cyfrin
- 发布于 2024-11-07 12:57
- 阅读 38
本文深入探讨了智能合约的形式验证和符号执行测试。通过对这些技术的原理、工具和应用进行详细介绍，强调了它们在Web3安全审核中的重要性，并与其他测试方法进行比较。
智能合约形式验证和符号执行测试
我们与两位Trail of Bits Web3安全团队的成员讨论了形式验证和符号执行。此外，我们还回顾了这些技术带来的价值并将其与其他工具进行比较。
符号执行和形式验证 | Trail Of Bits区块链工程主管 - YouTube
Cyfrin审计
4.76K订阅者
符号执行和形式验证 | Trail Of Bits区块链工程主管
Cyfrin审计
搜索
信息
购物
轻触静音
如果播放未能很快开始，请尝试重新启动设备。
你已退出登录
你观看的视频可能已添加到电视的观看历史中并影响电视推荐。为了避免这种情况，请在计算机上取消并登录YouTube。
取消确认
分享
包含播放列表
检索共享信息时发生错误。请稍后再试。
稍后观看
分享
复制链接
观看于
0:00
/
•现场
•
引言
形式验证是使用数学模型证明或反驳系统的给定属性的行为。
符号执行是一种用于形式验证的技术。符号执行探索程序中的不同路径，为每个路径创建数学表示。
简而言之，符号执行就是把你的代码转换为一组数学表达式。更简单地说，就是把你的代码变成数学。
这是否是你审计旅程的万灵药？让我们一探究竟。
团队
Josselin采访缩略图
我非常高兴地采访了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永远不应回退，我们将尝试证明或反驳这一点。当然，这可能看起来是个傻例子，但你可以想象这只是一个称为“提取资金”的函数，而你希望用户能够始终提取他们的钱。这将显得更不愚蠢。
在符号执行中，我们将把这个函数转换为每条执行路径的数学/逻辑表示。一旦我们有了一组数学函数，我们可以将其输入到一个求解器中，它将告诉我们属性是真还是假，或者我们的不变式是真还是假的。要利用符号执行进行形式验证，我们遵循以下步骤：
- 探索所有可能的路径
- 将路径转换为数学表达
- 将数学表达发送到SMT/SAT求解器
探索路径
使用符号执行的形式验证过程可视化
在这个例子中，我们有两个路径：
- 路径1：我们返回(a + 1)
- 路径2：a + 1溢出并且我们回退
如果我们传递最大uint256值，并尝试加1，Solidity将在0.8版本时回退。这是我们的代码可以选择的两条路径。软件工具可以自动找到这些路径，但稍后我们会展示给你。
现在我们有了这两条路径，我们将它们转换为数学表达式。其中一种最流行的表达形式是将它们转换为一组布尔值，如下所示：
路径 1
a < type(uint256).max
路径 2
a == type(uint256).maxa + 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断言检查器
这样我们将再次看到它能够找到输入以数学方式破坏我们的断言。
回顾
所以这里发生了很多事情。让我们回顾一下。
- 我们构建了一些Solidity代码。
- 我们理解了不变式。
- 我们使用符号执行工具（如Solidity内置工具）创建了一组布尔表达，表示我们代码的每个执行路径（这自动完成）。
- 然后，我们将它们发送到求解器如Z3进行处理（在后台）。
在与Josselin的采访中，我们对此示例进行了全面的讲解，因此如果你想了解更多，请务必查看。
如果这看起来有点复杂，不要害怕；请务必提出问题并在描述中留言。
限制
和Troy的采访缩略图
这是一剂灵药吗？
不。
有时服务器可能无法解决问题，比如问题过于复杂。我们通常会给服务器提供超时，因为，比如，如果你需要反转一个哈希函数，你知道，祝你好运。
- Josselin
和任何技术一样，这些并不是一刀切的方法。使用符号执行可能会遇到称为路径爆炸问题的事情；在合理的时间内，计算机无法探索太多路径，求解器也无法完成。
实践中的应用
采取这些步骤的实用性如何？这真的难做吗？
使用该技术需要显著的努力。你需要了解它们的工作原理，以及如何帮助它们，也需要付出持续的努力。我认为真正重要的是属性。如果你想知道错误是否会发生，以及属性是否可能被破坏，那么你并不一定需要正式的方法，你可以使用模糊测试，这更易用并提供相似的价值。
- Josselin
Trail of Bits团队创建了secure-contracts.com来帮助开发人员理解属性，以便他们可以以基于属性的测试方法来构建和测试代码。
有时，足够强大的模糊测试工具就是你所需要的，而符号执行和形式验证则显得有些过度。
此外，即使形式验证也不能证明你的代码没有错误。它仅仅是数学证明的特定操作正确定义。
我希望随着人工智能的发展，很多工作会变得更加容易，接下来我们拭目以待。
结论
但希望现在你至少了解了符号执行的基础知识。如果你想了解更多，请留下评论和赞赏。
😸😸关注Patrick！😸😸
预约智能合约审计：Cyfrin
与Trail Of Bits的形式验证
非常感谢Trail of Bits的 Troy 和 Josselin 拨冗接受这次采访。此外，特别感谢 Hari , Runtime Verification , Leo Alt 和 Palina 对于理解这些概念以及他们在该领域的工作所提供的帮助。
- 原文链接： cyfrin.io/blog/solidity-...
- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～
