Isabelle/HOL：Nitro分離エンジンの背後にある証明支援系

Amazonの2025年 re:Inventカンファレンスにおいて、Amazon Web Services（AWS）はNitro Isolation Engine（NIE）を発表しました。これは、AWSクライアントにリソースを提供しつつ、顧客データのセキュリティを確保する役割を担うソフトウェアモジュールです。AWSはまた、Isabelle/HOLと呼ばれる証明支援系を用いて、この隔離エンジンの正確性とセキュリティ保証の形式的検証を完了したことを発表しました。初の形式的に検証されたクラウドハイパーバイザーとして、NIEはクラウドセキュリティの新たな基準を確立します。証明支援系とは、数学的定理、ハードウェアやソフトウェアシステムの正当性、あるいはその中間にあるあらゆるものについて、人間のユーザーが形式的証明を構築するのを支援する自動化ツールです。一般的に使用されている証明支援系は複数ありますが、我々は表現力、自動化、証明の可読性、スケーラビリティのバランスが適切であったため、Isabelle/HOLを選択しました。では、それは具体的にどういう意味でしょうか？

コンピューターによる論理的推論

数学には固定された言語は存在しませんが、プログラミング言語が計算タスクを表現するのと同様に、数学的推論を表現するための言語を作り出すことができます。そして、プログラミング言語が表現力と性能の間でトレードオフを伴うのと同様に、数学的言語は表現力と自動化の容易さの間でトレードオフを伴います。自動化は極めて重要です。なぜなら、形式的証明の構築は時間がかかり、極めて退屈な作業であり、ちょうどビンの中に船を作るようなものだからです。最も基本的な数学的言語はブール論理、すなわちAND、OR、NOTという二項演算子の世界です。この言語は非常に単純であるため、これに対して強力な自動ソルバーが存在します。2016年、カーネギーメロン大学の教授（現在はAmazon Scholar）であるMarijn Heule氏とその同僚は、未解決の数学的問題である「ブール・ピタゴラス三つ組問題」をブール論理にエンコードし、自動ソルバーを用いて史上最大（200テラバイト）の証明を作成するのに貢献しました。

一階述語論理と呼ばれるより豊かな数学的言語を使えば、整数などの関心領域について語り、その領域上で関数を定義することができます。また、「すべての」や「存在する」といった量化子を命題に含めることで、ブール論理を超えることができます。この種の言語では、「2より大きいすべての素数は奇数である」といった文を表現できます。ルイス・キャロルによる次の定理も証明できます：「ダンスを踊るカモはいない。士官はダンスを断ることは決してない。私の家禽はすべてカモである。したがって、私の家禽に士官はいない」。

しかし、多くの人は、プログラミングで行うように型を定義できる、さらに強力な数学的言語を好みます。高階論理では、Haskellのような関数型プログラミング言語に見られるような関数型さえあります。高階論理は一階述語論理よりもはるかに豊かで、「数1を含み、加法について閉じているすべての集合は、すべての正の整数を含む」といった文を表現できます。これは数学の大部分を表現するのに十分なほど豊かであるように思われます。最も豊かな数学的言語（依存型理論と呼ばれる）では、型が任意の値をパラメータとして取ることさえ可能です（例：T(i)、ここでiは整数）。そのような言語で最もよく知られているのはLeanとRocqです。

一階述語論理には強力な自動定理証明器が存在しますが、高階論理やそれ以上では、完全な自動化は利用できません。これが表現力の代償です。証明支援系は、部分的な自動化と独自の証明探索をコーディングする可能性によってサポートされ、ユーザーが対話的に証明を構築することを可能にします。証明支援系は、通常、定理を作成する権限をコードの限られた部分にのみ与えるカーネルアーキテクチャを通じて、論理法則への厳格な準拠を強制します。証明支援系はまた、膨大になる可能性のある形式的仕様階層の対話的開発をサポートします。例えば、Nitro Isolation Engine（NIE）の検証は、Graviton-5プロセッサのアーキテクチャ仕様、ハイパーコールのRustコードとその機能的正確性、そして証明されるべきセキュリティ特性の仕様に基づいています。これらは、形式的証明を構成する25万行の大部分を占めています。

