SAFEBOX: A Verified Microkernel Based on Spatial-Temporal Isolation
Fan Zhang, Weining Su, Tianfang Wang, Xiaopeng Wang · 2015
The correctness of kernel is the key to the safety-critical embedded application, and only by formal verification it can prove the kernel does not exist some defects or meet certain attributes. In this paper, we introduce SAFEBOX, a microkernel based on spatial-temporal isolation, give the formal description of SAFEBOX, and use theorem proverb Isabelle/HOL to verify the functional and non-functional properties of SAFEBOX.