💻 computer science

Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs

本文引入了分段组合（piecewise composition），这是一种针对硬件设计的创新符号执行技术，它利用模块化结构将路径探索任务卸载给 SMT 求解器，在直接分析 RTL Verilog 而无需网表转换的情况下，实现了 97% 的运行时缩减以及路径探索数量级级的降低。

原作者： Kaki Ryan, Cynthia Sturton

发布于 2026-07-22

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Kaki Ryan, Cynthia Sturton

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你是一名试图在一座巨大的、充满未来感的城市中破解谜团的侦探。这座城市其实是一块计算机芯片，是一块控制着从你的手机到绕地球运行的卫星等一切事物的微小硅片。为了确保这座城市的安全，你需要检查每一条街道、每一个小巷和每一扇隐藏的门，以确保没有坏人能溜进来或破坏规则。这个科学领域被称为“硬件验证”（hardware verification），它在数字领域相当于一名安全检查员，在人们开车经过之前，确保大桥不会坍塌。

侦探们用来执行这项工作的核心工具被称为“符号执行”（symbolic execution）。符号执行并不是拿着一套特定的钥匙走过一条条街道，它更像是一张神奇的地图，让你能同时走过所有可能的街道。你用代表任何数字的“幽灵”来替换具体的数字，并观察这座城市对每种幽灵般可能性的反应。问题在于，随着城市变得越来越大、越来越复杂，街道的数量会呈爆炸式增长，以至于检查所有街道变得不再可能。这被称为“路径爆炸问题”（path explosion problem）。这就像试图用消防水龙头喝水；水（或者说，需要检查的路径数量）喷涌得太快了，导致你在找到漏水点之前就已经被淹没了。如果我们无法检查每一条路径，我们可能会错过黑客用来窃取秘密或导致系统崩溃的隐藏陷阱。

这就是论文《应对硬件设计符号执行中的路径爆炸问题》（Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs）发挥作用的地方。作者 Kaki Ryan 和 Cynthia Sturton 引入了一种聪明的策略，称为“分段组合”（piecewise composition）。他们意识到，与其试图同时走遍整座城市，不如将城市视为由一个个“街区”（或称“模块”）组成的。你可以分别探索每个街区，绘制出该单一街区内所有可能的路线，然后使用一个超级智能的计算器（称为 SMT 求解器）来计算这些独立的地图如何相互衔接。

把这想象成是在解一个巨大的拼图。旧的方法是试图将每一块碎片逐一强行放入位置，希望最终能呈现出图像。如果拼图有一百万块，你会永远在那里忙碌。新的“分段组合”方法则像是先将碎片分类成易于处理的小堆。你先解决“天空”堆，然后是“海洋”堆，最后是“树木”堆。一旦你得到了这些较小堆的解决方案，你就进行一次快速检查，看看它们是如何连接的。论文表明，这种方法不仅仅是略有帮助，它极大地减少了工作量。在对包括复杂的 CPU 和系统级芯片（SoC）在内的五种不同的开源设计进行测试时，这种方法将引擎需要探索的路径数量减少了约 92% 到 99%。

结果令人瞩目。新引擎比旧方法快了 97%。它成功地在以前难以彻底检查的设计中发现了安全漏洞和规则违规。例如，在测试一个名为 OR1200 的特定处理器内核时，该引擎发现了 30 个已知漏洞中的 27 个，而之前的工具发现的数量较少。作者强调，这不仅仅是一个理论构想；他们构建了一个能够读取用于构建这些芯片的实际代码（Verilog）并产生“反例”（counter-example）——即证明漏洞存在的特定指令集——的实用工具。

然而，论文也谨慎地指出，这并不是能瞬间解决一切的魔杖。该方法依赖于硬件采用模块化设计，即具有清晰且不会以混乱方式重叠的独立模块。如果一个设计具有某些混乱的连接（例如两个部分试图同时向同一内存写入数据的“写-写”依赖关系），该工具会停止运行并报告错误，而不是进行猜测。但对于绝大多数结构良好的硬件设计而言，这种新方法提供了一种驯服“可能性消防水龙头”的方法，使得确保我们的数字城市安全、可靠并面向未来变得更加容易。

技术摘要：通过分片组合解决硬件设计符号执行中的路径爆炸问题

问题陈述
符号执行是硬件设计的一种强力验证工具，能够通过将具体输入值替换为符号来推广测试，从而探索所有可能的执行路径。然而，它深受“路径爆炸”问题的困扰。在传统的符号执行中，需要探索的路径数量随设计中分支点（控制流语句）的数量呈指数级增长。对于复杂的硬件设计，这种指数级增长使得全量探索在计算上变得难以实现。以往缓解该问题的尝试包括将符号执行与模型检测相结合、利用具体执行轨迹，或将分析限制在小型设计上，但这些方法往往无法扩展到大规模、真实的寄存器传输级（RTL）设计。

