title: メタ計算を用いた Continuation based C の検証手法 author: Yasutaka Higa profile: lang: Japanese # プログラミング言語とソフトウェアの信頼性 * 信頼性の高いソフトウェアを提供したい * ソフトウェアの仕様を検証するには二つの手法がある * プログラムの持つ状態を数え上げ、仕様から外れた状態が無いかを確認するモデル検査 * プログラムの性質を直接証明してしまう定理証明 * モデル検査も証明も行ないやすい言語として Continuation based C 言語を開発している # 二つのアプローチを用いたソフトウェア検証 * モデル検査的アプローチ * メタ計算ライブラリ akasha による網羅的な実行 * 非破壊赤黒木の仕様定義と検証 * 定理証明的なアプローチ * 依存型を持つ証明支援系言語 Agda による CbC の証明 * 部分型を利用して Agda 上に型付きの CbC の項を記述する * 型システムを通して CbC の形式的な定義を得る * SingleLinkedStack の性質の証明 # Continuation based C * 当研究室で開発しているプログラミング言語 * アセンブラとC言語の中間のような言語であり、構文はほとんど C 言語 * OS や組み込みソフトウェアなどを対象にしている * CodeSegment と DataSegment という単位を用いてプログラミングする # CodeSegment * CodeSegment とは * 処理の単位 * 結合や分割が容易 * 入力と出力を持つ * CodeSegment どうしを接続することによりプログラム全体を作る * TODO: 図 # DataSegment * DataSegment とは * データの単位 * CodeSegment の入出力にあたる * 接続元の Output DataSegment は接続先の Input DataSegment * TODO: 図 # メタ計算 * とある計算を実現するための計算 * ネットワーク接続、例外処理、メモリ確保、並列処理など * 時に本来行ないたい処理よりも複雑になる * CbC は通常レベルの計算とメタ計算を分離して考える * 通常レベルではポインタは出てこない、など * TODO: 図 # Meta CodeSegment * メタ計算を行なう CodeSegment * 通常の CodeSegment どうしの接続の間に入る * TODO: 図 # Meta DataSegment * メタ計算用の DataSegment * 通常の DataSegment を含むような DataSegment * TODO: 図 # C言語との対応 * CodeSegment は C 言語における返り値の無い関数 * DataSegment は C 言語における構造体 * Meta CodeSegment は CodeSegment の前後にある CodeSegment * Meta DataSegment は全ての DataSegment の共用体を持つ構造体 * CodeSegment の接続は goto における軽量継続 * 末尾のみで行なうスタックを保持しない関数呼び出し # 並列に信頼性高く動作する GearsOS * CbC を用いたメタ計算の例として本研究室で開発している GearsOS がある * 並列実行やモデル検査をメタ計算として提供する * 現在はメモリ管理、Synchronized Queue、非破壊赤黒木などが実装済み * 今回はこの非破壊赤黒木の検証を行なう # 赤黒木 * データの保存に用いる二分木 * 特に赤黒木はノードが持つ赤か黒の色を使って木のバランスを取る * ルートノードと葉ノードの色は黒 * 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことは無い) * ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定 * TODO: 図 # GearsOS における赤黒木の利用例(ノードの挿入) * 挿入したい要素を DataSegment に格納して次の CodeSegment へ goto * goto する前に Meta CodeSegment が実行されて木に挿入する * GearsOS では木の実装のためにスタックを用いて経路情報を保持している * TODO: 図 # 仕様の記述とその確認 * 「バランスが取れている」とは何かを表現できる必要がある * 実行可能な CbC の式を使った assert になる * そしてそれを保証したい * プログラムの全ての状態においてこれは常に成り立つのか? # 既存のモデル検査器 spin * spin * promela と呼ばれる言語でプログラムを記述 * 並列に動作するプログラムの仕様を検証可能 * 検証した promela から実行可能な C ソースを生成可能 * 仕様は bool になる式を用いた assert * promela は C とは記述が異なる # 既存のモデル検査器 CBMC * CBMC * 検証対象のCソースを変更しないでも良い * C/C++ 言語の記号実行が可能 * 条件分岐を網羅的に実行 * 仕様は bool になる式を用いた assert * 有限ステップ検証する有界モデル検査器 # メタ計算ライブラリ akasha * メタ計算としてプログラムの状態を数え上げる * goto された時に挿入される要素の組み合わせを全て列挙して実行する * その度に仕様の式は成り立つかをチェックする * TODO: 図 # チェックする仕様 * TODO: たかさについて # akasha と CBMC の比較 * akasha は有限の要素数の組み合わせをチェックする * 要素数が13個までならどの順で木に挿入しても良い * 比較対象として C Bounded Model Checker を使用した * C/C++ の記号実行を行なう * 実行可能なステップ数411だけ展開しても仕様は満たされる * が、恣意的にバグを入れ込んでも反例を返さない * akasha は返した * 固定の要素数までの仕様検査で十分なのか? # 定理証明 * 任意の回数だけ木の操作を行なっても大丈夫なことを保証したい * そのままプログラムの性質を保証してやる * プログラムと証明は Curry-Howard Isomorphism により、自然演繹と型付ラムダ計算が対応 * プログラムにおける命題は型であり、証明はその導出が存在するかどうか * 例えば三段論法が書ける * (A -> B) -> (B -> C) -> (A -> C) * (int -> bool) -> (bool -> float) -> (int -> float) # 証明支援系 Agda * 依存型を持つ言語 * 型が第一級(型が値である) * 「型を取って型を返す型」などが定義可能 * 定理証明が記述可能 * この言語の上に CbC の項を表現する * Agda 経由で CbC の形式的な定義を得る # Agda 上に CbC を記述するには? * CbC と CbC の対応で書ける? * DataSegment -> 構造体(複数の値と名前によって成り立つ) * CodeSegment -> 関数型(型を取って型を返す) * Meta DataSegment -> 構造体の共用体 * Meta CodeSegment -> 関数型? * Meta CodeSegment の階層構造をどう定義するか * 構造体に相当するレコード型はAgdaにある * 共用体に相当する直和型も定義可能 # メタレベルの型付け * Meta CodeSegment が持っているべき性質 * メタレベルは階層構造を持つ * メタ計算は組み合わせられる * ノーマルレベルの DataSegment を一様に扱える * ノーマルレベルの CodeSegment へと goto できる * どんなプログラムからもライブラリとして使える * 構造体では融通が効かない * 完全にマッチしなくてはいけない * TODO: ソース # 部分型 * DataSegment が持つべき制約を表現できる型 * 型 T が期待される文脈で S を用いても良い、というようなことができる * 「S <: T」で「S は T の部分型である」と読む * 全てのDataSegment に対して「MDS <: DS」となるような MDS を用意する * DataSegment X が期待される CodeSegment に Meta DataSegment を渡してやる # 入力の部分型 # 出力の部分型 # 部分型で何ができたか? * Meta CodeSegment を部分型とすることで * ノーマルレベルの CodeSegment の前後に処理を入れても型は整合する * Meta CodeSegment を CodeSegment とすることで階層構造を作れる * Meta DataSegment を部分型とすることで * ノーマルレベルからはアクセスできないデータを保持してもOK * ノーマルレベルに Meta DataSegment を渡しても良い * こちらも階層構造を取ることができる # SingleLinkedStack の証明 * 証明支援系 Agda に GearsOS のデータ構造 SingleLinkedStack を定義 * スタックは赤黒木に用いられている * その性質を証明する * 性質もいくつか考えられる * 「push して pop するとスタックは元に戻る」 # Agda を用いた証明手法 * 基本的にはデータの構造に関する帰納法 * スタックは内部に SingleLinkedList を持つ * SingleLinkedList は NULL か値と次のノードを持つ * 値がある場合と無い場合との場合分け * 挿入する要素を指定せずに push を呼ぶとどうなるのか? * 実装依存のコード * 証明には表れる * TODO: かく... # まとめ * Continuation based C 言語を対象にした二種類の検証アプローチ * モデル検査的なアプローチ * 継続を上書きして可能な状態を数え上げるメタ計算ライブラリ akasha を実装 * 有限の要素数まで保証できた * 証明的なアプローチ * 証明支援系 Agda 上で CbC のプログラムを定義して直接証明 * 部分型を利用して CbC を型付け * データ構造 SingleLinkedStack の証明ができた # 今後の課題 * 部分型を利用してCbCを型付け * 依存型をCbC に導入して自身を証明可能にする * 型情報から stub を自動生成すkる * 赤黒木の挿入を証明する