Document Open Access Logo

Efficient Symbolic Execution of Software Under Fault Attacks

Authors Yuzhou Fang , Chenyu Zhou , Jingbo Wang , Chao Wang

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2026.4.pdf
  • Filesize: 1.36 MB
  • 25 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • Software and its engineering → Software testing and debugging
Keywords
  • Symbolic Execution
  • Safety Verification
  • Fault Attack
  • Embedded Software

Metrics

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, which is the main performance bottleneck of symbolic execution in general and, in this particular application, is exacerbated by the additional fault-induced program behavior. 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. Specifically, our method not only drastically reduces the overall running time of symbolic execution but also retains its error detection capabilities. 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.

Cite As Get BibTex

Yuzhou Fang, Chenyu Zhou, Jingbo Wang, and Chao Wang. Efficient Symbolic Execution of Software Under Fault Attacks. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 4:1-4:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ECOOP.2026.4

Author Details

Yuzhou Fang
  • University of Southern California, Los Angeles, CA, USA
Chenyu Zhou
  • University of Southern California, Los Angeles, CA, USA
Jingbo Wang
  • Purdue University, West Lafayette, IN, USA
Chao Wang
  • University of Southern California, Los Angeles, CA, USA

Funding

This work was supported in part by the NSF grant CCF-2220345.

Supplementary Materials

