Solar：Solidity的无上下文交互式分析 - Trail of Bits博客

Trent Brunson
2021年4月2日
区块链, 实习项目

我们正在招聘研究与工程团队成员！
作者：Aaron Yoo，加州大学洛杉矶分校

作为Trail of Bits的实习生，我开发了Solar——一个概念验证静态分析框架。Solar的独特之处在于它能够对Solidity智能合约进行无上下文的交互式分析。用户可以引导Solar探索程序路径（例如展开函数调用或跟踪if语句）并为变量分配约束或值，所有这些都无需参考具体执行。作为Solar的补充，我创建了一个类似集成开发环境（IDE）的工具，展示了Solar可提供的交互性和分析类型。

Solar用户界面

Solar用户界面有两个主要面板：“源代码”和“IR”（中间表示）。源代码面板显示正在分析的函数的源代码，IR面板将这些函数翻译成SlithIR的增强变体——我们的开源IR。绿色高亮显示正在分析的函数行。这两个窗格显示类似信息但用途不同：源代码窗格作为地图，辅助导航并提供上下文；IR窗格支持交互性并可视化Solar推导的信息。

基于Solar构建的分析称为“策略”。策略是模块化的，每个策略定义了Solar的不同操作模式。上述截图展示了三种策略：具体、符号和约束。尽管每种分析有其自己的工作流，但Solar需要所有三种策略来支持简化、下调和上调原语，下文将详细解释。

Solar原语

简化

简化原语指示框架基于当前信息进行尽可能多的推断。Solar可以通过用户输入或从程序推导公理来接收新信息。在下面的屏幕录像中，Solar公理推导出常量2的值。如果用户告诉Solar假设x的值为5，然后点击“简化”按钮，Solar将推导返回值。

下调

下调原语指示框架内联函数调用。函数调用被内联，以便用户可以在一个窗格中查看整个路径。在传统IDE中，用户必须导航到相关函数。在我们的框架中，下调的函数直接内联到IR窗格，其源代码带入源代码窗格。

上调

上调原语将当前上下文内联到调用函数中。换句话说，上调意味着遍历调用栈向上，通常与下调相反。通过上调，Solar可以向上遍历程序路径通过函数调用，如下所示。（特别注意绿色高亮行。）

这三种原语共同赋予Solar其定义属性：上下文不敏感性和交互性。Solar是无上下文（上下文不敏感）的，因为用户可以从任何函数开始分析。它是交互式的，因为确切的程序路径由上调和下调决定——这些由用户选择。

整数溢出推理演示

Solar可以帮助用户推理非平凡程序属性，如整数溢出。考虑以下程序：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13

contract Overflow {
    function z(uint32 x, uint32 y) public returns (uint32) {
        uint32 ret = 0;
        if (x < 1000 && y < 1000) {
            will_it_overflow(x, y);
        }
        return ret;
    }

    function will_it_overflow(uint32 x, uint32 y) public returns (uint32) {
        return x * y;
    }
}

这里，我们想找出will_it_overflow是否会导致整数溢出。当算术操作的数学结果无法适应为其存储分配的物理空间时，会发生整数溢出。

查看will_it_overflow函数，很明显整数溢出是可能的，因为两个32位数字相乘并放入32位结果。然而，基于will_it_overflow的调用站点，如果z调用will_it_overflow，则永远不会发生整数溢出；这是因为z验证了will_it_overflow的参数很小。让我们看看Solar如何得出这个结论。

使用Solar执行此分析需要使用约束策略，该策略通过尝试找到程序的单个有效执行来工作。用户可以用任意多项式约束来约束执行。要开始分析，我们从左窗格选择will_it_overflow函数，将其指示为所需的起点。以下是初始分析视图：

Solar提供一个可能的执行，将所有值评估为零。下一步是约束x和y的值。我们可以向约束策略提供以下约束（以IR变量表示，而非源代码变量）：

• x_1 < (2 ** 32)
• y_1 < (2 ** 32)
• x_1 * y_1 >= (2 ** 32)

前两个约束将x_1和y_1绑定到32位整数。第三个导致求解器尝试找到x_1 * y_1溢出的执行。通过显示属性的否定不可满足，使用SAT/SMT求解器证明属性是常见做法。考虑到这一点，我们将使用Solar显示没有x_1 * y_1溢出的执行，从而暗示will_it_overflow不会溢出。简化这些约束的使用后，我们得到以下结果：

再次，Solar基于约束提供一个可能的执行。上调一次将我们带到第5行：

由于绿色高亮行不形成逻辑矛盾，Solar仍然可以返回有效的程序执行。然而，再次上调返回不同的结果：

右侧的问号表示求解器无法找到给定程序路径的任何可能执行。这是因为第4行与我们之前写的不等式矛盾：x_1 * y_1 >= (2 ** 32)。上述步骤构成了非正式证明，如果从z调用will_it_overflow，溢出是不可能的。

结论

我为Solar的成果感到自豪。尽管它是一个原型，但Solar代表了一种新型分析平台，优先考虑交互性。考虑到代码审计和IDE风格语义检查的潜在应用，我期待看到Solar及其核心思想的未来。我要衷心感谢我的导师Peter Goodman，使这次实习有趣且充实。Peter完成了导师可能最具挑战性的任务：在提供指导和我思想自由之间取得微妙平衡。我还要感谢Trail of Bits主办这次实习。我期待看到未来实习生创建的激动人心项目！

如果你喜欢这篇文章，请分享： Twitter LinkedIn GitHub Mastodon Hacker News

页面内容 近期文章 使用Deptective调查你的依赖项 系好安全带，Buttercup，AIxCC的评分回合正在进行中！ 使你的智能合约超越私钥风险成熟 Go解析器中意外的安全陷阱 我们审查首批DKLs23库的收获 来自Silence Laboratories的23个库 © 2025 Trail of Bits。 使用Hugo和Mainroad主题生成。