Quantitative Analysis of Single Event Upsets in ARM
Translated title
Kvantitativ Analyse af Single Event Upsets i ARM
Authors
Terndrup, Morten Korsholm ; Andersen, Thomas Rafn
Term
4. term
Education
Publication year
2018
Pages
71
Abstract
Single Event Upsets (SEU)—enkeltbits-flip i registre eller hukommelse forårsaget af naturfænomener eller fremkaldt af angreb som rowhammer—kan ændre programadfærd i sikkerheds- og datasikkerhedskritiske systemer. Denne afhandling præsenterer en formel, statisk programanalyse for et ARM-baseret assemblersprog, der eksplicit modellerer fejl på bestemte bitpositioner og registre. Analysen retter sig mod brugervalgte kritiske programpunkter: data- og kontrolflowanalyse udtrækker en relevant programslice, symbolsk eksekvering beregner sti-betingelser frem til det kritiske punkt, og en særlig sikkerhedsassertion kontrolleres med Z3 SMT-solveren for at afgøre, hvilke fejl der kan krænke sikkerheds- og sikkerhedsmæssige egenskaber. For at håndtere de mange måder SEU’er kan påvirke eksekveringen, definerer vi fejlækvivalensklasser baseret på om betingelsesflag kan afvige under forskellige fejl, og giver en algoritme der afgør ækvivalens ved at bruge de indsamlede sti-betingelser. Vi koder desuden programsemantik og fejladfærd som timed automata og anvender UPPAAL SMC til statistisk modeltjek for at estimere risikoen for sårbare fejl. Tilgangen demonstreres på en simpel alarmcontroller og en hærdet variant med instruktionsduplikering, og vi diskuterer, hvordan analysen kan udvides ud over de løkkefri programmer, der antages i den indledende formalisering.
Single Event Upsets (SEUs)—single-bit flips in registers or memory caused by natural phenomena or induced by attacks such as rowhammer—can alter program behavior in safety- and security-critical systems. This thesis introduces a formal, static program analysis for an ARM-based assembly language that explicitly models faults at particular bit positions and registers. The analysis targets user-selected critical program points: data and control-flow analysis extracts a relevant slice, symbolic execution computes path conditions to the critical point, and a special security assertion is checked with the Z3 SMT solver to determine which faults can violate safety/security properties. To reason about the many ways SEUs can affect execution, we define fault equivalence classes based on whether conditional flags may differ under different faults, and give an algorithm that decides equivalence using the collected path conditions. We further encode program semantics and fault behavior as timed automata and use UPPAAL SMC for statistical model checking to estimate the risk associated with vulnerable faults. The approach is demonstrated on a simple alarm controller and a hardened variant using instruction duplication, and we discuss how to extend the analysis beyond the loop-free programs assumed in the initial formalization.
[This summary has been generated with the help of AI directly from the project (PDF)]
Keywords
Documents