SHF: Small: VeriFFI -- Formally Verified Functional+C programs

形式演绎验证--使用证明助手等工具对程序正确性进行机器检查的证明--是构建非常高保证的安全组件的有效方法，例如操作系统内核和密码通信原语。用于程序验证的现有逻辑、工具和方法要么适用于低级语言(如C)，要么适用于高级函数式语言。但现实世界的系统是用多种语言混合编写的：用于操作系统(OS)内核和加密原语等组件的低级命令式语言；用于大多数应用程序、OS管理代码、加密协议和高级语言的运行时系统的高级语言。该项目开发了与低级程序链接的高级语言程序的形式化验证方法和工具，事实证明是正确的，符合统一的规范，跨越了边界，没有空白。高级语言是CoQ证明助手中的函数式编程语言，使用Coq的逻辑进行验证，并使用CertiCoq编译器进行编译(可以证明是正确的)。低级语言是C语言，使用经过验证的软件工具链(VST)进行验证，并使用经过CompCert验证的C编译器进行编译(可以证明是正确的)。新的经过验证的外部函数接口(VeriFFI)利用认证Coq的工具链和VST/CompCert之间的协同作用来实现这种统一验证。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Formal deductive verification -- machine-checked proofs of program correctness using tools such as proof assistants -- is an effective way of building very high assurance secure components, such as operating-system kernels and cryptographic communications primitives. Existing logics, tools, and methods for program verification apply either to low-level languages (such as C) or high-level functional languages. But real-world systems are programmed in a mix of languages: low-level imperative languages for components such as operating-system (OS) kernels and cryptographic primitives; high-level languages for most applications, for OS-management code, for cryptographic protocols, and for the runtime systems of the high-level languages. This project develops methods and tools for formal verification of high-level language programs linked with low-level programs, proved correct to a unified specification that crosses the boundary with no gaps. The high-level language is the functional programming language inside the Coq proof assistant, verified using Coq’s logic, and compiled (provably correctly) with the CertiCoq compiler. The low-level language is C, verified using the Verified Software Toolchain (VST), and compiled (provably correctly) using the CompCert verified C compiler. The new Verified Foreign Function Interface (VeriFFI) exploits synergies between CertiCoq’s toolchain and VST/CompCert to enable such unified verifications.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.