seL4 kernel におけるプログラム検証の範囲と構成

まず､seL4 における形式検証の対象外となるものがいくつかある｡ seL4 は, 以下に関する幾つかの条件を仮定してコードベースの正当性を検証する｡[sel4_assumptions]

seL4カーネルの検証は､抽象的な設計レベル･ソースコードレベル･バイナリレベルの3レイヤに分割されて行われる｡ 設計レベルの抽象度に対して､ソースコード､バイナリが設計の要求を満たしているか(refinement) ^[1] を検証する｡

seL4 の設計･開発プロセスとその形式検証は密接に関わっている｡ これは､ボトムアップなアプローチをとるOS開発者とトップダウンで考える形式手法の専門家がスムーズに情報を共有しながら進まなくてはならない｡ 以下､seL4の設計開発プロセスの流れに沿って説明する｡

まず､抽象的な仕様をHaskellで記述する｡[hs_spec] ^[2] [run_spec]この記述から､Isabelleによる形式仕様へ自動的に変換することが出来る｡ また､この形式仕様を参考に手動でC言語によるカーネルの実装がされる｡

さらに､Haskellで形式仕様を書くことで､OSで開発者と形式手法専門家の間で前述の情報共有が達成される｡

また､この形式仕様は_実行でき_[run_spec]設計プロセスでのプロトタイピングの役割も果たす｡ ^[3] seL4では,これを用いて高速にプロトタイピングを行いつつ､C言語による実装を進めるといった設計開発プロセスが出来る｡ ^[4]

次に､C言語による実装が実際に前述の形式仕様の要求を満たすことを検証する｡ これは､上の形式仕様から導かれるIsabelleのコードとCのソースコードを変換したIsabelleのコード ^[5] を合わせて必要な条件を命題として立てて証明することで達成される｡

C言語からIsabelleへの変換は[c_parser]によってなされる｡ 変換器はC99の大体に対応しているが､検証に不都合な機能には対応していないこともある｡ (e.g.自動化のためローカル変数への & を許容しない([compverif], 4.3) [bytes_seplog]) 変換器は Isabelle 上で形式化された言語である Simpl[simpl]のコードに変換され ^[6] 対話的に証明することができる｡

最後に､カーネルがコンパイル･リンクされた後のバイナリがC言語による実装を適切に反映しているかを検証する｡ これも前述のC言語と抽象仕様との場合と同様に､バイナリとC言語の共通の論理的な表現に変換[bin_verif]した後に妥当性を検証する｡

バイナリの検証は､実装後の工程(e.g.コンパイル､リンク)の問題を防ぐためである｡ このような問題には､コンパイラ･リンカのバグなどがあり､バイナリを検証することでコンパイラやリンカの出力を信用しなくても良くなる｡ ^[7]

ここで取り上げた機能の正当性(functionalcorrectness)の他にも､ seL4の形式検証プロジェクトでは,マクロカーネルとしてfastpathの実装や､機密性に関する性質ついて検証しています｡ すべての証明･実装は[l4verified]と[sel4_src]で見ることが出来るので是非眺めてみてください｡