权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

SHF：小型：VeriFFI——经过正式验证的函数式 C 程序

基本信息

批准号：
2005545
负责人：
Andrew Appel
金额：
$ 50万
依托单位：
Princeton University
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2020
资助国家：
美国
起止时间：
2020-06-15 至 2025-05-31
项目状态：
未结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=2005545&HistoricalAwards=false
关键词：
SHF Small VeriFFI Formally Verified

项目摘要

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.

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