Formally Verifying Security Properties for OpenTitan Boot Code with UPPAAL

Bøgedal, Tobias Worm ; Pedersen, Magnus Winkel ; Møller, Bjarke Hilmer

4. term

Software, Master

2021

2021-06-16

The demand for secure computer systems increases as more information is stored and processed digitally. The ways a computer system can be attacked is limited only by the attackers' imagination. Therefore, safety-critical computer systems must be developed with this in mind. A system currently under development is the OpenTitan system. To follow the development and investigate the security mechanisms at play in the booting process of OpenTitan, we apply methods for formal verification. We do this with the hope of verifying relevant security principles of the system. To perform this task, we use the model checking tool UPPAAL version 4.1.24 to model the first boot stage of OpenTitan. The model is the foundation for the verification of certain security goals that we have developed previously. With the help of UPPAAL's built-in verification tool, we can successfully verify five out of eight selected goals. We further consider two of the remaining three security goals partially verified. The last security goal is not verified. This is partly due to the current state of the OpenTitan project documentation, which does not provide sufficient detail to make a qualified verification of the goal. Thus by building a model representing the OpenTitan system, we can do co-verification of the OpenTitan system with predominantly successful results.

Download
View record in AAU Student Projects