符号执行技术在硬件故障攻击分析中的应用与优化

1. 故障攻击与符号执行技术背景解析

在嵌入式系统和安全关键应用中，硬件故障攻击已成为一种极具威胁的攻击手段。攻击者通过电压毛刺、时钟毛刺甚至激光束照射等方式，在硬件层面注入瞬时故障，从而破坏软件的正常执行流程。这种攻击可能导致指令跳过、内存数据篡改等异常行为，进而绕过安全检查或泄露敏感信息。

传统分析方法主要依赖三类技术：

1. 硬件模拟：通过修改硬件描述语言模型注入故障
2. 软件模拟：在指令集模拟器中模拟故障效果
3. 硬件-软件协同模拟：结合前两种方法的优势

但这些方法存在明显局限：每次只能检查特定输入下的程序行为，覆盖率有限；分析过程耗时且难以扩展到复杂程序。相比之下，符号执行技术能同时覆盖所有可能的程序输入和执行路径，理论上可以实现更全面的分析。

2. 现有方法的局限性分析

当前最先进的BINSEC工具采用符号执行进行故障分析，但其存在两个关键缺陷：

2.1 故障建模不准确问题

BINSEC采用"测试反转"的故障模型，即在条件跳转指令执行前反转其条件标志位。这种模型虽然能捕捉部分故障行为，但与实际硬件故障效果存在偏差。例如在x86架构中，故障更可能导致整个跳转指令被跳过（变为nop），而非仅仅反转条件判断。

考虑以下代码片段：

