💻 computer science

Efficient Symbolic Execution of Software under Fault Attacks

本文提出了一种针对软件故障攻击安全性的高效符号执行方法，通过自动程序转换实现精确的故障建模，并结合两种剪枝技术优化符号执行算法，在提升检测准确性的同时显著提高了分析效率。

原作者： Yuzhou Fang, Chenyu Zhou, Jingbo Wang, Chao Wang

发布于 2026-04-27

📖 1 分钟阅读☕ 轻松阅读

原作者： Yuzhou Fang, Chenyu Zhou, Jingbo Wang, Chao Wang

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

1. 背景：什么是“故障攻击”？（特工的“干扰弹”）

想象一下，你正在玩一个闯关游戏，你的角色（软件）正在按照既定的路线（程序逻辑）走：遇到门就开门，遇到陷阱就跳过去。

但是，有一个坏蛋（攻击者）在旁边。他并不直接修改你的游戏代码，而是通过物理手段（比如用激光晃你的眼睛，或者用电磁波干扰你的游戏机）来制造“故障”。

这种故障就像是坏蛋扔出的**“干扰弹”**：

原本你应该“跳过陷阱”，但干扰弹让你“直接撞上去”；
原本你应该“执行指令A”，但干扰弹让你“直接跳过了这一步”，导致你走错了路。

问题来了： 程序员怎么知道，如果坏蛋扔了干扰弹，程序会不会直接“死机”或者“泄露密码”呢？

2. 现状：现有的方法有什么问题？（“模拟演习”太假或太慢）

以前科学家有两种办法来测试，但都有缺陷：

方法 A（模拟太假）： 就像是模拟演习时，假设坏蛋能精准地改变你的“心情”（改变 CPU 的标志位）。但这不符合现实，坏蛋扔干扰弹是乱来的，他没法精准控制你的心情，他只能让你的动作“失灵”（比如让一个“跳跃”指令直接失效）。
方法 B（模拟太慢）： 就像是你要测试所有可能的干扰情况，结果发现干扰的可能性太多了，模拟器跑了几天几夜还没跑完，这叫“路径爆炸”。

3. 本文的创新：两件“黑科技”武器

这篇论文提出了两件厉害的武器，让模拟演习既真实又飞快。

第一件武器：精准的“故障建模”（更真实的剧本）

作者不再假设坏蛋能控制你的“心情”，而是模拟最真实的**“动作失灵”**。

比喻： 以前的模拟是假设：“如果坏蛋让你觉得路是通的，你就走过去。”
现在的模拟是： “如果坏蛋让你**‘忘了跳跃’**，你会不会掉进坑里？”
这种模拟方式更接近现实中黑客攻击硬件的方式（比如让跳转指令变成“空指令”），所以能发现以前发现不了的危险。

第二件武器：高效的“路径剪枝”（聪明的演习导演）

为了解决“模拟太慢”的问题，作者当了一回聪明的“演习导演”。

比喻： 假设演习有 100 条路线。导演发现，虽然路线 1、2、3 的开头不一样，但到了第 10 步之后，它们其实都在走同一条走廊。
导演的操作： “既然路线 1 已经走过这条走廊并证明是安全的了，那么路线 2 和 3 只要进入这条走廊，就直接宣布‘安全通过’，不用再走一遍了！”
这种技术叫做**“路径总结”**。它通过数学计算，识别出哪些路是“重复劳动”，直接把重复的路给“剪掉”了。

4. 总结：研究成果如何？（演习大获全胜）

通过实验证明，这套新方法非常牛：

更敏锐： 它能抓到以前方法漏掉的“安全漏洞”（发现更多真实的危险）。
更聪明： 它不会被“假危险”骗了（减少了误报）。
更神速： 相比于老方法，它的运行速度提升了好几个数量级（可能从跑几天缩短到几分钟）。

一句话总结：
这篇论文发明了一种更像真实攻击、且跑得飞快的“模拟器”，让开发者能在黑客动手之前，就提前预知软件在硬件受损时会不会“翻车”。

这是一篇关于在硬件故障攻击（Fault Attacks）环境下，如何高效且准确地进行软件符号执行（Symbolic Execution）的研究论文。以下是该论文的详细技术总结：

1. 问题背景与挑战 (Problem)

