Data Flow Analysis for Discovering Bitflip Vulnerabilities in TinyARM
Authors
Sørensen, Henrik Herbst ; Christensen, Anton
Term
4. term
Education
Publication year
2020
Abstract
Bitflips forårsaget af kosmisk stråling og andre single-event upsets kan ubemærket korrumpere processorregistre. Selvom hardware-redundans er udbredt i rum- og luftfart, er der behov for billigere softwarebaserede måder at ræsonnere om sådanne fejl. Denne afhandling udvikler en statisk dataflowanalyse, baseret på et monotont rammeværk, der kan afgøre om TinyARM-assembly er sårbar over for et enkelt bitflip i et generelt register. Vi repræsenterer programmer som kontrolflowgrafer med støtte for stifølsomhed og opbygger først en stifølsom intervalanalyse, der sporer kontrolflag under eksekvering. Derefter udvider vi analysen med en formelt defineret fejlmodel, som ved hver instruktion også overvejer den programtilstand, der ville opstå, hvis et enkelt bitflip skete umiddelbart før instruktionen. For at holde analysen praktisk ved vilkårlige registerbredder introducerer vi effektive metoder til at simulere bitflips og opdateringer af kontrolflag uden bruteforce. Resultatet er et værktøj, der også indeholder en TinyARM-fortolker og kan levere forskellige outputformater. Vi illustrerer analysen på repræsentative kodeeksempler, herunder et scenarie beslægtet med en PAM-autentificeringskontrol, samt på softwarebaserede beskyttelsesskemaer fra tidligere arbejde, og viser hvilke problemer analysen kan og ikke kan finde. Vi diskuterer også begrænsninger (herunder at vi ikke kan bevise fuld lydhed, da vi kun argumenterer for monotonitet af nogle transfunktioner) og skitserer veje til større præcision og en bredere fejlmodel.
Bit flips caused by cosmic radiation and other single-event upsets can silently corrupt processor registers. While hardware redundancy is common in aerospace systems, there is a need for affordable software-based ways to reason about such faults. This thesis develops a static data flow analysis, grounded in a monotone framework, to determine whether TinyARM assembly programs are vulnerable to a single bit flip in a general-purpose register. We represent programs as control-flow graphs that support path sensitivity and first build a path-sensitive interval analysis that tracks control-flag states during execution. We then extend it with a formally defined fault model that, at every instruction, also considers the program state that would arise if a single bit flip occurred just before that instruction. To keep the analysis practical for arbitrary register widths, we introduce efficient ways to simulate bit flips and control-flag updates without brute force. The result is a tool that includes a TinyARM interpreter and multiple output formats. We illustrate the analysis on representative code snippets, including a scenario akin to a PAM authentication check, and on software-only protection schemes proposed in prior work, showing the kinds of problems the analysis can and cannot detect. We also discuss limitations (including that we cannot fully prove soundness, as we only argue monotonicity for some transfer functions) and outline directions for improving precision and broadening the fault model.
[This summary has been generated with the help of AI directly from the project (PDF)]
Documents