The security of software systems is based on a chain of trust that is rooted in the hardware and ensures the security, in particular the integrity of computations run in higher layers of abstractions e.g. user code running on an operating system. Therefore, the root of trust (RoT) is a critical piece of software that is run when a device is powered up and any vulnerability in this code is compromising the security of any other code running on the device [1,2]. One of the key propertyof the RoT is to verify the integrity of software running on the device. For instance, a secure boot verified that the code operating system has not been tampered with.
The thesis will investigate the formal verification of RoT software. Compared to other software RoT have are several distinctive features that make their verification a challenge.
- A first challenge is the tight cooperation of the RoT software with security features of the hardware e.g. cryptographic keys sealed in the silicium. To be adequate, the formal model needs to provide a fine-grained model of the hardware which goes beyond the classic Instruction Set Architecture.
- Another challenge is that the software is typically written using both C code and assembly code for which semantics model are either missing or difficult to reason with.
Typically, there is a verification gap between a formal model and the running software. The thesis will tackle the challenge of verifying RoT software with the objective of narrowing the verification gap to the minimum.
To get to this objective, the thesis will investigate how to adapt the techniques coming from verified compilation [3] to automatically extract from the formal model an executable code that can be used as an in-place replacement. As RoT software cannot rely on any platform service or runtime this changes the focus compared to existing approaches to compile specification to executable code. To assess the developed techniques, the thesis will consider case-studies with features highlighting the difficulties of RoT software and showing that the proposed solution are adequate.
[1] S. Vasudevan, P. Ravi, A. Jati, S. Bhasin and A. Chattopadhyay, "Formal Verification of Secure Boot Process," 2024 Design, Automation & Test in Europe Conference & Exhibition (DATE), Valencia, Spain, 2024, pp. 1-6,
[2] A. Meza, F. Restuccia, J. Oberg, D. Rizzo and R. Kastner, "Security Verification of the OpenTitan Hardware Root of Trust," in IEEE Security & Privacy, vol. 21, no. 3, pp. 27-36
[3] Xavier Leroy. 2009. A Formally Verified Compiler Back-end. J.
Autom. Reason. 43, 4 (December 2009), 363–446.