仕様は存在しない (2025)

始める お問い合わせ 私たちは、すべての関心のあるパートナー、協力者、潜在的なクライアントと個人的につながることに誇りを持っています。Galoisとのつながり方について簡単な説明を添えてメールでお問い合わせください。1営業日以内にご返信できるよう最善を尽くします。 メール contact@galois.com 電話 503.626.6616 仕様は存在しない Mike Dodds 2025年6月16日 この記事は、「何が機能し、（何が機能しないか）形式手法の販売」という記事の補足です。 これは、私が2024年末に行った講演の一部として生まれました。 いくつかのことは困難であり、いくつかのことは単に高価です。 想像してみてください。エイリアンが私たち全員を殺しに来ています。人類は最高の交渉人を派遣し、エイリアンは、私たちがGCCの形式検証版を、コードのすべての行を…1年以内にリリースした場合のみ、恐ろしい攻撃を中止すると発表します。 当然の混乱の後、G7の首脳たちはXavier Leroyを呼び出し、彼に莫大な小切手を渡し、彼にそれをやらせるように言います。 すぐに、世界中の数学者の倉庫が昼夜を問わずRocqの定理を証明しています。調整の課題は膨大ですが、彼らはそれを成し遂げます！ エイリアンは去り、Xavierはフィールズ賞、EGOT、そして5つのノーベル賞すべてを獲得し、1、そして他のすべての人々はAIについて心配するのに戻ります。 私が言いたいのは、形式検証可能なコンパイラを構築する方法を基本的に知っているということです。私たちはすでにそれをやりました。 形式検証可能な暗号ライブラリ、パーサー、マイクロカーネルについても同様です。 GCCが形式検証されていない理由は、そうすることが不合理に高価だからです。コストを正当化するほどの利益が得られないでしょう。 しかし、エイリアンが現れたら、MCUフェーズ3（22億〜24億ドル）よりも安くできると賭けてもいいです。 さて、別の話です。エイリアンが私たち全員を殺しに来ており、形式検証可能なWebブラウザを要求しています。 Xavierは手を挙げます（今回は彼を連れてきました）そして尋ねます、ええと…彼らは正確に何を求めているのですか？ 例えば、Webブラウザとは正確には何なのでしょうか？ この質問はエイリアンを混乱させ、激怒させます！ Chromeの形式仕様があるはずですよね？私たちはそれを構築したのではないでしょうか？ そして、まあ、人類はこれで終わりです。 問題は、Chrome、ワードプロセッサ、あるいはPDFドキュメントフォーマットのような単純なものでさえ、形式仕様を持っていないことです。 いくつかのドメインを除いて、仕様は存在しません。私は単に誰もまだそれを書いていないという意味ではなく、正確で一貫した仕様を書くことができると信じる理由があるという意味です。 もし第二のエイリアンが現れたら、私たちは多くの新しいコンピュータサイエンスを急速に発明しなければならないでしょう。そして、MCUのお金でさえそれを成し遂げられるかどうかはわかりません。 形式仕様は形式的かつ具体的であるべきです そもそもなぜ形式仕様が欲しいのでしょうか（エイリアンは別として）？ 形式仕様とは、システムの要約または説明として機能するのに十分な精度で、私たちが望むものを述べることです。 システムを調べる代わりに、仕様を調べることができます。 これは一般的に、システムのすべてのことを決定するわけではありません（それは地図であり、領土ではありません）。 例えば、Rustの借用チェッカーは、「このプログラムはメモリエラーを生成しない」という単純な仕様を保証します。 安全なRustプログラムを私に与えれば、それは多くのことを行うかもしれませんが、それは行いません。 何かを形式的に検証したいのであれば、形式仕様が必要です。 そうでなければ、何を検証しているのでしょうか？ 実際の検証作業は、数学者の倉庫がRocqの定理を書くことを意味するかもしれませんし、Rustの借用チェッカーを実行することを意味するかもしれません。 しかし、仕様がなければ、始めることができません。 形式手法は古くからあり、人々は多くのことを仕様化しようとしてきました。 しかし、経験則として、最も有用な形式仕様はしばしば以下の特徴を持っています。 数学的にクリーン：仕様を、比較的単純な数学的概念のコレクションで記述できます。 推論しやすい：仕様を、人間の直感または形式分析によって、システムを理解するための方法として使用できます。 カプセル化されている：システムの「内部」と「外部」の間に明確な境界があり、仕様はその境界で何が起こるかを記述します。 広く合意されている：システムの設計者とユーザーは、システムが実際に仕様に一致することを期待しています。マップは領土の良い説明です。 変化に対して安定している：システムが進化しても、仕様はあまり変化しません。マップは小さな違いから抽象化されます。 いくつかのシステムは、これらの要件に非常に自然に適合するように見えます。例えば、コンパイラ、暗号ライブラリ、パーサー、マイクロカーネルです。 これらのシステムは自然に形式化可能であると言えるかもしれません。2 そのリストに見覚えがありますか？その通りです。これらはまさに形式検証の成功例です！ 仮説があります。質の高い形式仕様が得られれば、システムの検証は難しくなく、単に高価なだけです。 そして、形式検証ファンにとって、ここにまだ多くの未開発の可能性があります。 コンパイラ、マイクロカーネルなどはセキュリティクリティカルなコンポーネントですが、今日私たちが使用しているシステムで形式検証されているものはほとんどありません。 G7に電話してください。時間です。GCCを検証しましょう！ *記事終了、ラップトップを閉じる* いや、まだあります。 一部の人々はCompCertとSeL4を見て、「なぜ私のシステムを形式検証できないのですか？」と尋ねます。 しかし、自然に仕様化可能なシステムは、非常に小さく、非常に代表的でないニッチであると思います。 現実の世界では、ほとんどのシステムは仕様化が非常に困難であり、これは世界をさらに形式検証したい場合に大きな問題となります。 実際、仕様が多すぎます 形式仕様がないかもしれませんが、開発者は常に非形式的な仕様を書いています。 システムには、重要な情報を持つさまざまな種類の仕様が存在する可能性があります。 文章によるドキュメント - 社内向けの設計ドキュメント、社外向けのユーザーマニュアルやガイド、ホワイトペーパー、RFCなど。 スライドデッキ - 特に米国政府では驚くほど一般的です。 システム自体 - 特にレガシーシステムの場合、システムは「それがすることをする」だけであり、いかなる変更も定義により仕様に反します。 ユーザーストーリー - Webブラウザのようなユーザー向けアプリケーションの場合、ユーザーストーリーのセットが実際の最上位仕様である可能性がありますが、これらを形式的に表現することは通常非常に困難です。 単体テストおよび統合テスト - しばしば形式仕様に最も近いものですが、単一の入力またはシナリオに限定されます。 その他多数、参照実装、インラインコメント、チーム内の暗黙的/実践的なノウハウ、顧客の好み、規制要件、カフェのナプキンに走り書きされたメモなどを含みます。 実際、不完全なカバレッジを持つ多数の部分的な仕様があり、それらのどれも互いに一致しません。 Galoisのクライアントのためにプロジェクトのスコープを設定する際、私はしばしばこのような会話をします。 私：「[あなたの巨大なシステム]の仕様はありますか？」 クライアント：「はい、ここに2枚のスライドのパワポデッキがあります」 〜および/または〜 クライアント：「はい、ここに半構造化された文章で7000ページの要件ドキュメントがあります」 これらすべてが、問題のシステムを形式検証しようとする際に、次のような会話につながります。 私：「システムが[何か]を行うことがわかりましたが、あなたの仕様は[何か別のこと]を示唆しています。」 クライアント：「ああ、ふむ、それは問題ありません」 〜または〜 クライアント：「ええ、6ヶ月前に変更しました」 このような会話を約40,000回経験した後、私はサーカス道化師への再訓練を考えるか、単に川に身を投げることを考えるようになります。 クライアントと一緒に座って形式仕様を作成することもできます。 私：「仕様で[ある種の動作]を許可しますか？」 クライアント：「ええと…わかりません、その状況については考えていません」 私：「それを許可すると、[別の動作]も許可する必要があります。それは問題になりますか？」 クライアント：「その状況についてもわかりません…これはどれくらい時間がかかりますか？」 形式仕様を作成することは、非常に困難な作業であると考えるようになりました。 それは、設計者やエンジニアが通常持っていない、あるいは、より重要なこととして、必要としない、システムの上位レベルのビューを必要とします。 対照的に、非形式的な仕様は曖昧である可能性があります。