Formally Verifying the Correctness and Safety of OpenTitan Boot Code using CBMC
Translated title
Formel Verifikation af Korrektheden og Sikkerheden af OpenTitan Boot Code ved brug af CBMC
Authors
Søndergaard, Jacob Gosch ; Jensen, Kristoffer Skagbæk
Term
4. term
Education
Publication year
2021
Submitted on
2021-06-18
Pages
124
Abstract
Software that many systems rely on must be correct and secure. OpenTitan is an open-source hardware project that provides a silicon root of trust—the small, trusted component that ensures only authorized code runs when a device starts. Based on an in-depth analysis of OpenTitan, we, together with SV106f21, implemented C code that mirrors OpenTitan's initial boot stage. We used CBMC, a bounded model checker for C programs, to automatically check this boot code. We verified many safety aspects and confirmed that the code satisfies all 11 defined security properties, most of which come from our earlier work. To make the approach clear, we also provide an overview of how CBMC works and a structured, step-by-step method for verifying C code with CBMC. To represent the hardware environment, we used CBMC's nondeterminism to model inputs and behaviors the software cannot control. Finally, we examined how the boot code behaves under modeled hardware attacks. Our analysis shows that the current implementation is vulnerable to attacks on flash, ROM, and the OpenTitan Big Number Accelerator, which can lead to executing malicious code or system crashes.
Software, som mange systemer bygger på, skal være korrekt og sikker. OpenTitan er et open source-hardwareprojekt, der leverer en silicon root of trust—den lille, betroede komponent, som skal sikre, at kun godkendt kode kører ved opstart. På baggrund af en dybdegående analyse af OpenTitan udviklede vi, sammen med SV106f21, C-kode, der afspejler OpenTitans indledende opstartsfase. Vi brugte CBMC, en begrænset modeltjekker til C-programmer, til automatisk at kontrollere denne boot-kode. Vi verificerede mange sikkerhedsaspekter og bekræftede, at koden opfylder alle 11 definerede sikkerhedsegenskaber, hvoraf de fleste stammer fra vores tidligere arbejde. For at gøre fremgangsmåden klar giver vi også et overblik over, hvordan CBMC virker, og en struktureret, trin-for-trin metode til at verificere C-kode med CBMC. For at repræsentere hardwaremiljøet brugte vi CBMC's nondeterminisme til at modellere input og adfærd, som softwaren ikke kan styre. Til sidst undersøgte vi, hvordan boot-koden opfører sig under modellerede hardwareangreb. Vores analyse viser, at den aktuelle implementering er sårbar over for angreb på flash, ROM og OpenTitans Big Number Accelerator, hvilket kan føre til kørsel af ondsindet kode eller systemnedbrud.
[This apstract has been rewritten with the help of AI based on the project's original abstract]