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

形式検証アドベントカレンダー 1 日目の記事です｡ 形式検証された OS である seL4 の検証アプローチに関する話です｡ 使われているツールの詳細にはあまり踏み込まず全体的な指針をまとめたものです｡

以下の記述は概ね¹に基づいているので詳しくはそちらを読んでください｡

seL4 が検証しないもの

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

1. アセンブリ言語で書かれたコードベース
2. ハードウェア
3. 起動処理
4. 仮想メモリ
5. DMA
6. サイドチャネル攻撃による情報漏えい

seL4 verification architecture

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

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

runnable abstract specification

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

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

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

c refinement proof

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

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

binary verification

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

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

おわりに

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