技术摘要：用于硬件设计信息流分析的增强型符号执行技术

问题陈述

验证硬件设计的安全性需要分析信息如何从源信号（输入）流向汇信号（输出）。不希望的信息流可能导致访问授权违规、内存泄漏或权限提升。虽然符号执行（Symbolic Execution, SE）是一种无需插桩即可追踪这些流向的精确工具，但它面临“路径爆炸”问题，即执行路径的数量会随着分支点的增加而呈指数级增长。此外，硬件设计通过多时钟周期推理引入了复杂性，使得实现从输入到输出的完整流向变得困难。现有的解决方案通常限制设计空间或仅分析较小的关键组件。

核心挑战在于：如何在限定的时间范围内，高效地区分可实现的（Realizable）信息流（数据实际移动的真实路径）与不可实现的路径（无法在执行中发生的静态分析伪影），并提供具体的输入序列来驱动这些流向。

方法论：SEIF

作者提出了 SEIF（发音为 "safe"），这是一种通过增强符号执行来验证并阐明信息流路径的方法。SEIF 运行在一个静态构建的信息流（Information Flow, IF）图之上，该图对 Verilog RTL 设计中的信号连接进行了过近似（Over-approximation）。

该方法分为三个主要阶段：

1. 剪枝全局不可实现的路径

在调用符号执行之前，SEIF 通过分析 IF 图来消除逻辑上不可能存在的路径。

• 分段（Segmentation）： 根据非阻塞赋值（Non-blocking assignments）将 IF 路径划分为段，这些赋值定义了时钟周期的边界。
• 约束检查（Constraint Checking）： 对于每个段，收集实现该流向所需的条件。SMT 求解器会检查共满足性（Co-satisfiability）。如果单个时钟周期段内的约束相互矛盾（例如，一个信号必须同时为高电平且为低电平），则该路径被视为全局不可实现并被丢弃。

2. 引导式符号执行

对于剩余的路径，SEIF 使用由 IF 图引导的符号执行，在设计状态中寻找可实现的执行路径。

• 引导搜索（Guided Search）： 执行引擎被限制为仅遵循那些包含实现当前 IF 图段所需的特定代码行的设计路径。这显著缩小了搜索空间。
• 时钟周期边界剪枝（Clock Cycle Boundary Pruning）： 在每个时钟周期，引擎会检查当前的符号状态是否满足下一个 IF 段的条件。如果不是，则指向该分支的路径会被剪枝。
• 停顿策略（Stalling Strategy）： 一个关键的创新是能够“停顿”IF 路径的推进。如果当前状态无法满足下一个段的条件，SEIF 会对设计进行一个时钟周期的符号执行，以推进机器状态，但不推进 IF 路径指针。至关重要的是，在停顿时，SEIF 会防止符号引擎探索会覆盖先前段中累积信息的路径（例如，防止寄存器被清空）。
• 搜索启发式算法（Search Heuristics）： 本文评估了四种搜索策略：
  1. 基准 1（Baseline 1）： 仅进行继续或停顿（组合的穷举搜索）。
  2. 基准 2（Baseline 2）： 仅进行回溯（不进行停顿）。
  3. 结合停顿与回溯（Stalling with Backtracking）： 一种混合方法。
  4. 结合停顿与 UNSAT Core 启发式（Stalling with UNSAT Core Heuristic）： 利用 SMT 求解器的 UNSAT core 来优先处理能减少约束冲突的停顿路径，从而有效地引导搜索向有效的下一状态迈进。

3. 语义分析与后处理

• 真流验证（True Flow Verification）： SEIF 执行语义检查以消除“假阳性”，即存在文本流但实际上没有信息传输的情况（例如，y = x XOR x）。
• 复位状态验证（Reset State Verification）： 工具会检查所找到的执行路径是否可以从设计的复位状态到达。如果不能，则将其识别为从中间状态开始的路径。

核心贡献

1. 定义 SEIF： 一种结合了静态分析（IF 图）与引导式符号执行，用于分析硬件信息流的新颖方法论。
2. 实现： 一个基于 Sylvia 符号执行引擎和 Hyperflow 图工具链构建的工具实现，并利用了 Z3 求解器。
3. 搜索启发式算法： 开发并评估了特定的搜索策略，特别是使用 UNSAT core 来引导停顿，以管理多时钟周期路径探索的复杂性。
4. 评估： 在四个开源设计（OR1200、openMSP430、AKER 访问控制和 AES 核心）上进行了全面的测试。

结果

评估是在一台配备 12 核处理器和 62GB 内存的双路服务器上进行的。

• 路径计数（Path Accounting）： SEIF 成功解释了静态构建的 IF 图中 86–90% 的路径。这是通过找到对应的可实现设计路径或证明该路径不可行来实现的。
• 真流（True Flows）： 在被解释的路径中，58–77% 被识别为真实的有效信息流，这表明静态 IF 图是一个很强的近似。
• 性能： SEIF 平均可在 4–6 秒内穷举探索深度达 10–12 个时钟周期的路径。
• 搜索策略有效性： UNSAT Core 启发式算法表现优于其他策略，它比基准方法多找到了 26% 的对应设计路径，并将平均搜索时间降低至每条路径 3–6 秒。与非启发式方法相比，它也显著减少了回溯的频率。
• 可扩展性： 在针对 MSP430 程序计数器的案例研究中，SEIF 在 16 个时钟周期的搜索范围内，为 19,060 个 IF 路径中的 89.93% 找到了设计路径。

重要性与声明

论文声称 SEIF 通过自动化区分静态分析伪影与实际安全违规的过程，为安全验证提供了一个新的视角。

• 精确性： 它消除了工程师手动追踪复杂的多周期流或猜测输入序列的需求。
• 可操作性： 当发现违规时，SEIF 提供一组具体的输入值，用于驱动设计沿着违规路径运行，该路径可以从复位状态或中间状态开始。
• 效率： 通过使用静态 IF 图来引导符号执行，SEIF 避免了纯符号执行固有的路径爆炸问题，从而能够分析比纯 SE 更深的周期和更大的设计。
• 局限性： 作者承认 SEIF 针对的是由规范和设计中良性人为错误引起的缺陷。它无法检测由恶意合成工具、制造或供应链攻击（例如，在验证后插入的模拟木马）引入的缺陷。此外，对于重敛扇出（reconvergent fan-out）场景，如果工具无法穷举探索所有设计路径，可能会报告错误的结果。