Our formal proof efforts focus on the security monitor implementation. The security monitor is implemented in Rust. There are minor parts that require assembly, e.g., context switches. Read more about our approach in the paper.
Above Figure presents the finite state machine (FSM) implemented by the security monitor. Non-confidential Flow (orange) implements part of the security monitor that responds to hypervisor requests. Confidential Flow (blue) implements part of the security monitor that response to confidential VM requests. Heavy context switch, i.e., switch between security domains, occures during "stealing" and "returning" a confidential hart from/to a confidential VM.
To speed up the implementation, we used OpenSBI as firmware. OpenSBI runs together with the security monitor in the M-mode. The ultimate goal is to deprivilege it or re-implement it in Rust and then formally verify. Our principle is to rely on as minimal Rust dependencies as possible.
We will interatively add our proofs to the repository. Check the verification folder to learn more.
This is an active research project, without warranties of any kind.
@inproceedings{ozga2023riscvtee,
title={Towards a Formally Verified Security Monitor for VM-based Confidential Computing},
author={Ozga, Wojciech and Hunt, Guerney D. H. and Le, Michael V. and Palmer, Elaine R. and Shinnar, Avraham},
booktitle = {Proceedings of the 12th International Workshop on Hardware and Architectural Support for Security and Privacy},
series = {HASP2023},
year={2023}
}