証明が約束できること

ソフトウェアが信頼されるのは、たいていテストされたからです。誰かがうまくいかなくなりそうな場面を考え、試し、切り抜けるのを確かめました。この方法はよく機能します。誰も思いつかなかった場合に行き当たるまでは。

証明は反対側から始めます。場合を試すのではありません。ある命題がすべての場合に成り立つことを、数学によって示します。

試した場合ではなく、すべての場合

小さな約束を例にとりましょう。「このコードは、バッファの終わりを越えて読むことがない」。テストは千個の入力、あるいは十億個の入力を与えて、どれもコードを壊さなかったと報告できます。証明が述べるのは、種類の違うことです。コードを壊す入力は存在しない。見つからなかったのではなく、ないのです。

その代償は厳密さです。証明には、コードが何をすべきかを正確に述べたもの、つまり仕様と、コードの一行一行を仕様に結びつける論証が必要です。現実のソフトウェアでは、その論証は人が目で確かめるには長すぎます。そこで、コンピュータが検査します。

機械による検査

「機械検査された」とは、そういう意味です。証明は、証明支援系と呼ばれるプログラムが読める言語で、省略なしに書き下されます。そしてそのプログラムが、一つひとつのステップを論理の規則に照らして検査します。九百ページ目で疲れることはなく、誰の言葉も鵜呑みにしません。

seL4の証明は、Isabelle/HOLという証明支援系で、このように検査されています。証明は公開されており、誰でももう一度実行できます。

seL4の証明が述べていること

seL4は、すべてのNoWayOSシステムがその上で動くカーネルです。約10,000行のコードであり、デバイスを完全に制御できる唯一のコードです。要点はその小ささにあります。一万行についての論証は、最後までやり遂げられます。数千万行についての論証は、まだできません。

seL4 Foundationは、これらの証明を層に分けて説明しています。

• コードは仕様のとおりに動作し、それ以上のことはしません。 そこから、カーネルにはできないことの一覧が導かれます。バッファをあふれさせること、ヌルポインタをたどること、メモリをリークすること、ゼロで割ること。
• 実際に動くプログラムは、証明されたコードと一致します。 両者の間にはコンパイラがあるので、その出力を別の証明が検査します。
• カーネルは、システムの各部分を分離しておけます。 ある部分は、権利を付与されていないかぎり、別の部分のデータを変更することも、読むことも、必要とする資源を奪うこともできません。
• システムは、設計されたとおりの状態で起動できます。 その記述に挙げられた付与と、ちょうど同じ付与を持って。

すべての層が、すべてのプロセッサ、すべての構成について完了しているわけではありません。これは重要な点で、後でもう一度触れます。

証明が前提とするもの

証明の広さは、その命題の広さとちょうど同じで、証明は前提の上に立っています。seL4は自らの前提を書き出しています。ハードウェアがそのモデルのとおりに振る舞うこと、最も低いレベルの数百行のコードが正しいこと、カーネルの起動前に動くコードが役目を果たしていること。機密性の証明は、タイミングを対象としていません。

証明は、仕様が正しいことを求めているかどうかについては何も述べず、カーネルより上のソフトウェアについても何も述べません。証明されたカーネルは、バグのあるプログラムも忠実に隔離します。バグはそこに残っています。ただ、ほかの何にも届かないだけです。

これは証明の弱点ではありません。証明に価値がある理由です。何を対象とするかを正確に述べるので、何が残っているかを正確に知ることができます。

NoWayOSの立ち位置

率直に申し上げます。NoWayOSはseL4の上で動きますが、現時点で、seL4の完了済みの証明の範囲に入るNoWayOSイメージはありません。NoWayOSが使うのはseL4の混合クリティカリティ構成で、私たちのプロセッサ向けの証明は進行中です。そして、seL4の証明がNoWayOS自身のコードを対象としたことは、一度もありません。ですから、私たちはNoWayOSを“形式検証済み”とは呼びませんし、これからも呼びません。

どのイメージも、自分の立ち位置を示します。イメージの横に置かれるファイルが、カーネルの構成を、seL4が証明した構成と並べて、オプションごとに記載します。セキュリティのページに、実物があります。

私たち自身の、小さな証明

NoWayOSのコードは、別の方法で保証を得ています。Rust、隔離、レビュー、テスト、そしてもっと控えめな種類の証明です。

システムの部分どうしがやり取りするメッセージのデコーダには、すべて有界証明があります。Kaniというモデル検査器で作ったものです。有界証明は、定められた大きさまでのすべての入力を対象とします。ここでは、デコーダが受け付ける最長のレコードまでです。その範囲の中では、本物の証明です。どんな入力も、デコーダをパニックさせず、オーバーフローさせず、境界外を読ませません。範囲の外については何も述べません。だからこそ、範囲を、ありうる最長の入力に合わせてあります。

そのうえで、私たちはデコーダをわざと壊し、証明がそれに気づくことを確かめます。失敗できない証明は、失敗できないテストより優れているわけではありません。

等身大の姿

証明は、何かを“ハッキング不可能”にするものではありません。証明は、一つの命題を、すべての場合に、読むことのできる前提のもとで、真にします。命題と前提を知れば、自分が何を手にしているかがわかります。

だからNoWayOSは、その証明を持つカーネルの上に作られています。そして、証明がどこまで届いているかを、イメージごとにお伝えします。