论文标题
验证生成分离内核
Verification of a Generative Separation Kernel
论文作者
论文摘要
我们对MUEN分离内核的功能正确性进行了正式验证。 Muen是利用硬件虚拟化支持的现代分离内核等级的代表，并且本质上是生成性的，因为它们为每种系统配置生成了专门的内核。这些特征对现有验证技术构成了重大挑战。我们提出了一个称为条件参数改进的验证框架，该框架使我们能够正式推理生成系统。我们使用此框架来执行基于条件改进的MUEN内核发生器的正确性证明。我们对几种系统配置的分析表明，我们的技术有效地产生了正确性的机械化证明，还可以确定可能损害分离属性的问题。
We present a formal verification of the functional correctness of the Muen Separation Kernel. Muen is representative of the class of modern separation kernels that leverage hardware virtualization support, and are generative in nature in that they generate a specialized kernel for each system configuration. These features pose substantial challenges to existing verification techniques. We propose a verification framework called conditional parametric refinement which allows us to formally reason about generative systems. We use this framework to carry out a conditional refinement-based proof of correctness of the Muen kernel generator. Our analysis of several system configurations shows that our technique is effective in producing mechanized proofs of correctness, and also in identifying issues that may compromise the separation property.
