利用变异体改进 Slither
改进静态分析工具可能很困难;一旦你基于程序的有效表示实现了一个好工具,并添加了大量规则来检测问题,如何进一步增强工具的漏洞发现能力?
为静态分析器提出新规则和引擎升级的一种(必要)方法是使用“经验指导的智能”——对智能合约及其缺陷的深入了解、审计经验以及大量深入思考。然而,这种方法很困难,需要一定水平的专业知识。即使是最有经验的审计员使用这种方法也可能遗漏问题。
在我们发表于2021年IEEE国际软件质量、可靠性与安全会议的论文中,我们提供了一种替代方法:使用变异体将错误引入程序,并观察静态分析器是否能检测到它们。本文描述了这种方法,以及我们如何使用它为Slither(由Trail of Bits开发的静态分析工具)编写新规则。
使用程序变异体
改进静态分析工具的最常见方法是找到工具本应能够发现的代码错误,然后确定工具需要哪些改进来发现这些错误。
这就是程序变异体的用武之地。变异测试工具(如universalmutator)将程序作为输入,并输出程序的(可能巨大的)一组轻微变体。这些变体称为变异体。假设原始程序(大部分)正确,大多数变异体会给程序添加错误。
变异体最初设计用于帮助确定程序的测试是否有效(参见我个人博客上关于变异测试的文章)。测试套件无法检测到的每个变异体都暗示测试套件可能存在缺陷。将这个想法扩展到静态分析工具并不困难。
使用变异体改进静态分析工具
使用变异体改进整个测试套件与专门改进静态分析工具之间存在重要差异。首先,虽然期望一个好的测试套件检测几乎所有添加到程序的变异体是合理的,但期望静态分析工具这样做是不合理的;许多错误无法静态检测。其次,许多变异体会改变智能合约的含义,但不符合好代码或坏代码的一般模式。像Slither这样的工具不知道合约应该做什么。
这些差异表明,必须费力检查Slither未检测到的每个变异体,这将是痛苦的,且只有偶尔有成果。幸运的是,这不是必要的。只需查看那些1) Slither未检测到且2) 另一个工具检测到的变异体。这些变异体有两个有价值的属性。首先,因为它们是变异体,我们可以相当确信它们是错误。其次,它们原则上必须是可静态检测的:即使Slither没有检测到,其他工具检测到了!如果其他工具能够找到这些错误,我们显然希望Slither也能做到。变异体的性质与差异比较(这里指两个静态分析工具之间的比较)的结合给了我们想要的东西。
即使有这种只识别我们关心的错误的有用方法,可能仍然有太多需要查看。例如,在改进Slither的努力中,我们比较了它检测到的错误与SmartCheck和Securify检测到的错误(当时,这两个是可能的替代静态分析工具)。结果如下:
所有三个工具都检测到了一些非常明显的问题,但这18个变异体仅占所有检测到的变异体的不到0.5%。此外,每对工具都有100-400个变异体的显著重叠。然而,每个工具至少独特检测了1,000个变异体。我们自豪的是,Slither检测到的变异体总数最多,且独特检测的变异体也最多。事实上,Slither是唯一检测到大多数(近60%)任何工具检测到的变异体的工具。正如我们所希望的,Slither擅长发现可能的错误,特别是相对于它产生的警告总数。
然而,有1,256个SmartCheck检测到的错误和1,076个Securify检测到的错误Slither没有检测到!现在,这些工具在100个智能合约上运行了近50,000个变异体,每个合约只有大约25个错误。尽管如此,这仍然有很多需要查看!
然而,快速浏览Slither遗漏的变异体显示,许多彼此非常相似。与测试不同,我们不关心每个单独的错误——我们关心Slither未检测到的模式,以及Slither遗漏已知模式的原因。考虑到这一点,我们可以通过首先查看彼此差异最大的变异体来对它们进行排序。
首先,我们构建一个距离度量来确定两个给定变异体之间的相似性水平,基于它们在代码中的位置、它们引入的突变类型,以及最重要的,突变代码的实际文本。如果两个变异体以类似的方式改变类似的Solidity源代码,我们认为它们非常相似。然后,我们按相似性对所有变异体进行排名,所有非常相似的变异体排在底部。这样,前100个左右的变异体代表了代码模式中的大部分实际差异!
因此,如果有500个变异体将msg.sender更改为tx.origin,并且被SmartCheck和Slither检测到,这些工具往往对tx.origin过度偏执,甚至经常标记合法使用,我们可以立即忽略这些变异体;我们知道,Slither关于使用tx.origin的警告规则经过了大量思考。我们正是这样做的。
新规则(及启发它们的变异体)
现在让我们看看帮助我们设计一些新规则添加到Slither的变异体。这些变异体中的每一个都被SmartCheck和/或Securify检测到,但未被Slither检测到。所有这三个变异体代表了一类Slither本可以检测到但未检测到的真实错误:
显示布尔常量误用的变异体:
|
|
第一个变异体显示了一个基于布尔常量的分支。通过此代码的路径无法执行。这段代码充其量是令人困惑和无意义的;最坏的情况下,它是为测试或调试所做的更改的遗留物,不知何故进入了最终合约。虽然这个错误似乎很容易通过手动审查发现,但如果常量不是直接出现在条件中,而是通过布尔变量引用,可能很难注意到。
显示基于类型的同义反复的变异体:
|
|
这个变异体与第一个类似,但更微妙;一个布尔表达式似乎编码了一个真正的决策,但实际上,由于所用变量的类型(DiscountTTMTokenId6是一个无符号值),结果可以在编译时计算。这是一个隐藏布尔常量的情况,即使值出现在条件本身,人类如果不记住类型模型,可能很难发现。
显示精度损失的变异体:
|
|
最后一个变异体真正微妙。Solidity整数除法可以截断结果(回想一下Solidity没有浮点类型)。这意味着两个数学上等效的表达式在求值时可能产生不同的结果。例如,在数学中,(5 / 10) * 2 和 (5 * 2) / 10 有相同的结果;然而,在Solidity中,第一个表达式的结果是零,另一个结果是一。在可能的情况下,在Solidity中几乎总是最好先乘后除以避免精度损失(尽管有例外,例如当类型的大小限制要求先除时)。
识别这些候选后,我们为它们编写了新的Slither检测器。然后,我们在用于内部审查新检测器的语料库上运行这些检测器,并确认它们能够找到真实错误(且不会报告太多误报)。所有三个检测器已在Slither的公共版本中可用一段时间(分别作为boolean-cst、tautology和divide-before-multiply规则),并且divide-before-multiplying规则已经取得了两个成果,一个在2020年12月,另一个在2021年1月。
下一步是什么?
我们的工作证明,变异体可以是改进静态分析器的有用工具。我们很乐意继续使用这种方法向Slither添加规则,但不幸的是,据我们所知,没有其他静态分析工具能与Slither相媲美并得到认真维护。
多年来,Slither已成为学术研究人员的基本工具。如果您想在您自己的研究中利用其能力,请与我们联系。最后,如果您想加入我们的核心研究团队,请查看我们的空缺职位(安全顾问、安全学徒)。
如果您喜欢这篇文章,请分享: Twitter LinkedIn GitHub Mastodon Hacker News