Value-set Analysis for RISC-V: Detecting Bitflip Vulnerabilities
Authors
Christiansen, Ida Thoft ; Ernstsen, Lena Said
Term
4. term
Education
Publication year
2023
Submitted on
2023-06-09
Pages
70
Abstract
Bitflip-angreb - hvor en enkelt 0/1-bit i data bliver vendt - er en reel sikkerhedsrisiko, som tidligere er vist for PAM-mekanismen til autentifikation. Dette speciale præsenterer et proof-of-concept til at opdage bitflip-sårbarheder i RISC-V-programmer ved hjælp af value-set-analyse, en statisk teknik der vurderer, hvilke værdier variabler og registre kan få. Vi formaliserer et RISC-V-sprog og opstiller fejlsmodeller, der beskriver forskellige typer bitflip-angreb. Oven på dette definerer vi en value-set-analyse inden for det monotone rammeværk (en matematisk ramme for statisk analyse): vi specificerer et analysedomæne, der er et komplet gitter (en matematisk struktur), og giver monotone overførselsfunktioner for alle instruktioner. Analysen er implementeret i værktøjet BitflipperVild. I samlingen FISSC detekterer BitflipperVild alle register-relevante bitflip-sårbarheder. Med værktøjet kan vi desuden vise, at visse bitflips kan gøre det muligt for en angriber at nå et privilegeret punkt uden autentifikation.
Bitflip attacks - where a single 0/1 bit in data is flipped - are a practical security risk, as shown in prior work on the PAM mechanism for authentication. This thesis presents a proof-of-concept for detecting bitflip vulnerabilities in RISC-V programs using value-set analysis, a static technique that estimates which values variables and registers may take. We formalize a RISC-V language and define fault models that capture different kinds of bitflip attacks. Building on this, we design a value-set analysis within the monotone framework (a mathematical setup for static analysis): we specify an analysis domain that is a complete lattice (a mathematical structure) and provide monotone transfer functions for all instructions. We implement the analysis in a tool called BitflipperVild. In the FISSC collection, BitflipperVild detects all register-relevant bitflip vulnerabilities. Using the tool, we also show that certain bitflips could let an attacker reach a privileged point without authentication.
[This summary has been rewritten with the help of AI based on the project's original abstract]
Keywords
Documents