Assessing Bit Flip Attacks and Countermeasures

Thomsen, Kristian Mikkel ; Nduru, Christoffer Kinyanjui Duun

4. term

Software, Master

2016

2016-05-31

64

Angreb mod smartkort bliver stadig mere avancerede, og det er derfor vigtigt at vurdere, hvor robust software er. Selvom der findes mange modforanstaltninger, er det svært at vælge de rette til et bestemt program. Denne rapport undersøger, hvordan fejlangreb, der forårsager bit flips—små ændringer fra 0 til 1 eller omvendt—kan påvirke Java-programmer. Vi bygger videre på tidligere arbejde, der definerede formel semantik (præcise regler for programadfærd) og fejlmodeller (strukturerede beskrivelser af mulige fejl) for et lille Java Card-inspireret sprog. Dette arbejde udvides med et værktøj, der automatisk konverterer Java bytecode til modeller for UPPAAL, et verificeringsværktøj. Med UPPAAL verificerer vi sikkerhedsegenskaber i forhold til de formaliserede fejlmodeller.

Attacks on smart cards are becoming more sophisticated, making it important to assess how well software can withstand them. Although many countermeasures exist, it is hard to decide which ones fit a specific program. This report examines how fault attacks that cause bit flips—small changes from 0 to 1 or vice versa—can affect Java programs. We build on earlier work that defined formal semantics (precise rules for program behavior) and fault models (structured descriptions of possible faults) for a small language inspired by Java Card. We extend this work by creating a tool that automatically converts Java bytecode into models for UPPAAL, a verification tool. Using UPPAAL, we check security properties of programs against the formalized fault models.

[This abstract was generated with the help of AI]

java ; smart card ; uppaal ; fault injection ; modelling ; bit flip

Download
View record in AAU Student Projects