Spoq: Scaling Machine-Checkable Systems Verification in Coq
Spoq: Scaling Machine-Checkable Systems Verification in Coq
复制标题
DOI：
--
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
Xupeng Li;Xuheng Li;Wei Qiang;Ronghui Gu;Jason Nieh
中科院分区：
文献类型：
--
作者：
Xupeng Li;Xuheng Li;Wei Qiang;Ronghui Gu;Jason Nieh
系统软件通常是庞大而复杂的，导致许多漏洞可能被利用来危及系统的安全性。形式化验证为创建无缺陷软件提供了一个潜在的解决方案，但其采用的一个关键障碍仍然是证明成本。我们提出了Spoq，一个高度自动化的验证框架，在Coq中构建机器可检查的证明，以更少的证明成本。Spoq引入了一种新颖的程序结构重构技术，利用LLVM将C代码转换为Coq，支持完整的C语义，包括C宏，内联汇编和编译器指令，因此源代码不再需要手动修改才能进行验证。Spoq利用分层证明策略，引入新的Coq策略和转换规则，自动生成层规范和精化证明，简化并发系统软件的验证。Spoq还支持轻松集成手动编写的层规范和细化证明。我们使用Spoq来验证多处理器KVM虚拟机管理程序的实现。使用Spoq进行验证所需的证明工作量比手动编写的规范和证明少70%，以验证旧的实现。此外，使用Spoq的证明适用于直接编译和执行的未修改的实现。
System software is often large and complex, resulting in many vulnerabilities that can potentially be exploited to compromise the security of a system. Formal verification offers a potential solution to creating bug-free software, but a key impediment to its adoption remains proof cost. We present Spoq, a highly automated verification framework to construct machine-checkable proofs in Coq for system software with much less proof cost. Spoq introduces a novel program structure reconstruction technique to leverage LLVM to translate C code into Coq, supporting full C semantics, including C macros, inline assembly, and compiler directives, so that source code no longer has to be manually modified to be verified. Spoq leverages a layering proof strategy and introduces novel Coq tactics and transformation rules to automatically generate layer specifications and refinement proofs to simplify verification of concurrent system software. Spoq also supports easy integration of manually written layer specifications and refinement proofs. We use Spoq to verify a multiprocessor KVM hypervisor implementation. Verification using Spoq required 70% less proof effort than the manually written specifications and proofs to verify an older implementation. Furthermore, the proofs using Spoq hold for the unmodified implementation that is directly compiled and executed.