Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Efficient Symbolic Execution of Software under Fault Attacks

Yuzhou Fang, Chenyu Zhou, Jingbo Wang, Chao Wang

TL;DR

The paper tackles the problem of safely analyzing software under fault attacks, where hardware faults can cause instruction skipping and aberrant control flow. It introduces two key innovations: a program-transformation fault-modeling technique that injects fault flags to accurately capture fault-induced behavior, and a suffix-summary–based pruning approach that uses the weakest precondition ($WP$) to cut redundant symbolic-execution paths while respect­ing a fault budget $\\beta$. The method is implemented atop LLVM, KLEE, and Z3 and evaluated on 32 benchmarks, showing that it detects many previously missed safety violations and achieves about $2.0\times$ speedup on average compared with the state of the art. This work advances scalable, software-only verification for fault-resilient embedded systems by reducing path explosion and improving fault-model fidelity, enabling more comprehensive safety guarantees under realistic fault models.

Abstract

We propose a symbolic method for analyzing the safety of software under fault attacks both accurately and efficiently. Fault attacks leverage physically injected hardware faults to break the safety of a software program. While there are existing methods for analyzing the impact of faults on software, they suffer from inaccurate fault modeling and inefficient analysis algorithms. We propose two new techniques to overcome these problems. First, we propose a fault modeling technique that leverages program transformation to add symbolic variables to the program, to accurately model the fault-induced program behavior. Second, we propose a redundancy pruning technique that leverages the weakest precondition and fault saturation to mitigate path explosion, which is a performance bottleneck of symbolic execution that is exacerbated by the fault-induced program behavior. We have implemented the method and evaluated it on a variety of benchmark programs. The experimental results show that our method significantly outperforms the state-of-the-art method. Specifically, it not only reveals many previously-missed safety violations but also reduces the running time drastically. Compared to the baseline, our optimized method is 2.0$\times$ faster on average.

Efficient Symbolic Execution of Software under Fault Attacks

TL;DR

The paper tackles the problem of safely analyzing software under fault attacks, where hardware faults can cause instruction skipping and aberrant control flow. It introduces two key innovations: a program-transformation fault-modeling technique that injects fault flags to accurately capture fault-induced behavior, and a suffix-summary–based pruning approach that uses the weakest precondition () to cut redundant symbolic-execution paths while respect­ing a fault budget . The method is implemented atop LLVM, KLEE, and Z3 and evaluated on 32 benchmarks, showing that it detects many previously missed safety violations and achieves about speedup on average compared with the state of the art. This work advances scalable, software-only verification for fault-resilient embedded systems by reducing path explosion and improving fault-model fidelity, enabling more comprehensive safety guarantees under realistic fault models.

Abstract

We propose a symbolic method for analyzing the safety of software under fault attacks both accurately and efficiently. Fault attacks leverage physically injected hardware faults to break the safety of a software program. While there are existing methods for analyzing the impact of faults on software, they suffer from inaccurate fault modeling and inefficient analysis algorithms. We propose two new techniques to overcome these problems. First, we propose a fault modeling technique that leverages program transformation to add symbolic variables to the program, to accurately model the fault-induced program behavior. Second, we propose a redundancy pruning technique that leverages the weakest precondition and fault saturation to mitigate path explosion, which is a performance bottleneck of symbolic execution that is exacerbated by the fault-induced program behavior. We have implemented the method and evaluated it on a variety of benchmark programs. The experimental results show that our method significantly outperforms the state-of-the-art method. Specifically, it not only reveals many previously-missed safety violations but also reduces the running time drastically. Compared to the baseline, our optimized method is 2.0 faster on average.

Paper Structure

This paper contains 33 sections, 1 theorem, 6 equations, 5 figures, 3 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Background
  3. The Threat Model
  4. Goal of the Adversary
  5. Fault-Induced Behavior
  6. Instruction Skipping
  7. The Example Program
  8. Fault Modeling
  9. Path Pruning
  10. Our Method
  11. The Notation
  12. Baseline Symbolic Execution
  13. Our Symbolic Execution
  14. The Fault Counter
  15. The Suffix Summary
  16. ...and 18 more sections

Key Result

theorem thmcountertheorem

Our path pruning technique is sound in the sense that the subroutine PruningCondition$(s)$ in Algorithm alg:pruning checks for a "sufficient" condition under which the current execution can be safely skipped.

Figures (5)

  • Figure 1: Example C program (left), assembly code layout with four basic blocks sequentially arranged (middle), and the control flow graph of its x86 assembly code (right): the assertion at Line 8 holds regardless of which branch is executed.
  • Figure 2: Illustrating the new $br'$ added to basic block BB in Algorithm \ref{['alg:modelfaults']}.
  • Figure 3: The transformed program $P'$ for the original program $P$ in Fig. \ref{['fig:motivating']}, where faults are modeled by the red edges.
  • Figure 4: Leveraging the suffix summary: we end the new prefix at $s$ when $s.pcon$ represents a subset of $\mathtt{WP}[s.l]$ since it will not lead to any unexplored suffix.
  • Figure 5: Scatter plots of our method with and without redundancy pruning: points above the red diagonal lines are winning cases for our optimized method.

Theorems & Definitions (1)

  • theorem thmcountertheorem: Soundness