References

  1. Hagai Bar-El, Hamid Choukri, David Naccache, Michael Tunstall, and Claire Whelan. The sorcerer’s apprentice guide to fault attacks. Proc. IEEE, 94(2):370-382, 2006. URL: https://doi.org/10.1109/JPROC.2005.862424.
  2. Ali Asghar Beigizad, Hadi Soleimany, Sara Zarei, and Hamed Ramzanipour. Linked fault analysis. IEEE Trans. Inf. Forensics Secur., 19:632-645, 2024. URL: https://doi.org/10.1109/TIFS.2023.3327658.
  3. Dirk Beyer. State of the art in software verification and witness validation: SV-COMP 2024. In Bernd Finkbeiner and Laura Kovács, editors, Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III, Lecture Notes in Computer Science, pages 299-329. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57256-2_15.
  4. Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In Richard Draves and Robbert van Renesse, editors, 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings, pages 209-224. USENIX Association, 2008. URL: http://www.usenix.org/events/osdi08/tech/full_papers/cadar/cadar.pdf.
  5. Hamid Choukri and Michael Tunstall. Round reduction using faults. Workshop on Fault Diagnosis and Tolerance in Cryptography (FDTC), 2005. Google Scholar
  6. Leonardo Mendonça de Moura and Nikolaj S. Bjørner. Z3: an efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, Lecture Notes in Computer Science, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  7. Amine Dehbaoui, Jean-Max Dutertre, Bruno Robisson, and Assia Tria. Electromagnetic transient faults injection on a hardware and a software implementations of AES. In Guido Bertoni and Benedikt Gierlichs, editors, 2012 Workshop on Fault Diagnosis and Tolerance in Cryptography, Leuven, Belgium, September 9, 2012, pages 7-15. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/FDTC.2012.15.
  8. Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976. URL: https://www.worldcat.org/oclc/01958445.
  9. Soline Ducousso, Sébastien Bardin, and Marie-Laure Potet. Adversarial reachability for program-level security analysis. In Thomas Wies, editor, Programming Languages and Systems - 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, Lecture Notes in Computer Science, pages 59-89. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30044-8_3.
  10. Louis Dureuil, Guillaume Petiot, Marie-Laure Potet, Thanh-Ha Le, Aude Crohen, and Philippe de Choudens. FISSC: A fault injection and simulation secure collection. In Amund Skavhaug, Jérémie Guiochet, and Friedemann Bitsch, editors, Computer Safety, Reliability, and Security - 35th International Conference, SAFECOMP 2016, Trondheim, Norway, September 21-23, 2016, Proceedings, Lecture Notes in Computer Science, pages 3-11. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-45477-1_1.
  11. Guillaume Girol, Guilhem Lacombe, and Sébastien Bardin. Quantitative robustness for vulnerability assessment. Proc. ACM Program. Lang., 8(PLDI):741-765, 2024. URL: https://doi.org/10.1145/3656407.
  12. Thomas Given-Wilson, Nisrine Jafri, and Axel Legay. Combined software and hardware fault injection vulnerability detection. Innov. Syst. Softw. Eng., 16(2):101-120, 2020. URL: https://doi.org/10.1007/S11334-020-00364-5.
  13. Patrice Godefroid, Michael Y. Levin, and David A. Molnar. SAGE: whitebox fuzzing for security testing. Commun. ACM, 55(3):40-44, 2012. URL: https://doi.org/10.1145/2093548.2093564.
  14. Jacob T. Grycel and Patrick Schaumont. Simplifi: Hardware simulation of embedded software fault attacks. Cryptogr., 5(2):15, 2021. URL: https://doi.org/10.3390/CRYPTOGRAPHY5020015.
  15. Shengjian Guo, Markus Kusano, and Chao Wang. Conc-iSE: incremental symbolic execution of concurrent software. In David Lo, Sven Apel, and Sarfraz Khurshid, editors, Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016, Singapore, September 3-7, 2016, pages 531-542. ACM, 2016. URL: https://doi.org/10.1145/2970276.2970332.
  16. Shengjian Guo, Markus Kusano, Chao Wang, Zijiang Yang, and Aarti Gupta. Assertion guided symbolic execution of multithreaded programs. In Elisabetta Di Nitto, Mark Harman, and Patrick Heymans, editors, Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2015, Bergamo, Italy, August 30 - September 4, 2015, pages 854-865. ACM, 2015. URL: https://doi.org/10.1145/2786805.2786841.
  17. Shengjian Guo, Meng Wu, and Chao Wang. Symbolic execution of programmable logic controller code. In Eric Bodden, Wilhelm Schäfer, Arie van Deursen, and Andrea Zisman, editors, Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2017, Paderborn, Germany, September 4-8, 2017, pages 326-336. ACM, 2017. URL: https://doi.org/10.1145/3106237.3106245.
  18. Shengjian Guo, Meng Wu, and Chao Wang. Adversarial symbolic execution for detecting concurrency-related cache timing leaks. In Gary T. Leavens, Alessandro Garcia, and Corina S. Pasareanu, editors, Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/SIGSOFT FSE 2018, Lake Buena Vista, FL, USA, November 04-09, 2018, pages 377-388. ACM, 2018. URL: https://doi.org/10.1145/3236024.3236028.
  19. Volodymyr Kuznetsov, Johannes Kinder, Stefan Bucur, and George Candea. Efficient state merging in symbolic execution. In Jan Vitek, Haibo Lin, and Frank Tip, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '12, Beijing, China - June 11 - 16, 2012, pages 193-204. ACM, 2012. URL: https://doi.org/10.1145/2254064.2254088.
  20. Guilhem Lacombe, David Féliot, Etienne Boespflug, and Marie-Laure Potet. Combining static analysis and dynamic symbolic execution in a toolchain to detect fault injection vulnerabilities. J. Cryptogr. Eng., 14(1):147-164, 2024. URL: https://doi.org/10.1007/S13389-023-00310-8.
  21. Julien Lancia. Detecting fault injection vulnerabilities in binaries with symbolic execution. In 14th International Conference on Electronics, Computers and Artificial Intelligence, ECAI 2022, Ploiesti, Romania, June 30 - July 1, 2022, pages 1-8. IEEE, 2022. URL: https://doi.org/10.1109/ECAI54874.2022.9847500.
  22. Daniel Larsson and Reiner Hähnle. Symbolic fault injection. In Bernhard Beckert, editor, Proceedings of 4th International Verification Workshop in connection with CADE-21, Bremen, Germany, July 15-16, 2007, CEUR Workshop Proceedings. CEUR-WS.org, 2007. URL: https://ceur-ws.org/Vol-259/paper09.pdf.
  23. Chris Lattner and Vikram S. Adve. LLVM: A compilation framework for lifelong program analysis & transformation. In 2nd IEEE / ACM International Symposium on Code Generation and Optimization (CGO 2004), 20-24 March 2004, San Jose, CA, USA, pages 75-88. IEEE Computer Society, 2004. URL: https://doi.org/10.1109/CGO.2004.1281665.
  24. Hoang M. Le, Vladimir Herdt, Daniel Große, and Rolf Drechsler. Resilience evaluation via symbolic fault injection on intermediate code. In Jan Madsen and Ayse K. Coskun, editors, 2018 Design, Automation & Test in Europe Conference & Exhibition, DATE 2018, Dresden, Germany, March 19-23, 2018, pages 845-850. IEEE, 2018. URL: https://doi.org/10.23919/DATE.2018.8342123.
  25. Zhenyuan Liu, Dillibabu Shanmugam, and Patrick Schaumont. Faultdetective explainable to a fault, from the design layout to the software. IACR Trans. Cryptogr. Hardw. Embed. Syst., 2024(4):610-632, 2024. URL: https://doi.org/10.46586/TCHES.V2024.I4.610-632.
  26. Nicolas Moro, Karine Heydemann, Emmanuelle Encrenaz, and Bruno Robisson. Formal verification of a software countermeasure against instruction skip attacks. J. Cryptogr. Eng., 4(3):145-156, 2014. URL: https://doi.org/10.1007/S13389-014-0077-7.
  27. Kit Murdock, David F. Oswald, Flavio D. Garcia, Jo Van Bulck, Daniel Gruss, and Frank Piessens. Plundervolt: Software-based fault injection attacks against intel SGX. In 2020 IEEE Symposium on Security and Privacy, SP 2020, San Francisco, CA, USA, May 18-21, 2020, pages 1466-1482. IEEE, 2020. URL: https://doi.org/10.1109/SP40000.2020.00057.
  28. Onur Mutlu and Jeremie S. Kim. Rowhammer: A retrospective. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 39(8):1555-1571, 2020. URL: https://doi.org/10.1109/TCAD.2019.2915318.
  29. Bo Ning and Qiang Liu. Modeling and efficiency analysis of clock glitch fault injection attack. In Asian Hardware Oriented Security and Trust Symposium, AsianHOST 2018, Hong Kong, China, December 17-18, 2018, pages 13-18. IEEE, 2018. URL: https://doi.org/10.1109/ASIANHOST.2018.8607175.
  30. Colin O'Flynn. BAM BAM!! on reliability of EMFI for in-situ automotive ECU attacks. IACR Cryptol. ePrint Arch., 2020:937, 2020. URL: https://eprint.iacr.org/2020/937.
  31. Karthik Pattabiraman, Nithin Nakka, Zbigniew T. Kalbarczyk, and Ravishankar K. Iyer. SymPLFIED: Symbolic program-level fault injection and error detection framework. IEEE Trans. Computers, 62(11):2292-2307, 2013. URL: https://doi.org/10.1109/TC.2012.219.
  32. Basile Pesin, Sylvain Boulmé, David Monniaux, and Marie-Laure Potet. Formally verified hardening of C programs against hardware fault injection. In Kathrin Stark, Amin Timany, Sandrine Blazy, and Nicolas Tabareau, editors, Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2025, Denver, CO, USA, January 20-21, 2025, pages 140-155. ACM, 2025. URL: https://doi.org/10.1145/3703595.3705880.
  33. Yanis Sellami, Guillaume Girol, Frédéric Recoules, Damien Couroussé, and Sébastien Bardin. Inference of robust reachability constraints. Proc. ACM Program. Lang., 8(POPL):2731-2760, 2024. URL: https://doi.org/10.1145/3632933.
  34. Koushik Sen, Darko Marinov, and Gul Agha. CUTE: a concolic unit testing engine for C. In Michel Wermelinger and Harald C. Gall, editors, Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2005, Lisbon, Portugal, September 5-9, 2005, pages 263-272. ACM, 2005. URL: https://doi.org/10.1145/1081706.1081750.
  35. Sergei P. Skorobogatov and Ross J. Anderson. Optical fault induction attacks. In Burton S. Kaliski Jr., Çetin Kaya Koç, and Christof Paar, editors, Cryptographic Hardware and Embedded Systems - CHES 2002, 4th International Workshop, Redwood Shores, CA, USA, August 13-15, 2002, Revised Papers, Lecture Notes in Computer Science, pages 2-12. Springer, 2002. URL: https://doi.org/10.1007/3-540-36400-5_2.
  36. Huiyu Tan, Pengfei Gao, Fu Song, Taolue Chen, and Zhilin Wu. Sat-based formal verification of fault injection countermeasures for cryptographic circuits. IACR Trans. Cryptogr. Hardw. Embed. Syst., 2024(4):1-39, 2024. URL: https://doi.org/10.46586/TCHES.V2024.I4.1-39.
  37. Adrian Tang, Simha Sethumadhavan, and Salvatore J. Stolfo. CLKSCREW: exposing the perils of security-oblivious energy management. In Engin Kirda and Thomas Ristenpart, editors, 26th USENIX Security Symposium, USENIX Security 2017, Vancouver, BC, Canada, August 16-18, 2017, pages 1057-1074. USENIX Association, 2017. URL: https://www.usenix.org/conference/usenixsecurity17/technical-sessions/presentation/tang.
  38. Simon Tollec, Mihail Asavoae, Damien Couroussé, Karine Heydemann, and Mathieu Jan. Exploration of fault effects on formal RISC-V microarchitecture models. In Workshop on Fault Detection and Tolerance in Cryptography, FDTC 2022, Virtual Event / Italy, September 16, 2022, pages 73-83. IEEE, 2022. URL: https://doi.org/10.1109/FDTC57191.2022.00017.
  39. Simon Tollec, Mihail Asavoae, Damien Couroussé, Karine Heydemann, and Mathieu Jan. μarchifi: Formal modeling and verification strategies for microarchitectural fault injections. In Alexander Nadel and Kristin Yvonne Rozier, editors, Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, IA, USA, October 24-27, 2023, pages 101-109. IEEE, 2023. URL: https://doi.org/10.34727/2023/ISBN.978-3-85448-060-0_18.
  40. Qiuping Yi, Zijiang Yang, Shengjian Guo, Chao Wang, Jian Liu, and Chen Zhao. Postconditioned symbolic execution. In 8th IEEE International Conference on Software Testing, Verification and Validation, ICST 2015, Graz, Austria, April 13-17, 2015, pages 1-10. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/ICST.2015.7102601.
  41. Qiuping Yi, Zijiang Yang, Shengjian Guo, Chao Wang, Jian Liu, and Chen Zhao. Eliminating path redundancy via postconditioned symbolic execution. IEEE Trans. Software Eng., 44(1):25-43, 2018. URL: https://doi.org/10.1109/TSE.2017.2659751.
  42. Bilgiday Yuce, Patrick Schaumont, and Marc Witteman. Fault attacks on secure embedded software: Threats, design, and evaluation. J. Hardw. Syst. Secur., 2(2):111-130, 2018. URL: https://doi.org/10.1007/S41635-018-0038-1.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact