Modelling Java Card Applications With Defensive Measures In UPPAAL
Translated title
Moddelering af Java Card Applikationer Med Beskyttelsesmetoder I UPPAAL
Authors
Vinther, Anders Kaastrup ; Jørgensen, Jakob
Term
4. term
Education
Publication year
2015
Submitted on
2015-06-01
Pages
73
Abstract
This thesis investigates how single event upsets (bit flips) that can cause arbitrary jumps in the program counter affect the control flow of Java Card applications, and whether in-program software defenses can detect such events at runtime. Building on published operational semantics, we model a specific, industry-used defensive strategy in UPPAAL (including SMC) and develop a toolchain comprising a program generator and a model parser that translates programs into UPPAAL-compatible XML models. The attacker model assumes no ability to craft a precise path through the program but allows choosing when the single bit flip occurs. We present the modeling of control flow, attack timing and success criteria, and the queries used to evaluate the defense. The work demonstrates that UPPAAL can be a strong ally for program analysis of Java Card applications with defensive measures; detailed quantitative findings are beyond what is available in this excerpt.
Denne afhandling undersøger, hvordan enkeltstående bitflip-hændelser (single event upsets), som kan få programtælleren til at springe vilkårligt, påvirker kontrolflowet i Java Card-applikationer, og om indbyggede softwarebaserede beskyttelsesmekanismer kan opdage sådanne hændelser under kørsel. Med udgangspunkt i publicerede operationelle semantikker modellerer vi et udvalgt, industrielt anvendt forsvarsprincip i UPPAAL (herunder SMC) og udvikler en værktøjskæde bestående af en programgenerator og en modelparser, der oversætter programmer til UPPAAL-kompatible XML-modeller. Modellen antager en angriber, der ikke kan styre en specifik vej gennem programmet, men kan bestemme tidspunktet for en enkelt bitflip. Vi beskriver modelleringen af kontrolflow, angrebets timing og succesbetingelser samt de forespørgsler, der bruges til at evaluere forsvaret. Arbejdet demonstrerer, at UPPAAL kan være et stærkt værktøj til programanalyse af Java Card-applikationer med defensive tiltag; detaljerede kvantitative resultater ligger ud over, hvad der fremgår af dette uddrag.
[This apstract has been generated with the help of AI directly from the project full text]
Keywords