在嵌入式系统中，攻击者常通过物理手段（如电压毛刺、电磁波、激光等）注入硬件故障，导致 CPU 执行异常。这种攻击可能导致软件违反安全属性（如跳过关键的权限检查指令）。

现有的分析方法主要面临两大瓶颈：

故障建模不准确 (Inaccurate Fault Modeling)： 现有技术（如 Test Inversion）通常假设故障会翻转 CPU 的标志位（Flag），但这并不符合实际物理过程。实际攻击中，故障更常表现为将跳转指令（Jump Instruction）变为空操作（NOP），即“指令跳过”（Instruction Skipping）。
分析效率低下 (Inefficient Fault Analysis)： 硬件故障会引入大量的异常执行路径，导致符号执行中经典的“路径爆炸”（Path Explosion）问题被进一步放大，使得分析大规模程序变得极其缓慢。

2. 核心方法论 (Methodology)

为了解决上述问题，作者提出了两种核心技术：

A. 基于程序转换的精确故障建模 (Accurate Fault Modeling via Program Transformation)

作者不再将故障建模作为分析过程的一部分，而是将其实现为一个独立的程序转换阶段。

原理： 利用编译器在中间表示（IR）层级自动为程序添加辅助变量（Fault Flags）。
实现： 对于程序中的每一个跳转指令（无论是条件跳转还是无条件跳转），转换算法都会在其前方插入一个新的分支。这个新分支由一个符号化的“故障标志位”控制：
- 如果标志位为 false（无故障），程序按原逻辑执行。
- 如果标志位为 true（发生故障），程序将直接跳过当前的跳转指令，执行下一条指令（模拟 NOP 效果）。
优点： 这种模型能够精确模拟“指令跳过”这一实际攻击行为，且转换后的程序可以被任何下游符号执行工具处理。

B. 高效的冗余路径剪枝算法 (Efficient Redundancy Pruning)

为了应对路径爆炸，作者设计了一种结合了“故障饱和”与“路径摘要”的剪枝策略：

故障饱和剪枝 (Pruning Based on Fault Saturation)： 引入“故障预算”（Fault Budget $\beta$ ）的概念。一旦当前执行路径激活的故障数量超过 $\beta$ ，立即终止该路径的探索。
基于路径摘要的剪枝 (Pruning Based on Path Summary)： 这是本文的核心创新。
- 路径摘要： 利用**最弱前置条件（Weakest Precondition, WP）**来计算已探索路径的“摘要”。
- 冗余检测： 当符号执行遇到一个已探索过的程序位置（Location）时，检查当前路径的路径条件（Path Condition）是否被该位置已有的路径摘要所覆盖。
- 逻辑： 如果当前路径条件是已有摘要的一个子集，说明从当前点出发的所有可能行为在之前已经探索过了，因此可以直接跳过该路径的后续执行（Suffix），从而避免重复计算。

3. 主要贡献 (Key Contributions)

新模型： 提出了一种基于指令跳过（Instruction Skipping）的自动程序转换技术，比传统的标志位翻转模型更符合物理实际。
新算法： 开发了一种结合 WP 路径摘要和故障饱和的符号执行算法，专门针对故障诱导的路径爆炸进行了优化。
新工具： 基于 LLVM、KLEE 和 Z3 构建了一套完整的自动化分析工具链。

4. 实验结果 (Results)

作者在 112 个基准程序（包括 VerifyPIN 和 SV-COMP 测试集）上进行了评估，结果显示：

准确性更高： 与现有最先进技术（State-of-the-art）相比，该方法不仅能检测到之前被漏掉的安全违规（Real Violations），还能有效避免由于模型不准导致的虚假违规（Bogus Violations）。
效率大幅提升： 在减少路径数量和缩短执行时间方面表现卓越。在许多情况下，优化后的算法比基准算法快了几个数量级（Orders-of-magnitude faster）。

5. 研究意义 (Significance)

这项研究为嵌入式软件的安全验证提供了一种更实用、更高效的手段。它填补了“物理硬件故障”与“软件逻辑验证”之间的鸿沟，使得开发者能够在软件开发阶段，通过自动化工具预判硬件攻击可能带来的安全风险，对于构建高可靠性的嵌入式系统具有重要的工程价值。