F*：一种通用的面向证明的编程语言

简介 F*（发音为 F star ）是一种通用的面向证明的编程语言，支持纯函数式和有效的编程。它将依赖类型的表达能力与基于 SMT 求解和基于策略的交互式定理证明的证明自动化相结合。默认情况下，F* 程序编译为 OCaml。 F* 的各种片段还可以通过 KaRaMeL 工具提取为 F#、C 或 Wasm，或者使用 Vale 工具链进行汇编。 F* 在 F* 中实现并使用 OCaml 进行引导。 F* 在 GitHub 上开源，并由 Microsoft Research、Inria 和社区积极开发。下载 F* 是根据 Apache 2.0 许可证分发的。 Windows、Linux 和 Mac OS X 的二进制文件定期发布在 GitHub 的发布页面上。您还可以按照 INSTALL.md 中的说明从 OPAM、Docker、Nix 安装 F*，或从源代码构建它。学习 F* 正在编写一本在线书籍《F* 中的面向证明的编程》，并定期更新发布在网上。您可能想通过单击下图在浏览器中尝试示例和练习的同时阅读它。 Low* 我们还有一个涵盖 Low* 的教程，它是 F* 的低级子集，可以由 KaRaMeL 编译为 C。课程材料 F* 课程通常在各种季节性学校教授。其中一些人的讲座和课程材料也是有用的资源。在 F* 中嵌入面向证明的编程语言 使用 F* 和 Meta-F* 进行形式验证 使用 F* 验证低级代码以实现正确性和安全性 程序验证 使用 F* 在工业和学术环境中的多个项目中使用。我们在这里列出其中的一些。如果您在项目中使用 F*，请写信给 fstar-mailing-list 告知我们。 Project Everest Project Everest 是一个在 F* 中开发高保证安全通信软件的伞式项目。 F* 开发的很大一部分是由珠穆朗玛峰项目的目标场景推动的。珠穆朗玛峰计划的几个分支继续作为自己的项目，包括下面列出的一些项目。 HACL*、ValeCrypt 和 EverCrypt HACL* 是一个高保证加密原语库，以 F* 编写并提取为 C。ValeCrypt 在 Vale 中提供了经过正式验证的加密原语实现，Vale 是一个嵌入在 F* 中的经过验证的汇编语言编程框架。 EverCrypt 将它们组合成一个单一的加密提供程序。这些项目的代码现已在多个项目的生产中使用，包括 Mozilla Firefox、Linux 内核、Python、mbedTLS、Tezos 区块链、ElectionGuard 电子投票 SDK 和 Wireguard VPN。 EverParse EverParse 是一个二进制格式的解析器生成器，可生成从经过形式验证的 F* 中提取的 C 代码。 EverParse 的解析器在多个项目的生产中使用，包括在 Windows Hyper-V 中，其中通过 Azure 云平台的每个网络数据包首先由 EverParse 生成的代码进行解析和验证。 EverParse 还用于其他生产设置，包括 ebpf-for-windows 。研究 F* 是一个活跃的研究主题，无论是在编程语言和形式方法社区，还是从安全和系统社区的应用程序角度来看。我们在下面列出了其中的一些，并在本参考书目中提供了这些论文的完整引用。如果您希望您的论文包含在此列表中，请联系 fstar-maintainers@googlegroups.com。 F* 及其 DSL 的设计，使用 Dijkstra Monad 验证高阶程序的语义和效果（PLDI 2013），介绍了 Dijkstra monad 的概念，这是 F* 效果系统的核心特征。 Dijkstra Monads for Free (POPL 2017)，展示了如何使用连续传递转换自动导出一类计算 monads 的 Dijkstra monads A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations (CPP 2018)，它建立在 Dijkstra Monads for Free 工作的基础上，构建一个用于证明与多个程序或程序相关的属性的框架处决。 Dijkstra Monads for All (ICFP 2019)，概括了 Dijkstra monad 的概念，并展示了如何通过 monad 态射系统地将计算和规范 monad 联系起来。回忆见证：单调状态的基础和应用 (POPL 2018)，它描述了用于推理状态单调演变的程序的程序逻辑设计，例如，状态是仅附加日志的情况。这一逻辑是 Low* 和 Steel 的基础。 SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependly Typed Programs (ICFP 2020)，它描述了 SteelCore 并发分离逻辑，这是 Steel DSL 的基础。 USSSL: A Universe-Stratified, Predicative Concurrent Separation Logic 一种基础的、无公理的并发分离逻辑，浅层嵌入到 F* 中，支持