Efficient Symbolic Execution of Software under Fault Attacks

Technical Summary: Efficient Symbolic Execution of Software under Fault Attacks

1. Problem Statement

The paper addresses the security challenge of hardware fault injection attacks on embedded systems. In these attacks, adversaries use physical mechanisms (e.g., voltage glitching, laser beams, or electromagnetic waves) to induce hardware faults in a CPU. These faults can cause software to behave abnormally, such as skipping critical security checks (e.g., an if statement guarding sensitive data).

Existing analysis methods suffer from two primary limitations:

• Inaccurate Fault Modeling: Current state-of-the-art techniques (like "test inversion") model faults by flipping CPU flags. This does not reflect real-world attacks, where faults more commonly cause instruction skipping (turning a jump instruction into a nop). Consequently, existing methods either miss real vulnerabilities or report "bogus" violations that cannot occur in practice.
• Inefficient Fault Analysis: Symbolic execution, the standard for exploring program paths, faces an extreme path explosion problem when faults are introduced. Because a fault can occur at almost any instruction, the number of possible execution paths grows astronomically, making exhaustive analysis computationally infeasible.

2. Methodology

The authors propose a two-pronged approach to improve both the accuracy and efficiency of fault analysis through a specialized symbolic execution framework.

A. Accurate Fault Modeling (Program Transformation)
Instead of modeling faults during the analysis phase, the authors implement fault modeling as a standalone automated program transformation at the LLVM Intermediate Representation (IR) level.

• Instruction Skipping Model: For every branching instruction (conditional or unconditional) in the original program, the tool automatically inserts an auxiliary "fault flag" variable ($b_{FT}$).
• Control Flow Augmentation: The transformation adds a new branch: if the fault flag is active, the program skips the original jump and proceeds to the next sequential instruction. This faithfully simulates the "instruction skipping" observed in empirical studies.
• Soundness: The authors prove that this transformation is both sound and complete, meaning it captures all real violations without introducing fake ones.

B. Efficient Fault Analysis (Redundancy Pruning)
To combat path explosion, the authors introduce a symbolic execution algorithm that utilizes two pruning techniques:

• Fault Saturation: The algorithm tracks a "fault counter." If the number of activated faults in a path exceeds a predefined fault budget ($\beta$), the path is immediately terminated.
• Path Summary-based Pruning: This is the core innovation for efficiency. The authors observe that many fault-induced paths share common "suffixes" (the remaining part of a program after a certain point).
  • The tool computes a Weakest Precondition (WP) for explored suffixes and stores them as a "path summary."
  • When the engine encounters a new path (prefix) that leads to a previously explored location, it uses an SMT solver (Z3) to check if the current path condition is a subset of the existing summary. If it is, the engine skips the redundant suffix, as it cannot lead to any new safety violations.

3. Key Contributions

1. A novel fault modeling technique based on compiler-level program transformation that accurately simulates instruction skipping.
2. An optimized symbolic execution algorithm specifically designed for fault analysis, integrating fault saturation and a new redundancy pruning mechanism.
3. A practical implementation leveraging the LLVM compiler, the KLEE symbolic execution engine, and the Z3 SMT solver.
4. A formal proof of the soundness and completeness of the proposed fault modeling.

4. Experimental Results

The method was evaluated against the state-of-the-art (BINSEC) using 112 benchmark programs (VerifyPIN and SV-COMP suites).

• Improved Accuracy: The proposed method detected 14 more real safety violations than the existing state-of-the-art. Crucially, it avoided "bogus" violations (false positives) that previous methods reported due to inaccurate flag-inversion modeling.
• Superior Efficiency:
  • The optimized algorithm explored significantly fewer paths than the baseline.
  • In terms of execution time, the method was orders of magnitude faster than the baseline in many cases.
  • While there is some overhead from SMT solver calls for pruning, the reduction in the total number of paths explored leads to a massive net gain in performance for complex programs.

5. Significance

This work provides a highly effective tool for developers and security researchers to verify the robustness of embedded software against physical hardware attacks. By bridging the gap between low-level hardware fault behavior and high-level software symbolic analysis, the authors have created a method that is both more realistic (detecting actual vulnerabilities) and more scalable (handling the complexity of real-world software) than previous approaches.