一句话：提出 Low*：将良行为 C 子集浅嵌入 F*，以类型保证内存安全并借助 F* 验证，经抽取编译到 C。
低层安全关键代码常用 C，性能高但缺少内存安全与功能正确性保证；经验证的高级语言又多依赖 GC 和隐式堆分配，难以高效。本文提出 Low*，将小型、顺序、行为良好的 C 子集浅嵌入依赖类型语言 F*。Low* 采用 CompCert 风格结构化内存模型，无 GC 或隐式堆分配，由类型系统保证内存安全；程序员可用 F* 规范，结合 SMT 与手工证明验证功能正确性。抽取时规范与证明被擦除，代码可预测地翻译为 C。作者实现 Low* 到 C 后端并证明翻译保持语义与抗侧信道性；在约 28,000 行密码算法与工具上完成验证，性能与未验证 C 密码库相当。
We present Low*, a language for low-level programming and verification, and its application to high-assurance optimized cryptographic libraries. Low* is a shallow embedding of a small, sequential, well-behaved subset of C in F*, a dependently- typed variant of ML aimed at program verification. Departing from ML, Low* does not involve any garbage collection or implicit heap allocation; instead, it has a structured memory model à la CompCert, and it provides the control required for writing efficient low-level security-critical code. By virtue of typing, any Low* program is memory safe. In addition, the programmer can make full use of the verification power of F* to write high-level specifications and verify the functional correctness of Low* code using a combination of SMT automation and sophisticated manual proofs. At extraction time, specifications and proofs are erased, and the remaining code enjoys a predictable translation to C. We prove that this translation preserves semantics and side-channel resistance. We provide a new compiler back-end from Low* to C and, to evaluate our approach, we implement and verify various cryptographic algorithms, constructions, and tools for a total of about 28,000 lines of code. We show that our Low* code delivers performance competitive with existing (unverified) C cryptographic libraries, suggesting our approach may be applicable to larger-scale low-level software.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{ProtzenkoZRRWBD17,
title = {Verified low-level programming embedded in F*},
author = {Jonathan Protzenko and Jean-Karim Zinzindohoué and Aseem Rastogi and Tahina Ramananandro and Peng Wang and Santiago Zanella-Béguelin and Antoine Delignat-Lavaud and Cătălin Hriţcu and Karthikeyan Bhargavan and Cédric Fournet and Nikhil Swamy},
journal = {Proceedings of the ACM on Programming Languages},
volume = {1},
number = {ICFP},
year = {2017},
doi = {10.1145/3110261}
}