Web3 中的自动化安全：静态分析对比动态分析 – ImmuneBytes

2026年3月5日

引言

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

答案是两者兼而有之。

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

让我们分解一下每种方法带来的优势，以及为什么我们同时使用它们来确保被测程序 (PUT) 坚不可摧。

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

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

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

静态分析中的关键技术

• 程序语义

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

工作原理：

• 操作语义： 使用抽象机器描述状态变化方面的执行行为。
• 指称语义： 将程序含义表示为数学函数，有助于推理正确性。
• 抽象解释： 近似程序行为以在不执行代码的情况下检测可能的错误。

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

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

示例：

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

数据流分析

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

工作原理：

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

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

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

示例：

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

过程间分析

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

工作原理：

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

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

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

示例：

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

指针分析

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

工作原理：

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

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

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

示例：

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

字节码分析

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

工作原理：

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

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

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

示例：

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

静态分析的局限性

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

动态分析：对合约进行测试

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

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

动态分析中的关键技术

1. 符号执行

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

工作原理

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

示例

有漏洞的代码：

function add(uint256 a, uint256 b) public pure returns (uint256) {
    return a + b; // 如果 a + b 超过 uint256 限制，可能发生溢出
}

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

• a = X (符号值)
• b = Y (符号值)

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

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

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

SMT 求解器是一种工具，用于确定给定的逻辑公式是否可满足，即是否存在使公式为真的值赋值。

工作原理：

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

SMT 基于分析中常用的理论

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

1. 混合测试

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

工作原理：

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

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

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

示例：

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

动态分析的局限性

虽然动态分析功能强大，但它也面临挑战。它需要更多的计算资源和时间，使其对于大型代码库而言不如静态分析可扩展。此外，我们无法测试所有可能的执行路径，这意味着一些漏洞可能仍然未被发现。

静态分析与动态分析：谁更胜一筹？

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

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

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

建议永远不要只依赖一种方法。静态分析有助于在过程早期识别潜在漏洞，而动态分析则验证这些发现并发现只在执行期间才会出现的额外问题。同时使用这两种技术可以实现更彻底、更有效的审计。

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

• 检测代码结构和执行中都存在的漏洞。
• 验证理论漏洞是否构成真实威胁。
• 在部署前后增强智能合约安全性。
• 最大限度降低因未被发现的漏洞而导致漏洞利用的风险。

最终思考

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

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

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