F*: 一般目的の証明指向プログラミング言語

はじめに ダウンロード 学習 コミュニティ 利用法 研究 人々 F*（エフスターと発音）は、純粋関数型プログラミングと効果的プログラミングの両方をサポートする、一般目的の証明指向プログラミング言語です。依存型（dependent types）の表現力と、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のリリースページに定期的に投稿されています。OPAM、Docker、NixからF*をインストールすることも、INSTALL.mdの指示に従ってソースからビルドすることもできます。 学習 オンライン書籍「Proof-oriented Programming In F*」が執筆されており、定期的にオンラインで更新が投稿されています。以下の画像をクリックして、ブラウザで例や演習を試しながら読むのが良いでしょう。 Low* KaRaMeLによってCにコンパイルできるF*の低レベルサブセットであるLow*のチュートリアルもあります。 コース教材 F*のコースは、様々な季節学校でしばしば教えられています。それらのうちのいくつかの講義やコース教材も役立つリソースです。 Embedding Proof-oriented Programming Languages in F* Oregon Programming Language Summer School (2021) のオンライン講義：講義ノート、スライド、コード Formal Verification with F* and Meta-F* ECI 2019 の講義とチュートリアル：講義ノート、スライド、コード Verifying Low-Level Code for Correctness and Security Oregon Programming Language Summer School (2019) の講義：講義ノート、スライド、コード Program Verification with F* 2018 EUTypes Summer School、8月8-12日、2018年、オフリド、マケドニアでのコース教材 コミュニティ F*に関する質問、発表事項の確認などには、GitHub Discussionsをご利用ください。以前はSlackインスタンスを使用していましたが、Zulipのこの公開フォーラムにオンラインコミュニティを統合することを目指しています。トラフィックは非常に少ないですが、メーリングリストもあります。fstar-mailing-listで購読できます。ユーザーと開発者の会議であるF* PoP Up Seminarは、すべての人に開かれています。月に一度の開催を目指していますが、スケジュールは不規則です。皆様のご参加をお待ちしております。メンテナーにはfstar-maintainers@googlegroups.comまでご連絡ください。 利用法 F*は、産業界および学術界のいくつかのプロジェクトで使用されています。いくつか例を挙げます。もしあなたのプロジェクトでF*を使用している場合は、fstar-mailing-listにご連絡ください。 Project Everest Project Everestは、F*で高信頼性のセキュア通信ソフトウェアを開発するアンブレラプロジェクトです。F*の開発の大部分は、Project Everestが対象とするシナリオによって動機付けられています。Project Everestからのいくつかの派生プロジェクトは、以下にリストされているものの一部を含め、独自のプロジェクトとして継続しています。 HACL*, ValeCrypt, and EverCrypt HACL*は、F*で記述されCに抽出された高信頼性暗号プリミティブのライブラリです。ValeCryptは、F*に埋め込まれた検証済みアセンブリ言語プログラミングのフレームワークであるValeで、暗号プリミティブの形式的に証明された実装を提供します。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までご連絡ください。 The Design of F* and its DSLs Dependent Types and Multi-monadic Effects in F* (POPL 2016) これはF*システムを説明する標準的な参考文献です。この言語は2016年以降大きく進化しましたが、そのコア設計と実装はこの論文に基づいています。 Verified Low-level Programming Embedded in F* (ICFP 2017) これはF*の低レベルサブセットであるLow*フラグメントを説明しており、KaRaMeLによってCにコンパイルできます。 A Verified, Efficient Embedding of a Verifiable Assembly Language (POPL 2019) これは、F*に埋め込まれた検証済みアセンブリ言語であるVale言語を説明しています。 Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms (ESOP 2019) これは、F*内のメタプログラミングシステムであるMetaF*を説明しており、その戦術エンジンから型クラスのサポートまで、F*の様々な側面の実装に使用されています。 Programming and Proving with Indexed Effects (TR 2021) これは、F*のユーザー定義効果のサポートの設計を説明し、F*の論理コアを記述する計算式を提供します。 Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic (ICFP 2021) これは、Steel言語とそのSteelCore並行分離論理を使用した、様々な形式の並行処理を伴う命令型プログラムの証明への応用を説明しています。 Semantics and Effects Verifying Higher-order Programs with the Dijkstra Monad (PLDI 2013) これは、F*の効果システムの中核機能であるDijkstraモナドの概念を紹介しています。 Dijkstra Monads for Free (POPL 2017) これは、継続渡し変換を使用して、計算モナッドのクラスに対してDijkstraモナドを自動的に導出する方法を示しています。 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モナドの概念を一般化し、計算モナッドと仕様モナッドをモナドモルフィズムを介して体系的に関連付ける方法を示しています。 Recalling a Witness: Foundations and Applications of Monotonic State (POPL 2018) これは、状態が単調に進化するプログラム（例：追記専用ログである状態）を推論するためのプログラム論理の設計を説明しています。この論理は、Low*とSteelの両方の基盤となっています。 SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs (ICFP 2020) これは、Steel DSLの基盤であるSteelCore並行分離論理を説明しています。 USSL: A Universe-Stratified, Predicative Concurrent Separation Logic 予測可能な設定で動的な不変条件と高階ゴースト状態をサポートする、宇宙レベルの階層に従って述語を層別化することにより、F*に浅く埋め込まれた、基礎的で公理のない並行分離論理です。 PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs (PLDI 2025) F*に浅く埋め込まれた、基礎的で公理のない並行分離論理であり、予測不可能な不変条件と後続クレジットを伴う動的な不変条件と高階ゴースト状態をサポートします。PulseCoreは、並行分離論理における証明指向プログラミングのためのF*に埋め込まれた言語であるPulseの基盤です。 セキュリティと暗号化への応用 Project Everestの参考文献リストには、F*をセキュリティと暗号化に応用した多くの論文があります。ここでは、いくつかの著名なものや、関連のない他の応用例もいくつか紹介します。