Web3 中的自动化安全：静态分析 vs. 动态分析 – ImmuneBytes

2025年6月10日

介绍

作为一家 Web3 安全公司，我们花费了无数时间剖析智能合约和区块链代码库，寻找可能成就或毁掉区块链应用程序的漏洞。审计最基本的方面之一是选择正确的方法来分析合约。我们是不运行就逐行分解它，还是对其进行严格的测试，以了解它在真实条件下的行为？

答案是两者兼有。

静态分析和动态分析是我们武器库中的两个关键框架，理解它们如何工作对于任何认真确保智能合约安全的人来说至关重要。静态分析让我们在合约运行之前就能发现问题，而动态分析帮助我们发现只有在执行过程中才会出现的漏洞。

让我们分解一下每种方法带来的好处，以及为什么我们同时使用这两种方法来确保被测程序（PUT）万无一失。

静态分析：在执行前识别漏洞

静态分析就像在不部署或执行合约的情况下进行安全审查。它通常是任何彻底的智能合约审计的第一步。通过检查代码，我们可以识别逻辑、结构和安全实践中的漏洞，这些漏洞可能会在编译时破坏或损害实现。

静态分析最大的优势之一是速度。自动化工具可以在几秒钟内扫描成千上万行代码，标记潜在问题，如重入攻击、未初始化的变量和整数溢出。但作为审计员，我们不仅仅依赖框架；相反，一旦扫描器标记出任何问题，我们就会手动检查这些发现，验证其合法性，并在这些基础上构建更复杂的漏洞，这些漏洞可能是自动化扫描器遗漏的。

静态分析中的关键技术

程序语义

程序语义是指研究程序如何执行以及它们的含义。它提供了一个正式的框架来理解程序的行为，确保软件（包括智能合约）的行为符合预期。

其工作原理：

• 操作语义： 根据状态变化描述执行行为，通常使用抽象机器。
• 指称语义： 将程序含义表示为数学函数，使其可用于推理正确性。
• 抽象释义： 逼近程序行为以检测可能的错误，而无需执行代码。

在智能合约审计中的应用：

• 帮助形式化验证正确性属性，确保合约执行与预期一致。
• 能够进行安全证明，例如验证函数始终返回正确的值。
• 可用于建模和分析执行路径以检测意外行为。

示例：

• 操作语义定义了以太坊智能合约如何在执行期间更新状态变量。
• 安全研究人员可以使用指称语义来用数学方法证明合约永远不会进入无效状态。

数据流分析

数据流分析检查数据如何通过程序，帮助检测潜在问题，如未使用的变量、死代码和安全风险。

其工作原理：

• 分析变量生命周期和信息流通过控制流图。
• 使用常量传播、活动变量分析和污染分析等技术来检测问题。
• 通过识别冗余计算和无法访问的语句来帮助优化代码。

在智能合约审计中的应用：

• 检测死代码，确保未使用的函数不会引入攻击面。
• 识别受污染的数据源，这可能导致漏洞，如未检查的外部调用。
• 通过检测不必要的存储操作来帮助防止 Gas 效率低下。

示例：

• 到达定义分析有助于确定变量是否在 Solidity 合约中使用之前已被赋值。
• 这可以防止未初始化的变量漏洞，攻击者可以利用未定义的状态来操纵合约执行。

过程间分析

过程间分析检查数据和控制如何在多个函数之间流动，而不仅仅是在单个函数内部。

其工作原理：

• 使用调用图来映射函数之间的关系。
• 跟踪跨函数依赖关系以检测由函数交互引起的错误。
• 帮助识别由函数调用引起的副作用。

在智能合约审计中的应用：

• 检测合约函数之间意外的交互，防止安全缺陷。
• 通过消除冗余函数调用来帮助优化合约。
• 确保在多个合约组件之间正确执行访问控制。

示例：

• Solidity 智能合约中的调用图分析可确保旨在供内部使用的函数不会意外地暴露给外部调用者。
• 这可以防止不正确的访问控制漏洞，例如外部攻击者利用内部辅助函数。

指针分析

指针分析确定指针（或引用）如何在程序中交互，以检测内存错误、别名问题和性能瓶颈。

其工作原理：

