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
Pages
80
Abstract
This thesis investigates two ways to test how embedded software copes with faults (resilience testing). The first is source-code-level symbolic execution using MiniMC, which explores many possible execution paths by reasoning about inputs symbolically. The second is fault injection via a custom ARM Thumb-2 interpreter, which simulates the processor and lets us inject errors at precise times and code locations. To support these experiments, we built a small model language (TriviLang) and a compiler (TriviC) that can emit ARM Thumb-2 assembly and Whiley code. TriviC can also optionally insert automatic hardenings—simple defensive measures such as statement counters and variable duplication—into the programs under test. We created three TriviLang programs of increasing complexity for evaluation. Our results show that source-level symbolic execution can pinpoint faulty locations in small programs, but without heuristics or path pruning to limit the number of explored paths, larger programs suffer from path explosion. In contrast, fault injections with our interpreter provided fine-grained control over when and where faults were injected, and worked even on larger programs without the path-explosion problem.
Specialet undersøger to måder at teste, hvordan indlejret software klarer fejl (resiliens-test). Den første er symbolsk eksekvering på kildetekstniveau med MiniMC, som afprøver mange mulige kørselsforløb ved at ræsonnere symbolsk om input. Den anden er fejl-injektion via en specialbygget ARM Thumb-2-fortolker, som simulerer processoren og gør det muligt at injicere fejl på præcise tidspunkter og steder i koden. For at muliggøre dette byggede vi et lille modelsprog (TriviLang) og en kompilator (TriviC), der kan generere ARM Thumb-2 assembly og Whiley-kode. TriviC kan også valgfrit indsætte automatisk hærdning—enkle beskyttelsestiltag som sætningstællere (statement counters) og variabelduplikering—i de testede programmer. Vi udviklede tre TriviLang-programmer med stigende kompleksitet til evalueringen. Resultaterne viser, at symbolsk eksekvering på kildetekstniveau kan pege fejls placeringer ud i små programmer, men uden heuristikker eller sti-beskæring til at begrænse antallet af stier opstår der sti-eksplosion i større programmer. Omvendt gav fejl-injektion med vores fortolker finmasket kontrol over injektionstidspunkt og -sted og fungerede også på større programmer uden problemet med sti-eksplosion.
[This apstract has been rewritten with the help of AI based on the project's original abstract]
Keywords