Formally Verifying Security Properties for OpenTitan Boot Code with UPPAAL
Authors
Bøgedal, Tobias Worm ; Pedersen, Magnus Winkel ; Møller, Bjarke Hilmer
Term
4. term
Education
Publication year
2021
Abstract
Efterhånden som mere information lagres og behandles digitalt, stiger behovet for sikre computersystemer. Fordi angribere ofte er opfindsomme, skal sikkerhed tænkes ind fra starten i sikkerhedskritiske systemer. I dette arbejde undersøger vi OpenTitan, et system under udvikling, ved at se nærmere på dets opstartsproces. Vi anvender formel verifikation – matematiske metoder til at bevise egenskaber – og bruger modeltjek med værktøjet UPPAAL (version 4.1.24) til at modellere den første opstarts-fase. Modellen danner grundlag for at kontrollere en række sikkerhedsmål, som vi tidligere har formuleret. Med UPPAALs indbyggede verifikator kan vi fuldt ud verificere 5 ud af 8 udvalgte mål, delvist verificere 2, og vi kan ikke verificere 1 mål. Den manglende verifikation skyldes delvist, at den nuværende dokumentation for OpenTitan-projektet ikke er tilstrækkeligt detaljeret til at muliggøre en kvalificeret vurdering. Ved at opstille en model af OpenTitan kan vi dermed gennemføre co-verifikation af systemets opstartsmekanismer med overvejende succes.
As more information is stored and processed digitally, the need for secure computer systems grows. Because attackers are creative, safety-critical systems must be designed with security in mind from the start. In this work, we examine OpenTitan, a system under development, by focusing on its boot process. We use formal verification—mathematical methods to prove properties—and apply model checking with the UPPAAL tool (version 4.1.24) to model the first boot stage. This model forms the basis for checking a set of security goals that we previously defined. Using UPPAAL’s built-in verifier, we can fully verify 5 of 8 selected goals, partially verify 2, and we cannot verify 1 goal. The inability to verify the last goal is due in part to the current state of the OpenTitan project documentation, which lacks sufficient detail for a well-founded verification. By building a model of OpenTitan, we enable co-verification of its boot mechanisms with predominantly successful results.
[This summary has been rewritten with the help of AI based on the project's original abstract]
Documents