高階論理は、HOLとHOL Lightという2つの密接に関連する証明支援系によってサポートされており、1990年代以降、ハードウェア設計、浮動小数点アルゴリズム、純粋数学の検証に使用されてきました。AWSシニアプリンシパルアプライドサイエンティストのJohn Harrison氏はHOL Lightを開発し、暗号アルゴリズムの最適化バージョンを検証することで、AmazonのGraviton2チップ上のデジタル署名の性能を最大94％向上させるために使用しました。そのコードは繊細であり、網羅的なテストは実行不可能でした。そのような重要なソフトウェアをデプロイする前には、完全な機能的正確性の形式的検証のみが適切だったのです。しかし、今日我々が関心を持っているのはIsabelle/HOLです。

Isabelle/HOLの概要

Isabelle/HOLと他のHOLシステム（いずれも高階論理に基づく）の最も目に見える違いは、その仕様記述言語と証明言語です。ほとんどの証明支援系では、ユーザーは証明したいことを述べ、その後、一種のモグラ叩きゲームのように元のゴールを一連のサブゴールに置き換えるコマンドのリストを記述します。Isabelleでは、そしてある程度Leanでも、証明言語は望ましい中間ゴールを明示的に書き出すことを可能にし、より制御された証明プロセスとより読みやすい証明文書を実現します。オンラインには多くの例があります。

その他の注目すべき機能は以下の通りです：

• ユーザー設定可能なパーサー：これにより、仕様にRust言語の重要なフラグメントを埋め込むことができました。
• 型クラス：原則に基づくオーバーロードを実現し、例えば+に自然な意味を与えることができ、様々な数値型だけでなく、マシンワードや他の適切な文脈でも使用可能です。
• ロケール：軽量なモジュールシステムで、仕様の階層を定義し、証明内でも様々な方法で解釈可能です。
• 強力な組み込み自動化：簡約化と後向き連鎖証明探索による。
• スレッジハンマー：ワンクリックでさらに強力な外部自動化ツールにアクセス可能。
• 反例発見ツール：実際には偽である主張を特定するため。
• 実行可能な高階仕様からのコード生成：我々は適合性テストに使用しました。

NIEの検証のために、我々はまずIsabelle/HOLの上に分離論理と呼ばれる専門言語を実装することから始めました。分離論理は、共有リソース上で動作するプログラムコードを検証するために設計されています。我々は独自の証明自動化をコーディングし、組み込みのものも使用しました。そのため、分離論理を使用できる一方で、必要に応じて平易な高階論理も使用することができました。Isabelleは、真に巨大なサブゴールに対処するのに十分な回復力と効率性を備えていることが判明しました。市販のラップトップを使用して、その25万行の証明を30分で実行することができました。

Isabelle/HOLの応用例

NIE以前のIsabelleの単一で最も印象的な応用例は、広く使用されているマイクロカーネルであるseL4の検証でしょう。この証明も最初に発表された時点で約25万行でした（現在ははるかに長くなっています）。seL4の開発者たちは、マイクロカーネルのC実装が抽象仕様を洗練させていることを証明し、コア操作の完全な機能的正確性を導き出しました。そして、検証されたコード部分ではバグは観察されていませんが、テストは未検証部分や形式化できない特定の仮定をカバーする上で依然として役割を果たしています。

Isabelleはまた、以下のプロジェクトで使用されました：

• WebAssembly言語の意味論を形式化し、エラーを特定し、特にその型システムの健全性を証明するため。
• Cogentプログラミング言語の検証フレームワークを作成するため。
• 分散編集に使用されるコンフリクトフリー複製データ型のアルゴリズムの正確性を証明するため。
• 純粋数学における数多くの結果を形式化するため。
• 抽象レベルで暗号プロトコルを検証するため。

Isabelleは無料でオープンソースであり、ダウンロード可能です。十分なメモリを搭載したあらゆるマシンの主要なオペレーティングシステム上で動作します。