Software Resillience of Critical Embedded Systems: Evaluating Software through Symbolic Execution and Low-Level Runtime Fault Injection
Authors
Thorsen, Åsmundur Alexander Kjærbæk ; Bækgaard, Peter
Term
4. term
Education
Publication year
2026
Submitted on
2026-05-28
Abstract
This thesis examines two ways to test how embedded software withstands faults. The first is source-level symbolic execution using MiniMC. The second is fault injection through a custom ARM Thumb‑2 interpreter. To support this, we built a simple model language (TriviLang) and a compiler (TriviC) that can generate ARM Thumb‑2 assembly; we also used Whiley. The compiler can optionally insert automatic hardening into the programs under test, such as a statement counter and variable duplication. We created three TriviLang programs of increasing complexity for evaluation. The results show that source-level symbolic execution can pinpoint faulty locations in small programs, but without heuristics or path pruning it suffers from path explosion on more complex programs. In contrast, fault injection with our interpreter offers fine-grained control over when and where faults are injected and remains practical on larger programs because it does not suffer from path explosion.
Denne afhandling undersøger to måder at teste, hvor robust indlejret software er over for fejl. Den første er symbolsk eksekvering på kildeniveau med MiniMC. Den anden er fejlinjektion via en specialudviklet ARM Thumb‑2‑fortolker. For at understøtte arbejdet byggede vi et simpelt modelsprog (TriviLang) og en compiler (TriviC), der kan generere ARM Thumb‑2‑assembly; vi brugte også Whiley. Compileren kan valgfrit indsætte automatiske robusthedstiltag i de testede programmer, som for eksempel en sætningstæller og duplikering af variabler. Vi udviklede tre TriviLang‑programmer med stigende kompleksitet til evalueringen. Resultaterne viser, at symbolsk eksekvering på kildeniveau kan pege på fejlsteder i små programmer, men uden heuristikker eller beskæring af stier opstår der en eksplosion i antallet af mulige eksekveringsstier i mere komplekse programmer. Til gengæld giver fejlinjektion med vores fortolker finmasket kontrol over, hvornår og hvor der injiceres fejl, og kan bruges på større programmer uden problemet med stieksplosion.
[This abstract has been rewritten with the help of AI based on the project's original abstract]
Keywords