pith. sign in

arxiv: 2503.15825 · v2 · submitted 2025-03-20 · 💻 cs.SE · cs.PL

Efficient Symbolic Execution of Software under Fault Attacks

Yuzhou Fang , Chenyu Zhou , Jingbo Wang , Chao Wang This is my paper

Pith reviewed 2026-05-22 23:52 UTC · model grok-4.3

classification 💻 cs.SE cs.PL
keywords fault attackssymbolic executionprogram transformationsafety analysisembedded softwarepath pruning
0
0 comments X

The pith

A program transformation that adds symbolic variables for faults plus pruning in symbolic execution detects missed safety violations under fault attacks and runs orders of magnitude faster.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proposes modeling hardware fault attacks on embedded software by automatically transforming the program to insert symbolic variables that represent possible fault effects. This transformed program can be analyzed by standard tools, but the authors supply a specialized symbolic execution engine that applies two pruning steps to control the added path complexity. The central claim is that this combination produces more accurate results than prior fault analysis methods, catching real violations that earlier techniques missed while eliminating spurious reports that do not correspond to actual attacks. A sympathetic reader would care because fault attacks are a documented practical threat to safety-critical embedded devices, and better analysis would let developers check whether their code remains secure when hardware is physically tampered with.

Core claim

The central claim is that automated program transformation can add symbolic variables to the original program so that the new behaviors induced by injected faults are modeled accurately, with the advantages that the modeled behavior matches what attackers exploit and that the resulting program can be fed to any downstream analysis algorithm. This is paired with an optimized symbolic execution procedure that uses two pruning techniques to limit path explosion on the transformed program. Experiments on benchmark programs show the method detects previously missed safety violations, avoids bogus violations, and runs orders of magnitude faster than the baseline algorithm.

What carries the argument

Automated program transformation that inserts symbolic variables to represent fault effects, together with two pruning techniques inside symbolic execution to reduce path explosion on the transformed program.

If this is right

  • The method detects safety violations that prior techniques missed.
  • It avoids reporting bogus violations that do not arise in actual attacks.
  • Analysis completes orders of magnitude faster than the baseline symbolic execution algorithm.
  • The transformed program can be analyzed by any existing fault analysis algorithm without modification.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same transformation idea could be used to model other hardware faults such as radiation-induced bit flips if equivalent symbolic rules are written.
  • Developers could generate concrete fault-injection test vectors from the symbolic paths to guide physical experiments.
  • The pruning techniques might reduce complexity when symbolic execution is applied to other sources of nondeterminism such as concurrent interleavings.

Load-bearing premise

The automated program transformation accurately captures the new program behavior induced by injected faults in a way that matches what real attackers exploit in practice.

What would settle it

A physical fault-injection campaign on the same benchmark programs in which the safety violations observed in hardware differ from the violations reported by the symbolic analysis would show that the modeling step does not match real attacks.

Figures

Figures reproduced from arXiv: 2503.15825 by Chao Wang, Chenyu Zhou, Jingbo Wang, Yuzhou Fang.

Figure 1
Figure 1. Figure 1: Example C program (left), assembly code layout with four basic blocks [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Illustrating the new br′ added to basic block BB in Algorithm 2. Regardless of whether the branch br is conditional (e.g., je target) or un￾conditional (e.g., jmp next), it must have BB, target and next. Here, BB is the basic block where br belongs to, target is the basic block where br jumps to, and next is the basic block immediately following br in the original program P. Here, the word “next” refers to… view at source ↗
Figure 3
Figure 3. Figure 3: The transformed program P ′ for the original program P in [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Leveraging the suffix summary: we end the new prefix at [PITH_FULL_IMAGE:figures/full_fig_p012_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Scatter plots of our method with and without redundancy pruning: points [PITH_FULL_IMAGE:figures/full_fig_p018_5.png] view at source ↗
read the original abstract

We propose a symbolic execution method for analyzing the safety of software under fault attacks both accurately and efficiently. Fault attacks leverage physically injected hardware faults in an embedded system to break the safety of a software program. While there are existing methods for analyzing the impact of maliciously injected hardware faults on the embedded software, they suffer from inaccurate fault modeling and inefficient fault analysis. To overcome these limitations, we propose two novel techniques. First, we propose a new fault modeling technique that leverages automated program transformation to add symbolic variables to the original program, to accurately model the new program behavior induced by the injected faults. This new fault modeling approach has two advantages over existing techniques: (a) the fault-induced program behavior is closely related to what attackers exploit in practice and (b) the automatically transformed program may be analyzed by any downstream fault analysis algorithm. Second, we propose an efficient symbolic execution algorithm that is designed specifically for conducting fault analysis on the transformed program. It leverages two pruning techniques to mitigate path explosion. We have implemented the proposed method and evaluated it on a variety of benchmark programs. The experimental results show that our method significantly outperforms the state-of-the-art techniques. Compared to the current state-of-the-art, it is able to detect previously-missed safety violations and at the same time avoid bogus violations. Furthermore, compared to the baseline algorithm, our optimized symbolic execution algorithm can be orders-of-magnitude faster.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper proposes a symbolic execution method for analyzing software safety under fault attacks. It introduces an automated program transformation technique that adds symbolic variables to model fault-induced behaviors, with claimed advantages of closer relation to real attacker exploits and compatibility with any downstream analysis algorithm. It also presents an optimized symbolic execution algorithm using two pruning techniques to mitigate path explosion. Evaluation on benchmark programs is said to show detection of previously-missed safety violations while avoiding bogus ones, plus orders-of-magnitude speedups over the baseline algorithm and state-of-the-art techniques.

Significance. If the central claims on accurate fault modeling and sound pruning hold with proper validation, the work would advance fault-attack analysis for embedded systems by improving both accuracy (missed violations without false positives) and efficiency. The program-transformation approach enabling reuse of existing analysis tools is a notable strength. However, the absence of hardware ground truth or explicit verification details for the modeling and pruning steps limits the assessed significance.

major comments (2)
  1. [Abstract / Evaluation] Abstract and evaluation section: the claims of detecting previously-missed violations, avoiding bogus violations, and orders-of-magnitude speedups rest on unevaluated assumptions. No details are supplied on benchmark selection criteria, how ground-truth violations were established (e.g., via manual inspection, hardware experiments, or oracle), or verification that the two pruning techniques preserve all relevant behaviors without eliminating valid fault-induced paths.
  2. [Abstract] Abstract, advantage (a): the assertion that the automated program transformation produces fault-induced behavior 'closely related to what attackers exploit in practice' is load-bearing for the accuracy claims (missed violations without bogus ones). No direct validation against physical fault injection (voltage glitches, EM pulses, precise-cycle bit flips) is described; without hardware ground truth, both the 'missed' and 'no bogus' results could be artifacts of the symbolic modeling rather than evidence of improved analysis.
minor comments (1)
  1. [Abstract] The abstract refers to 'a variety of benchmark programs' without naming them or providing characteristics (size, domain, fault models used); this should be expanded in the evaluation section for reproducibility.

Simulated Author's Rebuttal

2 responses · 1 unresolved

We thank the referee for the constructive review and for identifying areas where the evaluation methodology and validation of claims require additional clarification. We respond to each major comment below and indicate where revisions will be made.

read point-by-point responses

  1. Referee: [Abstract / Evaluation] Abstract and evaluation section: the claims of detecting previously-missed violations, avoiding bogus violations, and orders-of-magnitude speedups rest on unevaluated assumptions. No details are supplied on benchmark selection criteria, how ground-truth violations were established (e.g., via manual inspection, hardware experiments, or oracle), or verification that the two pruning techniques preserve all relevant behaviors without eliminating valid fault-induced paths.

    Authors: We agree that the evaluation section would benefit from explicit details on these points. Benchmarks were selected from standard suites in the fault-analysis literature (e.g., cryptographic primitives and control-flow examples from prior works). Ground truth for violations was established via manual inspection of the small programs, cross-checked against results from existing tools. The pruning techniques are accompanied by a soundness argument in Section 4 showing that only infeasible paths under the symbolic fault model are eliminated. We will revise the evaluation section to include these details on selection criteria, ground-truth process, and pruning verification. revision: yes

  2. Referee: [Abstract] Abstract, advantage (a): the assertion that the automated program transformation produces fault-induced behavior 'closely related to what attackers exploit in practice' is load-bearing for the accuracy claims (missed violations without bogus ones). No direct validation against physical fault injection (voltage glitches, EM pulses, precise-cycle bit flips) is described; without hardware ground truth, both the 'missed' and 'no bogus' results could be artifacts of the symbolic modeling rather than evidence of improved analysis.

    Authors: The modeling claim rests on the transformation directly encoding instruction- and register-level faults drawn from established attacker models in the literature, rather than on abstract approximations used by prior techniques. This enables detection of violations missed by coarser models while avoiding spurious ones through precise symbolic tracking. We acknowledge the absence of physical hardware experiments; the current work focuses on the symbolic approach and its compatibility with existing analyzers. We will add a clarifying discussion of the modeling basis and note the lack of direct hardware validation as a limitation of the present study. revision: partial

standing simulated objections not resolved
  • Direct hardware ground truth validation via physical fault injection experiments.

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper proposes a fault modeling technique via automated program transformation that adds symbolic variables, plus an optimized symbolic execution algorithm with two pruning techniques. No equations, fitted parameters, or self-citations appear in the provided abstract or description that reduce any claimed prediction or result to an input by construction. The advantages (a) and (b), the detection of missed violations, avoidance of bogus ones, and reported speedups are presented as direct consequences of the new transformation and pruning steps evaluated on benchmarks, without any self-definitional loops or load-bearing self-citations. This is the normal case of a self-contained proposal against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The approach rests on the domain assumption that symbolic variables inserted by transformation faithfully represent attacker-exploitable fault effects and that the two pruning rules preserve all paths that could reveal safety violations; no free parameters or invented entities are mentioned.

axioms (2)
  • domain assumption Symbolic execution on the transformed program correctly models all behaviors induced by the modeled faults.
    Stated as advantage (a) of the new modeling technique in the abstract.
  • domain assumption The two pruning techniques eliminate only paths irrelevant to safety-violation detection.
    Required for the efficiency claim without loss of accuracy.

pith-pipeline@v0.9.0 · 5779 in / 1191 out tokens · 30237 ms · 2026-05-22T23:52:03.884935+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

41 extracted references · 41 canonical work pages

  1. [1]

    Bar-El, H., Choukri, H., Naccache, D., Tunstall, M., Whelan, C.: The sorcerer’s apprentice guide to fault attacks. Proc. IEEE94(2), 370–382 (2006)

    work page 2006

  2. [2]

    IEEE Transactions on Information Forensics and Security (TIFS) (2023)

    Beigizad, A.A., Soleimany, H., Zarei, S., Ramzanipour, H.: Linked Fault Analysis. IEEE Transactions on Information Forensics and Security (TIFS) (2023)

    work page 2023

  3. [3]

    In: International conference on Tools and Algorithms for the Con- struction and Analysis of Systems (TACAS) (2024)

    Beyer, D.: State of the art in Software Verification and Witness Validation: SV- COMP 2024. In: International conference on Tools and Algorithms for the Con- struction and Analysis of Systems (TACAS) (2024)

    work page 2024

  4. [4]

    Nonlinear Dynamics (2019)

    Bonny, T., Nasir, Q.: Clock Glitch Fault Injection Attack on an FPGA-based Non- Autonomous Chaotic Oscillator. Nonlinear Dynamics (2019)

    work page 2019

  5. [5]

    In: USENIX Symposium on Operating Systems Design and Implementation (OSDI) (2008)

    Cadar, C., Dunbar, D., Engler, D.: KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In: USENIX Symposium on Operating Systems Design and Implementation (OSDI) (2008)

    work page 2008

  6. [6]

    FDTC (2005)

    Choukri, H., Tunstall, M.: Round reduction using faults. FDTC (2005)

    work page 2005

  7. [7]

    In: International Haifa Verification Conference

    Chu, D., Jaffar, J.: A framework to synergize partial order reduction with state interpolation. In: International Haifa Verification Conference. pp. 171–187 (2014)

    work page 2014

  8. [8]

    In: International conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2008)

    De Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2008)

    work page 2008

  9. [9]

    In: Work- shop on Fault Diagnosis and Tolerance in Cryptography (2012)

    Dehbaoui, A., Dutertre, J.M., Robisson, B., Tria, A.: Electromagnetic Transient Faults Injection on a Hardware and a Software Implementations of AES. In: Work- shop on Fault Diagnosis and Tolerance in Cryptography (2012)

    work page 2012

  10. [10]

    Prentice Hall, NJ (1976)

    Dijkstra, E.: A Discipline of Programming. Prentice Hall, NJ (1976)

    work page 1976

  11. [11]

    In: European Symposium on Programming (ESOP) (2023)

    Ducousso, S., Bardin, S., Potet, M.L.: Adversarial Reachability for Program-level Security Analysis. In: European Symposium on Programming (ESOP) (2023)

    work page 2023

  12. [12]

    In: Computer Safety, Relia- bility, and Security (2016)

    Dureuil, L., Petiot, G., Potet, M.L., Le, T.H., Crohen, A., de Choudens, P.: FISSC: A Fault Injection and Simulation Secure Collection. In: Computer Safety, Relia- bility, and Security (2016)

    work page 2016

  13. [13]

    Girol, G., Lacombe, G., Bardin, S.: Quantitative Robustness for Vulnerability As- sessment (2024)

    work page 2024

  14. [14]

    Given-Wilson, T., Jafri, N., Legay, A.: Combined software and hardware fault injection vulnerability detection. Innov. Syst. Softw. Eng.16(2), 101–120 (2020)

    work page 2020

  15. [15]

    Godefroid, P., Levin, M.Y., Molnar, D.A.: SAGE: whitebox fuzzing for security testing. Commun. ACM55(3), 40–44 (2012)

    work page 2012

  16. [16]

    Cryptography (2021)

    Grycel,J.T.,Schaumont,P.:SimpliFI:HardwareSimulationofEmbeddedSoftware Fault Attacks. Cryptography (2021)

    work page 2021

  17. [17]

    In: ACM Proc

    Guo, S., Kusano, M., Wang, C., Yang, Z., Gupta, A.: Assertion guided symbolic execution of multithreaded programs. In: ACM Proc. ESEC/FSE (2015)

    work page 2015

  18. [18]

    In: ACM SIGSOFT Symposium on Foundations of Software Engineering

    Jaffar, J., Murali, V., Navas, J.A.: Boosting concolic testing via interpolation. In: ACM SIGSOFT Symposium on Foundations of Software Engineering. pp. 48–58 (2013)

    work page 2013

  19. [19]

    In: Proc

    Kuznetsov, V., Kinder, J., Bucur, S., Candea, G.: Efficient state merging in sym- bolic execution. In: Proc. ACM PLDI (2012)

    work page 2012

  20. [20]

    Journal of Cryptographic Engineering (2024)

    Lacombe, G., Féliot, D., Boespflug, E., Potet, M.: Combining static analysis and dynamic symbolic execution in a toolchain to detect fault injection vulnerabilities. Journal of Cryptographic Engineering (2024)

    work page 2024

  21. [21]

    In: 14th International Conference on Electronics, Computers and Artificial Intelligence, ECAI 2022, Ploiesti, Romania, June 30 - July 1, 2022 (2022)

    Lancia, J.: Detecting fault injection vulnerabilities in binaries with symbolic exe- cution. In: 14th International Conference on Electronics, Computers and Artificial Intelligence, ECAI 2022, Ploiesti, Romania, June 30 - July 1, 2022 (2022)

    work page 2022

  22. [22]

    In: Beckert, B

    Larsson, D., Hähnle, R.: Symbolic fault injection. In: Beckert, B. (ed.) Proceedings of 4th International Verification Workshop in connection with CADE-21, Bremen, Germany, July 15-16, 2007. CEUR Workshop Proceedings, vol. 259 (2007)

    work page 2007

  23. [23]

    In: IEEE International Symposium on Code Genera- tion and Optimization (2004)

    Lattner, C., Adve, V.: LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In: IEEE International Symposium on Code Genera- tion and Optimization (2004)

    work page 2004

  24. [24]

    In: Madsen, J., Coskun, A.K

    Le, H.M., Herdt, V., Große, D., Drechsler, R.: Resilience evaluation via symbolic fault injection on intermediate code. In: Madsen, J., Coskun, A.K. (eds.) 2018 De- sign,Automation&TestinEuropeConference&Exhibition,DATE2018,Dresden, Germany, March 19-23, 2018. pp. 845–850 (2018)

    work page 2018

  25. [25]

    IACR Transactions on Cryptographic Hardware and Embedded Systems (2024)

    Liu, Z., Shanmugam, D., Schaumont, P.: Fault Detective Explainable to a Fault, from the Design Layout to the Software. IACR Transactions on Cryptographic Hardware and Embedded Systems (2024)

    work page 2024

  26. [26]

    In: Interna- tional Conference on Computer Aided Verification

    McMillan, K.L.: Lazy annotation for program testing and verification. In: Interna- tional Conference on Computer Aided Verification. pp. 104–118 (2010)

    work page 2010

  27. [27]

    Moro, N., Heydemann, K., Encrenaz, E., Robisson, B.: Formal verification of a software countermeasure against instruction skip attacks. J. Cryptogr. Eng.4(3), 145–156 (2014)

    work page 2014

  28. [28]

    In: IEEE Symposium on Security and Privacy (S&P) (2020)

    Murdock, K., Oswald, D., Garcia, F.D., Van Bulck, J., Gruss, D., Piessens, F.: Plundervolt: Software-based Fault Injection Attacks against Intel SGX. In: IEEE Symposium on Security and Privacy (S&P) (2020)

    work page 2020

  29. [29]

    IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (2019)

    Mutlu, O., Kim, J.S.: Rowhammer: A retrospective. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (2019)

    work page 2019

  30. [30]

    Ning, B., Liu, Q.: Modeling and Efficiency Analysis of Clock Glitch Fault Injection Attack.In:AsianHardwareOrientedSecurityandTrustSymposium(AsianHOST) (2018)

    work page 2018

  31. [31]

    IEEE Trans

    Pattabiraman, K., Nakka, N., Kalbarczyk, Z.T., Iyer, R.K.: Symplfied: Symbolic program-level fault injection and error detection framework. IEEE Trans. Com- puters 62(11), 2292–2307 (2013)

    work page 2013

  32. [32]

    In: Stark, K., Timany, A., Blazy, S., Tabareau, N

    Pesin, B., Boulmé, S., Monniaux, D., Potet, M.: Formally verified hardening of C programs against hardware fault injection. In: Stark, K., Timany, A., Blazy, S., Tabareau, N. (eds.) Proceedings of the 14th ACM SIGPLAN International Con- ference on Certified Programs and Proofs, CPP 2025, Denver, CO, USA, January 20-21, 2025. pp. 140–155 (2025)

    work page 2025

  33. [33]

    In: Proc

    Sellami, Y., Girol, G., Recoules, F., Couroussé, D., Bardin, S.: Inference of Robust Reachability Constraints. In: Proc. ACM POPL (2024)

    work page 2024

  34. [34]

    ACM SIGSOFT Software Engineering Notes (2005)

    Sen, K., Marinov, D., Agha, G.: CUTE: A Concolic Unit Testing Engine for C. ACM SIGSOFT Software Engineering Notes (2005)

    work page 2005

  35. [35]

    In: Crypto- graphic Hardware and Embedded Systems (CHES) (2003)

    Skorobogatov, S.P., Anderson, R.J.: Optical Fault Induction Attacks. In: Crypto- graphic Hardware and Embedded Systems (CHES) (2003)

    work page 2003

  36. [36]

    arXiv preprint arXiv:2307.00561 (2023)

    Tan, H., Gao, P., Chen, T., Song, F., Wu, Z.: SAT-based Formal Fault-Resistance Verification of Cryptographic Circuits. arXiv preprint arXiv:2307.00561 (2023)

    work page arXiv 2023

  37. [37]

    In: Usenix Security (2017)

    Tang, A., Sethumadhavan, S., Stolfo, S.: CLKSCREW: Exposing the perils of {Security-Oblivious} energy management. In: Usenix Security (2017)

    work page 2017

  38. [38]

    In: Workshop on Fault Detection and Tolerance in Cryptography (FDTC) (2022)

    Tollec, S., Asavoae, M., Couroussé, D., Heydemann, K., Jan, M.: Exploration of Fault Effects on Formal RISC-V Microarchitecture Models. In: Workshop on Fault Detection and Tolerance in Cryptography (FDTC) (2022)

    work page 2022

  39. [39]

    In: Formal Methods in Computer-Aided Design (FMCAD) (2023)

    Tollec, S., Asavoae, M., Couroussé, D., Heydemann, K., Jan, M.:µArchiFI: Formal Modeling and Verification Strategies for Microarchitetural Fault Injections. In: Formal Methods in Computer-Aided Design (FMCAD) (2023)

    work page 2023

  40. [40]

    IEEE Transactions on Software Engineering (TSE) (2017)

    Yi, Q., Yang, Z., Guo, S., Wang, C., Liu, J., Zhao, C.: Eliminating path redun- dancy via postconditioned symbolic execution. IEEE Transactions on Software Engineering (TSE) (2017)

    work page 2017

  41. [41]

    Journal of Hardware and Systems Security (2018)

    Yuce, B., Schaumont, P., Witteman, M.: Fault Attacks on Secure Embedded Soft- ware: Threats, Design, and Evaluation. Journal of Hardware and Systems Security (2018)

    work page 2018