• 识别别名，其中多个变量引用相同的内存位置。
• 检测悬空引用，这可能导致安全漏洞。
• 用于 C、C++ 等语言和低级字节码分析，但也适用于智能合约中的存储指针管理。

在智能合约审计中的应用：

• 确保基于 EVM 的合约中的安全内存和 calldata 堆栈处理。
• 帮助检测由于别名引起的意外合约状态修改。
• 通过识别不必要的存储操作来帮助进行 Gas 优化。

示例：

• 在 Solidity 中，mapping 类型充当对随机存储位置的引用。处理不当可能导致数据损坏或意外写入存储。
• 指针分析技术可以识别由于不正确的索引计算而导致一个 mapping 意外覆盖另一个 mapping 的情况。

字节码分析

字节码分析涉及检查由虚拟机（例如，以太坊虚拟机）执行的程序的低级表示。 它对于验证编译后的智能合约至关重要。

其工作原理：

• 分析编译后的 EVM 字节码，以检测源代码级别不可见的漏洞。
• 使用模式匹配、控制流分析和符号执行。
• 帮助确保优化不会引入安全风险。

在智能合约审计中的应用：

• 检测静态分析工具在源代码级别可能遗漏的模糊处理的漏洞。
• 帮助验证编译器正确性，确保 Solidity 到 EVM 的转换不会引入缺陷。
• 识别错误编译问题，防止意外的操作码行为。

示例：

• Solidity 智能合约的字节码分析可以揭示意外的 Gas 使用模式，确保合约遵守最佳实践。
• 它还可以检测隐藏的后门，例如原始源代码中不存在但通过字节码修改引入的自毁调用。

静态分析的局限性

虽然静态分析非常适合尽早发现问题，但它并不完美。它倾向于产生误报，这意味着它有时会标记实际上无法利用的问题。此外，它没有告诉我们合约在真实的区块链环境中的行为方式。一些漏洞只有在合约方法被执行时、与其他智能合约交互时、发生可变区块链环境状态时或存在不可预测的用户输入时才会出现。

动态分析：将合约投入测试

如果静态分析是阅读建筑物的蓝图，那么动态分析就是从内部和外部测试实际建筑物的结构。此方法涉及在不同环境中执行合约，以观察其在各种条件下的行为。它帮助我们发现静态分析可能遗漏的问题，如意外的状态变化、gas 效率低下和执行失败。

当我们进行动态分析时，我们会查看合约如何处理边缘情况，针对高交易量和不可预测的输入进行压力测试。此方法提供了真实世界的见解，对于确保安全性和可靠性至关重要。

动态分析中的关键技术

符号执行

符号执行是一种强大的技术，用于智能合约安全分析，有条不紊地探索合约的执行路径并在部署前检测漏洞。它不是使用实际值执行合约，而是使用符号变量来表示输入，允许审计员分析所有可能的执行路径，而无需手动测试每个场景。

它是如何工作的

1. 符号输入赋值
   • 合约不是使用真实的交易输入（例如，msg.sender = 0x123…）执行，而是使用符号变量（X、Y、Z）执行。
   • 这意味着每个函数和条件都会针对所有可能的值进行评估，从而更容易检测到边缘情况。
2. 路径探索与约束求解
   • 执行引擎有条不紊地探索所有可行的执行路径。
   • 每个条件（例如，if (balance > 100)）都会创建一个分支，从而导致不同的可能结果。
   • 可满足性模理论 (SMT) 求解器确定是否可以执行每个路径。
3. 漏洞检测
   • 该工具会标记无法访问的代码、无效的状态转换、整数溢出和访问控制缺陷。
   • 如果路径导致不安全的状态（例如，允许未经授权的访问），它会生成一个测试用例来演示利用。

示例

存在漏洞的代码：

使用符号执行，我们设置：

• a = X（符号值）
• b = Y（符号值）

求解器检查 X + Y > 2^256 – 1，确认是否可能发生溢出。

基于可满足性模理论 (SMT) 的技术

基于 SMT 的技术涉及使用自动推理通过求解逻辑约束来分析智能合约。 这些技术利用 SMT 求解器通过将合约逻辑编码为数学公式来验证合约的正确性、安全性和功能行为。

