Solar：无上下文交互式Solidity分析框架

作者：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可以通过用户输入或从程序中推导公理来接收新信息。在下面的屏幕录像中，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