if (x != 0) { n += 1; // 分支A } else { n += 2; // 分支B } assert(m != n);

BINSEC的模型只能产生两种变异：

1. 正常执行分支A或B
2. 条件反转后执行相反分支

而实际硬件故障可能导致更复杂的行为，如连续执行两个分支的代码，这种情形会被BINSEC遗漏。

2.2 路径爆炸问题加剧

符号执行固有的路径爆炸问题在故障分析场景下更加严重。每个潜在的故障注入点都会引入新的执行路径可能性。BINSEC虽然采用故障饱和技术（限制每个路径的故障注入次数），但效果有限。

实验数据显示，在分析包含33个故障目标的程序时，BINSEC需要探索206条路径，耗时远超合理范围。这种计算复杂度使得分析难以扩展到实际规模的应用程序。

3. 创新方法技术细节

3.1 基于程序转换的精确故障建模

我们提出了一种创新的程序转换方法，通过在原始程序中插入受控于符号变量的辅助分支，准确模拟指令跳过行为：

1. 故障标志引入：对每个跳转指令，添加一个布尔型符号变量bFT作为故障标志
2. 控制流扩展：在原始跳转前插入条件分支if (bFT) goto next_block
3. 语义保持：当所有bFT为false时，转换后程序行为与原始程序完全一致

以x86汇编为例：

; 原始代码 BB1: cmp eax, 0 je BB3 BB2: jmp BB4 BB3: ... BB4: ... ; 转换后代码 BB1: cmp eax, 0 cmp bFT1, 1 ; 新增故障检查 je BB2 ; 可能跳过原始跳转 je BB3 ; 原始条件跳转 BB2: cmp bFT2, 1 ; 新增故障检查 je BB3 ; 可能跳过无条件跳转 jmp BB4

这种建模方式能准确反映实际观察到的故障行为模式，特别是顺序执行本应互斥的代码路径的情况。

3.2 基于最弱前置条件的冗余路径修剪

我们提出双重修剪策略来应对路径爆炸：

3.2.1 故障计数器机制

1. 为每个执行路径维护故障计数器FC
2. 当路径中激活的故障数（bFT=true）超过预设阈值β时终止探索
3. 优先探索故障数少的路径，符合攻击者最小化攻击成本的假设

3.2.2 后缀摘要技术

关键观察：不同路径前缀可能共享相同后缀。我们通过最弱前置条件(WP)计算路径摘要：

1. 对已探索路径π，逆向计算每个位置l的wp[l]
2. 合并所有路径的wp[l]得到全局摘要WP[l]
3. 新路径执行到l时，若当前路径条件蕴含WP[l]，则跳过后续探索

wp计算示例：

# 对于路径片段： # BB1: assume(x==0) → BB3: n+=2 → assert(m!=n) wp[assert] = (m != n) wp[n+=2] = (m != n+2) # 反向替换 wp[BB1] = (m != n+2) ∧ (x==0) ∧ ¬bFT1

该方法显著减少了冗余计算，实验显示在某些案例中将探索路径数从125,195降至224。

4. 实现与评估

4.1 工具链构建

我们基于LLVM/KLEE/Z3构建了完整分析工具链：

1. 前端处理：LLVM Pass实现程序转换，插入故障标志和辅助分支
2. 符号执行：修改KLEE引擎支持故障计数和WP计算
3. 约束求解：Z3求解器处理路径条件和WP蕴含关系检查
4. 优化集成：约4,000行C++代码实现核心算法

工具工作流程：

C源码 → LLVM IR → 故障建模转换 → 符号执行 → 违规检测 ↑ ↑ 故障参数配置 路径修剪优化

4.2 实验设计

评估采用32个基准程序，包括：

• 8个VerifyPIN变体（密码验证核心）
• 24个SV-COMP程序（涵盖各类控制流模式）

对比指标：

1. 漏洞检测能力（是否发现已知违规）
2. 路径探索数量
3. 执行时间（120分钟超时）

4.3 结果分析

4.3.1 故障建模效果

在单故障注入场景下：

• BINSEC在24个非密码程序中检测到14个违规
• 我们的方法检测到18个违规，多发现4个真实漏洞

特别在trex02-2.c案例中，我们的方法发现了被BINSEC遗漏的边界条件违规，该漏洞允许通过特定故障模式绕过安全检查。

4.3.2 性能提升

冗余修剪带来显著优化：

1. 路径探索数平均减少58%（最大减少99.8%）
2. 执行时间平均缩短50%
3. 在复杂案例（如VerifyPIN_7.c）中，分析时间从481秒降至207秒

![路径探索对比图] （此处应插入路径数对比散点图，显示优化前后数据点大多位于y=x线以上）

5. 实际应用建议

5.1 工具使用指南

1. 参数配置：

./analyzer --program test.bc --fault-budget 3 --timeout 3600

• fault-budget：预期最大故障数（通常1-5）
• timeout：超时设置（秒）

2. 结果解读：

• 输出包含违规路径的输入值和故障位置
• 生成测试用例可用于重现问题

5.2 开发防护建议

基于分析结果，推荐以下加固措施：

1. 关键检查冗余：

// 原始代码 if (check) { /* 安全操作 */ } // 加固后 bool r1 = check; bool r2 = check; // 冗余执行 if (r1 && r2) { /* 安全操作 */ }

2. 故障检测计数器：

uint32_t sanity = 0xDEADBEEF; /* 敏感操作 */ assert(sanity == 0xDEADBEEF);

3. 控制流完整性检查：

// 使用哈希验证基本块序列 uint32_t cf_hash = INIT_HASH; BB1: update_hash(&cf_hash, 1); ... BB2: update_hash(&cf_hash, 2); ... assert(cf_hash == EXPECTED_HASH);

6. 局限性与未来方向

当前方法仍存在以下限制：

1. 对循环处理不够高效（需结合边界限制）
2. 浮点运算支持有限
3. 并行程序分析能力待加强

值得探索的改进方向：

1. 结合机器学习预测关键故障点
2. 支持更多故障模型（如内存位翻转）
3. 与形式化验证工具集成

在实际项目中应用时，建议先进行模块级分析，再逐步扩展到完整系统。对于大规模程序，可采用分层分析方法，先识别关键模块再深入分析。