プログラミング言語とソフトウェアの信頼性

• 信頼性の高いソフトウェアを提供したい
• ソフトウェアの仕様を検証するには二つの手法がある
  • プログラムの持つ状態を数え上げ、仕様から外れた状態が無いかを確認するモデル検査
  • プログラムの性質を直接証明してしまう定理証明
• モデル検査も証明も行ないやすい言語として 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る
• 赤黒木の挿入を証明する