形式検証

形式検証とは、システムやプログラムが仕様を満たすことを、有限個のテストによる確認ではなく、数学的論理に基づく証明によって示す検証手法であり、定理証明やモデル検査などの技法を用いて対象の振る舞いを仕様に対して網羅的に保証するものである。

詳細解説

テストが「選んだ入力に対して期待どおり動くこと」を確かめる手法であるのに対し、形式検証は対象を数学的な対象（論理式・状態遷移系など）としてモデル化し、仕様を満たすことを証明する。代表的な技法には、証明支援系（Isabelle/HOL等）の上で人が証明を構築する定理証明と、有限の状態空間を自動探索するモデル検査がある。OSカーネルの seL4 に対する機能正当性の証明（Klein et al., SOSP 2009）は、実用システムへの定理証明の適用例として広く知られる。

重要なのは、証明が仕様と前提に相対的であることだ。仕様そのものが誤っていれば「誤った仕様を満たすこと」が証明されるだけであり、前提（ハードウェアの正しさ等）の欠陥も保証範囲外になる。seL4が証明の仮定（アセンブリコード・ブートコード・マシンインターフェース・ハードウェア・DMA）を公式に列挙しているのは、この相対性の誠実な明示である。

SDVにおける位置づけ

ソフトウェアが安全機能を担うSDVでは、「テストでは尽くせない振る舞いの保証」への需要が大きく、分離カーネル（マイクロカーネル）の隔離保証のような土台部分で形式検証の価値が際立つ。一方で証明の範囲と前提を正確に理解せず「検証済み＝安全」と扱うことは、かえってリスクを生む。