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面板支持交互并可视化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