COGENT: Certified Compilation for a Functional Systems Language

COGENT: Certified Compilation for a Functional Systems Language
复制标题

COGENT：功能系统语言的认证编译

DOI：
--
复制
发表时间：
2016
期刊：
arXiv.org
影响因子：
--
通讯作者：
Gerwin Klein
Gerwin Klein
中科院分区：
--
文献类型：
--
作者：
Liam O'Connor;C. Rizkallah;Zilin Chen;Sidney Amani;Japheth Lim;Yutaka Nagashima;Thomas Sewell;A. Hixon;G. Keller;Toby C. Murray;Gerwin Klein

文献摘要

被引文献

相似文献

我们为 COGENT 系统语言提供了一个自认证编译器。 COGENT 是一种受限制的、多态的、高阶的、纯函数式语言，具有线性类型，不需要可信运行时或垃圾收集器。它编译为高效的 C 代码，旨在与现有的 C 函数进行互操作。该语言适用于具有最少共享的分层系统代码，例如文件系统或网络协议控制代码。对于类型良好的 COGENT 程序，编译器会生成 C 代码、其语义在 Isabelle/HOL 中的高级浅嵌入，以及 C 代码正确实现此嵌入的证明。目的是让证明工程师高效且等式地推理现实世界系统代码的完整语义，同时保留 C 的互操作性和精益性。我们描述了编译器的形式验证阶段，其中包括自动形式细化计算、从命令式更新语义到由线性类型系统形式证明的函数值语义的转换，以及许多标准编译器阶段，例如类型检查和 单态化。编译器证书是一系列语言级元证明和每个程序翻译验证阶段，在 Isabelle/HOL 中组合成一个连贯的顶级定理。
We present a self-certifying compiler for the COGENT systems language. COGENT is a restricted, polymorphic, higher-order, and purely functional language with linear types and without the need for a trusted runtime or garbage collector. It compiles to efficient C code that is designed to interoperate with existing C functions. The language is suited for layered systems code with minimal sharing such as file systems or network protocol control code. For a well-typed COGENT program, the compiler produces C code, a high-level shallow embedding of its semantics in Isabelle/HOL, and a proof that the C code correctly implements this embedding. The aim is for proof engineers to reason about the full semantics of real-world systems code productively and equationally, while retaining the interoperability and leanness of C. We describe the formal verification stages of the compiler, which include automated formal refinement calculi, a switch from imperative update semantics to functional value semantics formally justified by the linear type system, and a number of standard compiler phases such as type checking and monomorphisation. The compiler certificate is a series of language-level meta proofs and per-program translation validation phases, combined into one coherent top-level theorem in Isabelle/HOL.