A master thesis from Aalborg University
Value-set Analysis for RISC-V: Detecting Bitflip Vulnerabilities
Author(s)
Term
4. term
Education
Publication year
2023
Submitted on
2023-06-09
Pages
70 pages
Abstract
Bitflip attacks have been shown to be a real-life security issue, as demonstrated on the PAM mechanism. Thus, this report concerns a proof of concept for detecting bitflip vulnerabilities in RISC-V programs using a value-set analysis. This is achieved by formalizing the RISC-V language and creating fault models describing different bitflip attacks. Based on this formalization, a value-set analysis is defined that utilizes the monotone framework. In the analysis, we have defined a domain, which has been shown to be a complete lattice, as well as monotone transfer functions for all instructions. The defined analysis is implemented as a tool called BitflipperVild. BitflipperVild is shown to be able to detect all register-relevant bitflip vulnerabilities in the programs found in the collection FISSC. Thus, we are able to use our tool to show that some possible bitflips can result in an attacker reaching a privileged point without authentication.
Bitflip attacks have been shown to be a real-life security issue, as demonstrated on the PAM mechanism. Thus, this report concerns a proof of concept for detecting bitflip vulnerabilities in RISC-V programs using a value-set analysis. This is achieved by formalizing the RISC-V language and creating fault models describing different bitflip attacks. Based on this formalization, a value-set analysis is defined that utilizes the monotone framework. In the analysis, we have defined a domain, which has been shown to be a complete lattice, as well as monotone transfer functions for all instructions. The defined analysis is implemented as a tool called BitflipperVild. BitflipperVild is shown to be able to detect all register-relevant bitflip vulnerabilities in the programs found in the collection FISSC. Thus, we are able to use our tool to show that some possible bitflips can result in an attacker reaching a privileged point without authentication.
Keywords
Documents
Colophon: This page is part of the AAU Student Projects portal, which is run by Aalborg University. Here, you can find and download publicly available bachelor's theses and master's projects from across the university dating from 2008 onwards. Student projects from before 2008 are available in printed form at Aalborg University Library.
If you have any questions about AAU Student Projects or the research registration, dissemination and analysis at Aalborg University, please feel free to contact the VBN team. You can also find more information in the AAU Student Projects FAQs.