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

# F*：一种面向证明的编程语言 来源：https://fstar-lang.org/ ## 简介 --- F\*（读作 F star）是一种通用的面向证明的编程语言，既支持纯函数式编程，也支持带效果（effectful）的编程。它将依赖类型的强大表现力与基于 SMT 求解的证明自动化以及基于策略（tactic）的交互式定理证明相结合。 F\* 程序默认编译为 OCaml。F\* 的各个子集还可以通过名为 KaRaMeL (https://github.com/FStarLang/karamel) 的工具提取为 F#、C 或 Wasm，或者使用 Vale (https://github.com/project-everest/vale) 工具链提取为汇编代码。F\* 本身由 F\* 实现，并使用 OCaml 引导（bootstrap）。 F\* 在 GitHub (https://github.com/FStarLang/FStar) 上开源，目前由微软研究院 (https://research.microsoft.com/)、Inria (https://team.inria.fr/prosecco/) 以及社区积极开发。 ## 下载 --- F\* 以 Apache 2.0 许可证 (https://raw.githubusercontent.com/FStarLang/FStar/master/LICENSE) 发布。适用于 Windows、Linux 和 Mac OS X 的二进制文件会定期发布在 GitHub 的 releases 页面 (https://github.com/fstarlang/fstar/releases) 上。你也可以按照 INSTALL.md (https://github.com/FStarLang/FStar/blob/master/INSTALL.md) 中的说明，通过 OPAM、Docker、Nix 安装 F\*，或从源码构建。 ## 学习 F\* --- 一本在线书籍《Proof-oriented Programming In F\*》(https://fstar-lang.org/tutorial/proof-oriented-programming-in-fstar.pdf) 正在撰写中，并会定期在线更新。你可能希望在浏览器中点击下方图片尝试其中的示例和练习时阅读此书。 F\* 教程 (https://fstar-lang.org/tutorial) ## Low\* 我们还有一个涵盖 Low\* (https://fstarlang.github.io/lowstar/html/) 的教程。Low\* 是 F\* 的一个底层子集，可以由 KaRaMeL 编译为 C 语言。 ## 课程材料 F\* 课程经常在各种季节学校（seasonal schools）中讲授。其中一些课程的讲义和材料也是很有用的资源。 - 在 F\* 中嵌入面向证明的编程语言 - 俄勒冈编程语言夏季学校（2021）(https://www.cs.uoregon.edu/research/summerschool/summer21/) 的在线讲座： 讲义、幻灯片、代码 (https://fstar-lang.org/oplss2021/index.html) - 使用 F\* 和 Meta-F\* 进行形式化验证 - ECI 2019 (https://eci2019.dc.uba.ar/) 的讲座和教程： 讲义、幻灯片、代码 (https://fstar-lang.org/eci2019/index.html) - 验证底层代码的正确性与安全性 - 俄勒冈编程语言夏季学校（2019）(https://www.cs.uoregon.edu/research/summerschool/summer19/) 的讲座： 讲义、幻灯片、代码 (https://fstar-lang.org/oplss2019/index.html) - 使用 F\* 进行程序验证 - 2018 EUTypes 夏季学校 (https://sites.google.com/view/2018eutypesschool/home) 的课程，2018 年 8 月 8-12 日，马其顿奥赫里德 课程材料 (https://sites.google.com/view/2018eutypesschool/ahman) ## 社区 --- 请使用 GitHub Discussions (https://github.com/FStarLang/FStar/discussions) 提问关于 F\* 的问题、了解公告等。 虽然我们之前使用过 Slack 实例，但我们旨在将在线社区整合到 Zulip 上的这个公共论坛 (https://fstar.zulipchat.com/) 中。 我们还有一个邮件列表，流量很低。你可以通过 fstar-mailing-list (https://groups.google.com/g/fstar-mailing-list) 订阅。 F\* PoP Up 研讨会 (https://fstar-lang.org/popup/seminar.html) 是一个面向所有用户的开发者会议。我们计划每月举行一次，尽管日程不固定——希望在那里见到你！ 你也可以通过 [email protected] 联系 F\* 的维护者。 ## 应用 --- F\* 被用于多个工业和学术项目。这里列出其中一些。如果你在项目中使用 F\*，请通过 fstar-mailing-list (https://groups.google.com/g/fstar-mailing-list) 告诉我们。 ## Project Everest Project Everest (https://project-everest.github.io/) 是一个伞形项目，用 F\* 开发高可信的安全通信软件。F\* 开发的很大一部分是由 Project Everest 的目标场景驱动的。Project Everest 的多个分支继续作为独立项目存在，包括下面列出的一些项目。 ## HACL\*、ValeCrypt 和 EverCrypt HACL\* (https://hacl-star.github.io/) 是一个高可信密码学原语库，用 F\* 编写并提取为 C 语言。ValeCrypt (https://github.com/hacl-star/hacl-star/tree/main/vale) 提供用 Vale 实现并经过形式化证明的密码学原语。Vale 是一种嵌入在 F\* 中的经过验证的汇编语言编程框架。EverCrypt (https://hacl-star.github.io/EverCryptDoc.html) 将两者组合成一个统一的密码学提供者。这些项目的代码现已用于多个生产项目中，包括 Mozilla Firefox (https://blog.mozilla.org/security/2017/09/13/verified-cryptography-firefox-57/)、Linux 内核 (https://github.com/torvalds/linux/blob/0f2a4af27b649c13ba76431552fe49c60120d0f6/lib/crypto/curve25519-hacl64.c#L1)、Python (https://github.com/python/cpython/issues/99108)、mbedTLS (https://github.com/Mbed-TLS/mbedtls/blob/development/3rdparty/everest/)、Tezos 区块链 (https://www.reddit.com/r/tezos/comments/8hrsz2/tezos_switches_cryptographic_libraries_from/)、ElectionGuard (https://www.electionguard.vote/) 电子投票 SDK 以及 Wireguard (https://www.wireguard.com/) VPN。 ## EverParse EverParse (https://project-everest.github.io/everparse/) 是一个面向二进制格式的解析器生成器，它生成从经过形式化证明的 F\* 提取出的 C 代码。EverParse 生成的解析器已用于多个生产项目中，包括 Windows Hyper-V (https://www.microsoft.com/en-us/research/blog/everparse-hardening-critical-attack-surfaces-with-formally-proven-message-parsers/)，其中通过 Azure 云平台的每个网络数据包都首先由 EverParse 生成的代码进行解析和验证。EverParse 还用于其他生产环境，包括 ebpf-for-windows (https://github.com/microsoft/ebpf-for-windows)。 ## 研究 --- F\* 是一个活跃的研究主题，不仅在编程语言和形式化方法社区，而且在安全性和系统社区的应用视角中也是如此。下面列出其中一些，这些论文的完整引用可参见此参考文献列表 (https://fstar-lang.org/fstar_bib.php)。如果你希望将自己的论文加入此列表，请联系 [email protected]。 ## F\* 及其 DSL 的设计 - Dependent Types and Multi-monadic Effects in F\* (https://fstar-lang.org/papers/mumon/)（POPL 2016）这是描述 F\* 系统的经典参考文献。该语言自 2016 年以来已发生重大演变，但其核心设计和实现基于此论文。 - Verified Low-level Programming Embedded in F\* (https://arxiv.org/abs/1703.00053)（ICFP 2017）描述了 F\* 的 Low\* 子集，这是 F\* 的一个底层子集，可由 KaRaMeL 编译为 C 语言。 - A Verified, Efficient Embedding of a Verifiable Assembly Language (https://dl.acm.org/doi/10.1145/3290376)（POPL 2019）描述了 Vale 语言，一种嵌入在 F\* 中的经过验证的汇编语言。 - Meta-F\*: Proof Automation with SMT, Tactics, and Metaprograms (https://fstar-lang.org/papers/metafstar/)（ESOP 2019）描述了 MetaF\*，这是 F\* 内部的一个元编程系统，用于实现 F\* 的各个方面，从策略引擎到类型类支持。 - Programming and Proving with Indexed Effects (https://fstar-lang.org/papers/indexedeffects/)（TR 2021）描述了 F\* 对用户自定义效果的支持的设计，并提供了一个描述 F\* 逻辑核心的演算。 - Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic (https://fstar-lang.org/papers/steel/)（ICFP 2021）描述了 Steel 语言及其如何使用 SteelCore 并发分离逻辑来验证具有各种形式并发性的命令式程序。 ## 语义与效果 - Verifying Higher-order Programs with the Dijkstra Monad (https://dl.acm.org/doi/10.1145/2499370.2491978)（PLDI 2013）引入了 Dijkstra monad 的概念，这是 F\* 效果系统的核心特性。 - Dijkstra Monads for Free (https://fstar-lang.org/papers/dm4free/)（POPL 2017）展示了如何使用续延传递变换为一类计算 monad 自动推导 Dijkstra monad。 - A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations (https://arxiv.org/abs/1703.00055)（CPP 2018）在 Dijkstra Monads for Free 的基础上构建了一个框架，用于证明关联多个程序或程序执行的性质。 - Dijkstra Monads for All (https://arxiv.org/abs/1903.01237)（ICFP 2019）推广了 Dijkstra monad 的概念，并展示了如何通过 monad 态射系统地关联计算型 monad 和规约型 monad。 - Recalling a Witness: Foundations and Applications of Monotonic State (https://arxiv.org/abs/1707.02466)（POPL 2018）描述了用于推理状态单调演变的程序的程序逻辑设计，例如状态是仅追加日志的情况。该逻辑是 Low\* 和 Steel 的基础。 - SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs (https://fstar-lang.org/papers/steelcore/)（ICFP 2020）描述了 SteelCore 并发分离逻辑，它是 Steel DSL 的基础。 - USSL: A Universe-Stratified, Predicative Concurrent Separation Logic (https://fstar-lang.org/papers/ussl.pdf) 一种嵌入在 F\* 中的基础性、无公理的并发分离逻辑，通过按宇宙层级对谓词进行分层，在谓词性（predicative）设置中支持动态不变式和高阶幽灵状态。 - PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs (https://fstar-lang.org/papers/pulsecore-indirection-2025.pdf)（PLDI 2025）一种嵌入在 F\* 中的基础性、无公理的并发分离逻辑，支持动态不变式和高阶幽灵状态，并具有非直谓性（impredicative）不变式和 later credits。PulseCore 是 Pulse (https://fstar-lang.org/tutorial/book/pulse/pulse.html#pulse-proof-oriented-programming-in-concurrent-separation-logic) 的基础。Pulse 是 F\* 中用于在并发分离逻辑中进行面向证明编程的嵌入式语言。 ## 在安全与密码学中的应用 许多将 F\* 应用于安全和密码学的论文可以在 Project Everest 参考文献列表 (https://project-everest.github.io/papers/) 中找到。这里我们提及一些重要的论文，以及一些与 Project Everest 无关的应用。 - WYS\*: A DSL for Verified Secure Multi-party Computations (https://arxiv.org/abs/1711.06467)（POST 2017）描述了 WYS\* 语言，一种用于编写经过验证的混合模式安全多方计算的领域特定语言。 - Implementing and Proving the TLS 1.3 Record Layer (https://eprint.iacr.org/2016/1178)（S&P 2017）描述了在 Low\* 中实现的经过验证的 TLS-1.3 记录层。 - HACL\*: A Verified Modern Cryptographic Library (https://eprint.iacr.org/2017/536)（CCS 2017）描述了 HACL\*，一个用 Low\* 实现的经过验证的密码学库。 - Formally Verified Cryptographic Web Applications in WebAssembly (https://ieeexplore.ieee.org/document/8835291)（S&P 2019）开发了 LibSignal\*，一个使用 HACL\* 在 F\* 中实现的 Signal 协议实现，并由 KaRaMeL 编译为 Wasm。 - EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider (https://project-everest.github.io/assets/evercrypt.pdf)（S&P 2020）一个将 HACL\* 和 Vale 的 C 代码与汇编代码相结合的密码学提供者，以及一些构建在其上的应用，包括一个经过验证的高性能 Merkle 树，该树曾用于 Microsoft Azure CCF 的初始版本。 - HACL×N: Verified Generic SIMD Crypto (for all your favorite platforms) (https://project-everest.github.io/assets/haclxn.pdf)（CCS 2020）通过元编程生成密码学原语的向量化版本，实现了“编写一次，免费获得向量化版本”的风格。 - A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer (https://project-everest.github.io/assets/everquic.pdf)（S&P 2021）在 Low\* 中实现的经过验证的 QUIC 记录层，并结合了用 Dafny 实现的协议逻辑。 - DICE\*: A Formally Verified Implementation of DICE Measured Boot (https://www.microsoft.com/en-us/research/publication/dice-a-formally-verified-implementation-of-dice-measured-boot/)（USENIX Security 2021）证明了微控制器 DICE 测量启动协议的正确性和安全性，该协议使用 EverCrypt 和 EverParse 在 Low\* 中实现。 - DY\*: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code (https://ieeexplore.ieee.org/document/9581188)（Euro S&P 2021）一个用于对 F\* 中开发的密码协议实现进行基于类型的符号安全分析的框架。 - A Tutorial-Style Introduction to DY\* (https://link.springer.com/chapter/10.1007/978-3-030-91631-2_4)（LNCS 2021）是的，这是一篇 DY\* 的教程式介绍。 - An In-Depth Symbolic Security Analysis of the ACME Standard (https://dl.acm.org/doi/10.1145/3460120.3484588)（CCS 2021）使用 DY\* 证明了 ACME 证书签发和管理协议模型的安全性。 - Noise\*: A Library of Verified High-Performance Secure Channel Protocol Implementations (https://ieeexplore.ieee.org/document/9833621)（S&P 2022）通过元编程为一族安全信道协议生成可证明安全的实现。 - TreeSync: Authenticated Group Management for Messaging Layer Security (https://www.usenix.org/system/files/sec23fall-prepub-372-wallez.pdf)（USENIX Security 2023）F\* 中 MLS 的参考实现，并使用 DY\* 框架证明了其安全性。 - Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification (https://dl.acm.org/doi/10.1145/3607844)（ICFP 2023）描述了 HACL\* 中用于密码学构造的通用实现的证明工程技术，这些实现可以被反复特化为多种具体的 C 实现。这里使用的技术促成了经过验证的密码学代码被采用到 Python 编程语言的标准库中。 - Verifying Indistinguishability of Privacy-Preserving Protocols (https://kirby.linvill.net/pdfs/indistinguishability_paper.pdf)（OOPSLA 2023）在 F\* 中提供了一个名为 Waldo 的库，使得可以在网络协议的通信迹上证明不可区分性。 - Comparse: Provably Secure Formats for Cryptographic Protocols (https://eprint.iacr.org/2023/1390)（CCS 2023）提供了适用于符号协议分析器的数据格式解析库。Comparse 提供位级精确的格式说明，使 DY\* 协议分析框架能够推理具体消息，并发现其以前会遗漏的协议缺陷。 - Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust (https://eprint.iacr.org/2025/980)（CCS 2025）开发了 Bert13，一种具有后量子特性的 Rust 版 TLS-1.3 实现，并通过翻译（使用 Hax）到多种证明器后端来证明其正确性和安全性，其中包括用于证明 Rust 代码不会恐慌（panic）的 F\*。