SMT 求解器是一种工具，用于确定给定的逻辑公式是否可满足，这意味着是否存在使公式成立的值分配。

其工作原理：

1. 代码的正式表示：
   • 合约的逻辑被转换为涉及数学理论（例如，算术、按位运算和布尔逻辑）的逻辑公式。
   • 这是使用中间表示 (IR) 技术完成的。
2. 约束生成：
   • 智能合约的执行路径被编码为约束。
   • 这些约束定义了可能发生某些漏洞的条件（例如，“在什么条件下可以发生溢出？”）。
3. 自动推理：
   • SMT 求解器（例如，Z3、CVC4、Yices）尝试通过求解约束来证明或反驳漏洞的存在。
   • 如果存在不安全状态的可满足解，则该合约存在漏洞。
   • 如果求解器证明不存在解，则该合约对该特定问题是安全的。

SMT 分析中使用的常见理论

SMT 求解器同时处理多个数学理论。 在智能合约分析中，最相关的包括：

混合执行测试

混合执行测试（具体和符号执行的组合）是一种通过分析实际输入（具体执行）和抽象符号值（符号执行）来自动生成测试用例的技术。 它对于检测边缘情况和最大化代码覆盖率特别有用。

其工作原理：

• 具体执行： 程序使用实际输入运行，以观察其在正常条件下的行为。
• 符号执行： 使用符号变量而不是具体值来分析相同的执行路径。 这有助于确定原始测试中未涵盖的替代执行路径。
• 约束求解： 系统通过求解从符号执行导出的约束来生成新的测试用例，确保探索程序中的新路径。
• 迭代优化： 重复该过程，逐渐增加测试覆盖率并识别难以访问的漏洞。

在智能合约审计中的应用：

• 检测边缘情况： 混合执行测试有助于发现智能合约中的极端情况漏洞，例如整数溢出、重入和访问控制缺陷。
• 最大化代码覆盖率： 确保测试尽可能多的执行路径，从而使安全审计更加健壮。
• 改进模糊测试： 通过提供更结构化的方式来探索执行路径，可以很好地与模糊测试结合使用。

示例：

• 用于 Solidity 的混合执行测试工具使用实际输入和符号输入来执行智能合约。 如果交易正常执行而没有失败，但符号执行显示仅在特定条件下触发的隐藏漏洞，则该工具会生成一个新的测试用例来确认该问题。
• 例如，如果某个函数对大多数用户行为正确，但当发送者的地址具有特定字节模式时失败，则混合执行测试可以发现这种罕见但可利用的缺陷。

动态分析的局限性

虽然动态分析功能强大，但也面临着挑战。它需要更多的计算资源和时间，因此与大型代码库的静态分析相比，它的可扩展性较差。此外，我们无法测试所有可能的执行路径，这意味着某些漏洞可能仍未被检测到。静态与动态分析：谁胜出？

事实是，仅靠一种方法是不够的。作为审计员，我们见过静态分析标记了潜在问题，但动态分析证明是无害的情况，也见过动态分析揭示了静态分析完全遗漏的安全缺陷的情况。

以下是两种方法的快速比较：

为什么我们应该同时使用两者

建议永远不要只依赖一种方法。 静态分析有助于在过程的早期识别潜在的漏洞，而动态分析验证这些发现并发现仅在执行期间出现的其他问题。 将这两种技术结合使用可以进行更彻底，更有效的审核。

通过结合静态分析和动态分析，我们可以：

• 检测代码结构和执行中存在的漏洞。
• 验证理论上的漏洞是否构成真正的威胁。
• 在部署前后加强智能合约的安全性。
• 最大程度地降低未检测到可能导致漏洞利用的漏洞的风险。

最后想法

智能合约安全不仅仅是运行工具或遵循清单。 它需要对代码和执行行为有深刻的理解。 静态分析和动态分析是同一枚Coin的两个方面，每个方面都在保护区块链应用程序中起着至关重要的作用。

作为审计员，我们的目标应该是确保我们审查的每个智能合约在上线之前都尽可能安全。 通过利用静态分析和动态分析，我们可以构建更具弹性、值得信赖和高效的智能合约，这些合约可以在不断发展的 Web3 世界中经受住时间的考验。

• 原文链接： blog.immunebytes.com/202...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～