一个生成分离核的验证
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