方法论：分片组合（Piecewise Composition）
作者引入了分片组合技术，该技术利用硬件设计的固有模块化结构，将路径探索的负担从符号执行引擎转移到可满足性模理论（SMT）求解器上。

核心概念： 该方法并非将整个设计视为一个单一的整体控制流图进行探索，而是将设计分解为独立的块（具体为 Verilog always 块）。引擎在每个时钟周期内对每个独立块仅进行一次符号化探索，从而为每个块生成一组路径片段（树）。
通过 SMT 进行组合： 为了重建完整的根到叶路径或验证断言，引擎使用 SMT 求解器来组合这些独立的路径片段。求解器根据这些片段的路径条件和符号存储（symbolic stores），检查组合不同块中的特定片段的可行性。
复杂度降低： 对于一个拥有 $N$ 个独立 always 块、且每个块最多包含 $b$ 个二进制分支点的设计，传统符号执行需要探索 $O(2^{bN})$ 条路径。分片组合将复杂度降低为探索 $O(2^b \cdot N)$ 条路径。复杂度仅随单个块内的分支点呈指数级增长，而随块的数量呈线性增长。
处理依赖关系： 该方法考虑了块之间的各种数据依赖关系：
- 读-读（Read-Read）： 块可以分别进行探索；SMT 求解器会过滤掉共享变量存在冲突的不可行组合。
- 读-写（Read-Write）： 非阻塞赋值确保在一个周期内，一个块中的更新不会与另一个块中的读取发生冲突。
- 写-写（Write-Write）： 工具会检测并对存在写-写依赖的情况报错，因为这违反了 Verilog 的最佳实践。
实现细节： 该引擎直接在 Verilog RTL 上运行，无需转换为 C 或网表。它通过在探索顺序块之后根据“脏”（dirty）信号重新评估赋值，来处理组合逻辑。它支持多个时钟周期，通过在周期边界合并状态来实现，并包含了诸如处理重复子模块（通过 SMT 合并结果）以及利用影响锥（COI）分析来剪枝无关块等优化措施。

主要贡献

定义分片组合： 一种正式的技术，通过将路径组合逻辑转移到 SMT 求解器，利用硬件模块化特性来对抗路径爆炸。
符号执行引擎： 设计并实现了一个用于 Verilog RTL 的周期精确（cycle-accurate）引擎，该引擎利用分片组合技术，直接在源代码上运行。
实证评估： 在五个开源设计（包括 SoC 和 CPU 架构，如 OR1200、PULPissimo、openMSP430 等）上进行了全面的评估，使用了 84 个安全性关键断言。

结果
评估表明，该技术在性能提升和发现断言违例方面的有效性：

路径减少： 与传统的符号执行相比，分片组合减少了 92%–99% 的代码行访问量以及 64%–99% 的分支点访问量。
运行时间： 该技术使总运行时间平均减少了 97%。在对 MC68HC11 SPI 设计进行全量探索时，引擎仅探索了所需代码行的约 7% 和分支点的约 4%。
求解器效率： 与担心组合过程可能导致 SMT 查询复杂度爆炸的观点相反，探索路径的减少导致 SMT 查询次数平均减少了 18%，求解时间减少了 21%。
缺陷检测： 该引擎在所有五个设计中都成功发现了断言违例。具体而言，它在 Hack@DAC SoC 中识别出 31 个漏洞中的 24 个，在 OR1200 处理器中识别出 30 个漏洞中的 27 个。
对比： 该工具在不到 2 分钟的时间内找到了与同类设计中的漏洞，而之前的最先进工具（如 Coppelia、RTLConTest）则需要数小时才能找到类似的漏洞。

意义与主张
论文声称，分片组合为扩展符号执行以应对大型硬件设计提供了一条可行路径，且不会牺牲 RTL 级的分析粒度。通过解耦独立硬件模块的探索，并依靠现代 SMT 求解器来重新组合它们，该方法在保持单个路径信息优势的同时，减轻了搜索空间的指数级增长。作者断言，这种方法能够验证复杂的 SoC 和 CPU，而这些设计此前对于符号执行而言是难以处理的，并能提供直接可追溯至原始 RTL 设计的精确反例。这项工作被视为硬件安全验证领域的一大进步，使得检测真实世界设计中的断言违例和潜在漏洞成为可能。

类似论文