Advanced Development of Certified OS Kernels
Zhong Shao · 2015
Abstract : The PI and his team at Yale have successfully developed (1) a clean - slate CertiKOS hypervisor kernel that runs on multicore platforms and supports Linux and ROS applications; (2) a new certified programming methodologies and tools that can verify contextual correctness, liveness, and security properties in a unified setting; (3) a fully verified single - core CertiKOS in Coq; (4) new semantics and logics for reasoning about information flow control with declassification, resource analysis, and fine-grained concurrent programs; and (5) new proof assistant language VeriML and Coq Ltac libraries.