本文介绍了作者如何构建一个基于属性测试的工具 fuzzing-like-smarter-degen,用于检测智能合约中的漏洞。文章详细讨论了传统的单元测试的局限性,并介绍了模糊测试(fuzzing)的原理及其在智能合约安全检测中的应用。作者还介绍了如何通过假设库(Hypothesis)实现模糊测试,并展示了该工具的运行效果。
在这篇文章中,我解释了我如何以及为什么构建了 fuzzing-like-smarter-degen ,这是一个基于属性的测试软件,用于检测智能合约中的漏洞,使用的是 Hypothesis Python库。
让我们通过构建更好的安全工具来拯救以太坊生态系统(图片来自Dalle2)
当前,安全措施不足是阻碍Web3大众采用的最大障碍之一。智能合约直接涉及有价值的资产,其开源和公开可访问的属性,再加上公共区块链不可更改和抗审查的特性,使其成为黑客的完美目标。一旦漏洞被利用,通常为时已晚,且无法找回资金。
在过去三年中,由于安全性差,已经有超过50亿美元的资产被盗取(来源:https://hub.elliptic.co/analysis/top-five-defi-crime-trends-of-2022/ )
拥有近100%的单元测试覆盖率是一种常见的好实践,但这远远不够。我们当然可以通过更好的覆盖率度量提高测试质量,比如突变测试分数,这比更常用的代码覆盖率度量(如语句覆盖或分支覆盖)要强大得多,但这仍然是不够的。
人类只能编写少量的单元测试,只能测试在所有可能输入的大范围中微不足道的一小部分输入。
也许会让人感到吃惊的是,在其开创性文章 “重要智能合约中的实际缺陷是什么(我们如何找到它们)?”中,Trail of Bits审计团队报告称单元测试的质量与在代码库中发现的严重漏洞数量之间没有统计学上的显著相关性。
尽管单元测试很有帮助,但单独依靠它们似乎充其量在确保安全性方面的影响是微乎其微的!如果我们能让计算机以任意、随机的但聪明的方式自动生成数千或甚至数百万个测试,以更好地确保代码的安全,那将会怎样呢?这就是“模糊测试”的想法,也称为“基于属性的测试”。
基于属性的测试概括了手动编码的单元测试。首先,开发者编写一些称为_属性_或_不变式_的函数,如果代码正确实现,则应始终返回true。例如,一个简单的不变式可以是:如果用户_userA_试图向另一个用户_userB_发送_x_数量的代币,那么如果他的初始余额_balanceA_少于请求的数量x,那么该交易必须始终回退。不变式最好先用英语(自然语言)书写,然后仔细翻译成代码。
这是从优秀的Echidna工作坊系列中提取的另一个不变式示例
在编码了所有不变式后,模糊器运行,输入包含待测试软件和不变式。将生成成千上万的随机测试,并对所有这些测试检查每个不变式(可选择性地检查生成的输入是否验证某些用户指定的条件)。测试的输入并不是完全随机的:其中一些可能会在一个大区间内均匀选择,但模糊器经常选择专注于极端值:如0或_uint_类型的最大值。通过这种方式,典型上导致溢出或其他问题的多个边缘案例将被自动测试。这可以与人类生成的案例进行比较,人类往往更专注于“快乐路径”,而较少关注奇怪的边缘案例。这是模糊测试相较于单元测试的一个显著优势,因为许多错误往往集中在边缘案例上:这些对人类开发者来说并不直观。许多现代模糊器所使用的另一种技巧是覆盖指导:生成的测试被逐步突变,优先考虑那些能够揭示之前测试中较少探索的新代码部分的测试。如果你想深入了解覆盖指导模糊测试,我强烈推荐优秀的灰盒模糊测试章节来自《模糊测试手册》。 (顺便说一下,在机器学习中,这类似于基于新颖搜索的优化技术,如Map-Elites,这在解决需要大量探索的难题时非常流行)。
覆盖指导模糊测试工作原理的高层描述:通过专注于执行新代码部分的测试,我们可以更深入地探索错误。
在智能合约的上下文中,生成的测试实际上是发送到被测合约的一系列交易。在每次单个交易后,都会验证所有不变式。如果在交易序列结束时(最大长度,由用户设定)检查不变式,且所有不变式始终返回为真,则本地区块链的状态会被复位,以使待测合约恢复到其初始状态。然后,将另一系列交易发送到本地节点,验证不变式和生成交易的交替循环重复多次,直到检测到潜在错误(即某些不变式意外返回为假)或直到生成了如此多的测试而没有任何不变式遭到破坏,从而我们对代码的质量变得更有信心。如果发现某个不变式是可破坏的,就会进入一个最终阶段,称为缩减。这个阶段是可选的,但对于理解错误的来源非常有帮助。缩减的目标是找到导致不变式破坏的_最简单_测试用例。我们没有明确定义“最简单”,以避免深入技术细节,一个例子可以是:如果对一个参数为无符号整数的函数调用导致了错误,那么缩减将找到触发此错误的最小整数。另一个例子可能是找到导致不变式被否定的最短交易序列(如果需要多个函数调用)。这在后面的例子中会更清晰。
像符号执行和抽象解释这样的形式化方法呢?
形式化方法可以严格证明某个不变式永远为真(即对于任何输入)或找到打破该属性的反例,通过将_待测软件与不变式结合_转化为数学公式,然后对该公式应用自动证明器。模糊器只能通过提供一个反例来证明某些不变式是假的,因此你可能会遇到假负,但永远不会遇到假正。通过形式化方法,你得到的结果是一个真实的负面或真实的正面。
聪明的读者可能会问:“那么为什么不只使用形式化方法呢?模糊测试只测试少量输入,因此安全性无法保证。形式化方法是你所需要的,因为它们能够证明你的属性是正确的,因而比模糊测试更强大!”
模糊测试确实可能会遗漏一些错误:如果没有生成的输入能够破坏不变式,那么可能是一个假负。细节决定成败:形式化方法技术的使用更为复杂:它们的运行速度较慢,而且试图解决的数学问题通常如此复杂,以至于求解器会超时:在这种情况下,你不知道程序是没有漏洞还是包含了一个漏洞。你可以尝试调整形式化方法软件的许多参数来解决问题,但对于符号执行等技术存在基本限制:尤其是包含导致路径爆炸的循环的程序。另一方面,模糊测试对循环没有困难,而循环是现代软件中非常常见的构造。这就是为什么如今模糊测试在行业中越来越受到认可。根据Trail of Bits工程总监Josselin Feist的说法:
实际上,模糊器在检查智能合约不变式时给出了更好的投资回报 ;)
在典型的审计过程中,时间限制为1到3周,正式方法不太实用,而模糊测试则相对可行。正式方法特别适用于合同中最关键的部分,但我们必须有足够的时间正确运行和配置它们。这两种方法实际上是互补的。还要注意,两个领域之间的差异并不像最初看起来那样明确。最近,许多成功的模糊测试方法,如 concolic fuzzing,使用类似于符号执行的方法,因此它们是深受正式方法的启发!对智能合约中的符号执行感兴趣的读者,建议阅读这篇出色的 评述。
注意:这个模糊测试器最初是从 fuzzing-like-a-degen 分叉而来的,该项目附带一个不错的视频录制。生成测试用例的变异引擎仍然基于 Hypothesis Python 库。第一个改进是使用 Anvil 测试网络(来自 Foundry 框架)而不是 Ganache,这使得速度平均提高了40%。
首先,克隆 github 仓库并按照 README 中的说明安装模糊测试器。然后输入以下命令:
python fuzzer.py tests/invariant_breaker.sol
通过运行此命令,你正在用默认配置(包含在 config.yaml 中)启动模糊测试器,针对以下 solidity 文件,该文件也在原始 fuzzing-like-a-degen 中使用:
contract InvariantBreaker {
bool public flag0 = true;
bool public flag1 = true;
function set0(int256 val) public returns (bool) {
if (val % 100 == 0) flag0 = false;
return flag0;
}
function set1(int256 val) public returns (bool) {
if (val % 10 == 0 && !flag0) flag1 = false;
return flag1;
}
}
contract InvariantTest {
InvariantBreaker public inv;
function setUp() public {
inv = new InvariantBreaker();
}
function invariant_neverFalse() public returns (bool) {
return inv.flag1();
}
}
这段代码包含两个合约:第一个 InvariantBreaker 是我们想要验证的被测试合约。第二个 InvariantTest 是负责配置测试设置的辅助合约:它首先通过 setUp() 函数部署被测试的合约,然后定义了我们希望在每笔交易后检查的不变,该模糊测试器将尝试通过 _invariantneverFalse() 函数来破坏它。
默认配置参数为:
fuzz_runs: 1000
seq_len: 100
shrinking: true
swarm_testing: true
coverage_guidance: true
constants_mining: true
favor_long_sequence: true
anvil_port: 8545
前两个参数是最重要的。这意味着模糊测试器将尝试生成1000个序列,每个序列最多包含100笔交易。在每个序列之间,区块链的状态会重置为初始状态(即模糊测试活动开始时运行 setUp() 定义的状态)。对于最困难的案例,并为了提高安全性的信心,增加这两个参数是有用的。Echidna 的作者发现 _seqlen(交易序列的最大大小)参数到 300 是最佳的,而 _fuzzruns(交易序列的数量)可以增加一个或两个数量级,但要记住,增加这些参数也会使计算时间增加相同的倍数,这可能不够实用。
模糊测试器应该能够在不到1分钟的时间内找到一个破坏性反例。你应该获得类似于以下的输出:
Falsifying example: composite_test(
ops=[
(<Function set1>, 0),
(<Function set1>, 0),
(<Function set1>, 0),
(<Function set1>, 0),
(<Function set1>, 0),
(<Function set1>, 0),
(<Function set1>, 0),
(<Function set1>, 0),
(<Function set1>, 0),
(<Function set1>, 0),
(<Function set0>, 0),
(<Function set1>, 0)],
)
Invariant broken
注意最后两行:模糊测试器先调用 set0(0) 然后再调用 set1(0)。通过阅读 InvariantBreaker 可以检查到,这确实是将状态变量 flag1 设置为 false 所需的,因此破坏了我们想要测试的属性!
有一个警告,Hypothesis 的缩减过程在处理复杂测试(如复杂交易列表)时的性能不佳,因此它可能无法找到最小反例,在这种情况下:
(<Function set0>, 0),
(<Function set1>, 0)
请注意,原始 fuzzing-like-a-degen 程序甚至在进行几次迭代后不重置区块链的状态,因此反例的长度甚至更长,涉及数千笔交易,这使得可解释性变得更差。我最初的 fuzzing-like-a-smarter-degen 迭代实际上是使用了 Hypothesis 的 基于规则的状态机 框架进行有状态测试。虽然这在缩减过程中表现出色,并且还免费获取了群体测试功能(后面我们会详细讲解),但遗憾的是我必须放弃这个框架。这是因为在 Hypothesis 中 定向基于属性测试 在基于规则的状态机中并不受支持(即使是在每个测试结束时使用 target 方法,在 teardown 函数中)。定向基于属性测试仍被视为 Hypothesis 中的实验性功能,但我绝对需要它来实现覆盖引导模糊测试选项。
想要测试模糊测试器基于规则的状态机版本的好奇读者可以运行:
python RBSM_legacy.py tests/invariant_breaker.sol
这将输出在这种情况下的正确最小化反例(但即便是在更复杂的合约中,这个版本的缩减可能仍失败):
Falsifying example:
state = StateFulFuzzer()
state.reset_evm_state()
state.invariant_neverFalse()
state.set0(arg=0)
state.invariant_neverFalse()
state.set1(arg=0)
state.invariant_neverFalse()
state.teardown()
Invariant broken
正如你所看到的,这里检测到仅需要两个交易:set0(arg=0) 后跟 set1(arg=0)。然而,不推荐使用这个版本,因为它缺失了后期在 fuzzer.py 中添加的许多良好特性,例如 constants mining 和 coverage-guidance。
群体测试是一个非常有趣的想法,我在阅读 Alex Groce 的博客 时偶然发现的关于测试:高度推荐阅读以理解这一概念。因为在 无人免费午餐定理 的优化领域中,我们知道并不存在适用于解决每个问题的最佳配置,这也是为什么通常最好使用多样化的求解器序列。(这也提醒我们,为什么多样化的预测模型集在机器学习中几乎总是优于单一模型)。群体技术的理念是在不同的变异步骤中变化模糊测试器的一些参数,以便发现更深层次的错误。这些参数可以是交易的长度、在交易序列中调用的函数子集等。以下是我在代码中的实现方式:
@st.composite
def operations_list_strategy(draw):
# 生成操作的随机子集
if swarm_testing:
min_size_sampled = len(operations)-draw(st.integers(0,len(operations)-1))
unique_operations = st.sets(st.sampled_from(operations), min_size=min_size_sampled)
else:
unique_operations = st.just(operations)
selected_operations = draw(unique_operations)
if favor_long_sequence:
min_seq_len_sampled = seq_len-draw(st.integers(0,seq_len-1))
else:
min_seq_len_sampled = 1
selected_ops = st.lists(st.one_of(selected_operations), min_size=min_seq_len_sampled,max_size=seq_len)
return draw(selected_ops)
当 _swarmtesting 为真时,我们注意到只选择了一组功能(称为 operations)通过采样:_uniqueoperations,然后基于这些函数构造我们的交易序列。这使得模糊测试器能够发现如果一个函数必须在没有被“吸收状态”函数插入的情况下连续调用多次,错误就会很容易被忽略。
技术讨论: 注意上述代码中定义的 _min_sizesampled 行。我们选择这样定义是因为 Hypothesis 倾向于 favor 值接近于0 的整数值,以便促进缩减。然而,为了改善搜索空间的探索,有时能够在交易序列中对所有可用函数进行采样是更好的,这也是我们没有直接定义它为 min_size_sampled = draw(st.integers(0,len(operations)-1)) 的原因,否则 Hypothesis 几乎永远无法在合约具有大量函数的情况下采样使用所有可用函数的序列。出于类似原因,保持 _favor_longsequence 的默认值为真是更好的,因为我们希望鼓励长的交易序列来深入探索更深层次的Bug。
你可以通过运行以下命令查看群体测试的实力:
python fuzzer.py tests/swarm_test.sol
这将测试以下合约:
contract InvariantBreaker {
uint counter = 0;
bool public flag1 = true;
function reset(int256 val) public {
counter = 0;
}
function set(int256 val) public returns (bool) {
counter = counter + 1;
if (counter == 50) {
flag1 = false;
}
return flag1;
}
}
contract InvariantTest {
InvariantBreaker public inv;
function setUp() public {
inv = new InvariantBreaker();
}
function invariant_neverFalse() public returns (bool) {
return inv.flag1();
}
}
使用默认的 config.yaml,群体测试被激活,反例将在几秒钟内被找到:
Falsifying example: composite_test(
ops=[(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
...
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0),\
(<Function set>, 0)],
)
Invariant broken
然而,如果你更改 config.yaml 将 _swarmtesting 设置为 false,你几乎无法在 “仅有” 1000 笔交易的情况下打破不变!这是因为模糊测试器几乎是随机选择要调用的函数,因此极不可能仅随机选择 set() 函数连续调用50次而不调用 reset()。在合约中,reset() 是一个吸收状态,因为它每次调用时都会将 counter 变量重置为0。
类似于专业模糊测试器如 Echidna 的做法,我们使用一些静态分析来挖掘被测合约中的硬编码常量,以指导模糊测试器有时在这些常量中进行采样。确实,在现实世界的合约中,硬编码常量经常在如果语句中的等式中使用,例如随机模糊测试器几乎不会到达这样的分支:if (x==43685820975004) 如果 x 是随机生成的。我们使用 slither 从抽象语法树中提取硬编码常量,并将它们添加到 Hypothesis 策略中,针对相应的变量类型。你可以通过运行以下命令测试此功能:
python fuzzer.py tests/constants_test.sol
这将测试以下合约:
contract InvariantBreaker {
bool public flag0 = true;
function set0(string memory val) public returns (bool) {
if (keccak256(abi.encodePacked(val)) == keccak256("fuzzinglikeadegen"))
flag0 = false;
return flag0;
}
}
contract InvariantTest {
InvariantBreaker public inv;
function setUp() public {
inv = new InvariantBreaker();
}
function invariant_neverFalse() public returns (bool) {
return inv.flag0();
}
}
正如你所看到的,模糊测试器必须生成一个非常特定的字符串“ fuzzinglikeadegen” 来打破不变。这仅在 _constantsmining 被激活时工作(默认情况下是)。
为了实现覆盖引导,我使用 _debugtraceTransaction 调用监控每笔交易,然后提取每笔交易中到达的程序计数器列表。这是可接受的,因为它仅为运行代码增加了10%的时间开销。如果在交易序列中首次到达新的程序计数器,我们将给与相应的交易序列很高的奖励,以鼓励模糊测试器探索类似的交易。这是通过将奖励传递给 Hypothesis 库的 target 函数完成的,该函数允许定向基于属性测试(见 文档)。
默认情况下,_coverageguidance 选项处于激活状态,似乎在需要全面深度探索的情况下有一些帮助,但暂时将其视为实验性,我正尝试以多种方式进行改进。目前,仅基于程序计数器频率的方法可以在 GitHub 上使用,但我还尝试了一种更细致的方法,即取交易中到达的程序计数器列表的哈希。前者的方法类似于语句覆盖,而后者则是计算路径覆盖的一种方式(即考虑到到达的程序计数器的顺序)。更多技术细节可以在 代码 中找到。请随时测试并告诉我你的结果!
这个 alpha 版本只是我所设计的智能合约模糊测试器的初步草图。也许 Hypothesis 并不是区块链上有状态属性测试的最佳后端,但我尽力而为。我的目标是更多地了解模糊测试软件的内部工作,而不是做出最快或最好的模糊测试工具。我鼓励有动力的读者查看 README 文件中的长长待办事项列表,其中包含我想实现的特性。
此外,使用 Python 编写模糊测试器的初始动机之一,除了编程语言的巨大多功能性和用户友好性,还在于为 Pythonista 提供的巨大且无与伦比的机器学习生态系统。我将很快探索基于学习的技术如何以更聪明的方式指导模糊测试器。有关此主题的良好起始参考可以在这篇 优秀论文 的“基于学习的技术”部分中找到,作者为 Zhang 等。
- 原文链接: medium.com/@jat9292/buil...
- 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,在这里修改,还请包涵~
如果觉得我的文章对您有用,请随意打赏。你的支持将鼓励我继续创作!