証明指向言語F*の概要と活用事例
原題: F*: A general-purpose proof-oriented programming language
なぜ重要か
形式検証済みコードがFirefoxやLinuxカーネル等の主要OSS・商用製品に採用され、セキュリティクリティカルなソフトウェア開発における証明指向言語の実用性が広く示されている。
F*（エフスター）はMicrosoft ResearchとInriaが共同開発するオープンソースの汎用証明指向プログラミング言語で、依存型とSMTソルバーおよびタクティクベースの定理証明を組み合わせる。デフォルトでOCamlにコンパイルされ、KaRaMeLによりCやWasm、Valeツールチェーンによりアセンブリへの出力も可能。Apache 2.0ライセンスでWindows・Linux・macOS向けバイナリを公開中。
F*は純粋関数型プログラミングとエフェクトを伴うプログラミングの両方をサポートする汎用の証明指向プログラミング言語。依存型の表現力と、SMTソルビングに基づく証明自動化、タクティクベースのインタラクティブな定理証明を組み合わせている点が特徴。F*自身もF*で実装されており、OCamlによってブートストラップされている。
コンパイルターゲットはデフォルトでOCamlだが、F#・C・Wasmへの抽出にはKaRaMeL、アセンブリへの変換にはValeツールチェーンが利用可能。ソースコードはGitHubで公開され、OPAM・Docker・Nixによるインストールにも対応している。
産業・学術の双方で複数のプロジェクトに採用されている。Project Everestでは高保証なセキュア通信ソフトウェアの開発に利用。その派生プロジェクトHACL*は高保証な暗号プリミティブライブラリとしてF*で記述されCに抽出され、Mozilla Firefox・Linuxカーネル・Python・mbedTLS・Tezosブロックチェーン・ElectionGuard電子投票SDK・WireGuard VPNなど広範なプロダクションプロジェクトで採用されている。
ValeCryptはVerified Assembly Language（Vale）フレームワーク上で暗号プリミティブの形式証明済み実装を提供し、EverCryptはHACL*とValeCryptを統合した単一の暗号プロバイダーとして機能する。
さらにEverParseは形式証明済みF*コードからCコードを生成するバイナリフォーマット向けパーサジェネレータで、Windows Hyper-Vに採用されAzureクラウドプラットフォームを通過するすべてのネットワークパケットの解析に利用されている。
学習リソースとして、オンラインブック「Proof-oriented Programming In F*」が継続的に更新公開されており、ブラウザ上でサンプルや演習を試せる環境も提供。コミュニティはGitHub DiscussionsおよびZulipパブリックフォーラムで運営されている。