ソフトウェアの検証 成熟した方法論・ツール しかし、非常に高いコスト 人間的要因 ＞ アルゴリズム・設計・実装

Presentation on theme: "ソフトウェアの検証 成熟した方法論・ツール しかし、非常に高いコスト 人間的要因 ＞ アルゴリズム・設計・実装"— Presentation transcript:

1 ソフトウェアの検証 成熟した方法論・ツール しかし、非常に高いコスト 人間的要因 ＞ アルゴリズム・設計・実装
人間的要因　＞　アルゴリズム・設計・実装 開発方法論に部分的に埋め込むのが現実的 Lightweight verification 厳格な形式的検証は、コストが見合う分野に！ Safety critical software

2 Safety Critical Software
組み込みシステム 自動車・航空機・衛星 医療機器 制御システム プラント制御 鉄道制御 セキュリティ 認証プロトコル サーバ・クライアント スマートカード 実時間システム ハイブリッド・システム Fault-tolerant, dependable e.g., 電子商取引 リアクティブ・システム トランザクション Secure

3 検証の階層 仕様 アルゴリズム 設計 実装（ソースコード・レベル） 実装（バイトコード・レベル） 実装（機械語レベル）

4 方法論・ツール 証明支援系 状態探索系・モデル検査系 融合 高階論理・高階型理論＋帰納的定義 半自動証明＋対話的証明 証明手続き＝タクティク
状態遷移系 時相論理（離散・連続・確率） 全自動証明 静的検査を包含している。 dataflow analysis as model checking 融合

5 例：Petersonのアルゴリズム me = 0, 1 you = 1, 0 for (;;) { flags[me] = true;
turn = you; while (flags[you] == true) { if (turn != you) break; } // the critical section flags[me] = false; // the idle part

6 Petersonのアルゴリズム 0: flags[me] = true; 1: turn = you;
2: if (flags[you] != true) goto 4; 3: if (turn != you) goto 4; else goto 2; 4: critical section; 5: flags[me] = false; 6: either goto 6 or goto 0; 状態：(pc0, pc1, flags[0], flags[1], turn) pc0, pc1: 0..6 flags[0], flags[1]: {true, false} turn: {0, 1}

7 Petersonのアルゴリズムの正当性 安全性 活性（飢餓が起きないこと） 活性が成り立つためには公平性が必要 公平性（fairness）
二つのプロセスが同時にはcritical sectionに入らない。 pc0=pc1=4にはならない。 活性（飢餓が起きないこと） プロセスがヘッダ部に入ったら、 必ずいつかはcritical sectionに入ることができる。 活性が成り立つためには公平性が必要 どちらのプロセスも必ず進んでいなければならない。 ここでは，critical sectionで無限ループに陥らないと仮定。 公平性（fairness） どちらのプロセスも無限回実行される。 （unconditional fairness）

8 例：活性の検証 ヘッダ部に入ったにもかかわらず、critical sectionにいつまでたっても入れないとすると、2と3を回っているはずである。このとき、 flags[you] == true と turn == you の両条件が成り立っているはずである。こちら側が2と3を回っているとき、これらの二つの変数の値は、相手側しか変えることができない。相手方では、turn != you が成り立っているので、相手側が既に2と3を回り続けていることはない。一方、6を回りつづけているとすると、flags[me] == false となっているはずである。これは、こちら側では flags[you] == false を意味するので、これもあり得ない。従って、公平性を仮定すると、相手側は2にまで至るはずである。ところが、こちらが2と3を回っているならば、flags[me] == true のはずなので、相手側では flags[you] == true となる。従って、相手側が1を実行し2に入ると、2と3を回り続けることになる。一方、こちら側は、相手が1を実行すると、turn==me となるので4に進むことができる。これは矛盾である。

9 二つのアプローチ 証明支援系（proof assistant） 状態探索系・モデル検査系（model checker）
先のスライドのような議論を形式論理の中で行う。 主として高階論理＋帰納的定義 処理系の中で形式的な証明を構築しチェックする。 半自動的な証明機能（タクティク） 状態探索系・モデル検査系（model checker） 有限個の状態を機械的に網羅し、 活性を破るような無限経路がないことを確認する。 状態：(pc0, pc1, flags[0], flags[1], turn) 状態の網羅⇒有限の状態遷移系（グラフ） 無限経路＝グラフ上のループ 状態遷移系を記述する言語 ⇒ プロセス代数など 状態遷移系の性質を記述する言語 ⇒ 時相論理

10 時相論理（Temporal Logic） 状態の遷移や時間の経過の観点より システムの性質を記述するための論理体系 線形時間時相論理
LTL（Linear Time Temporal Logic) 分岐時間時相論理 CTL（Computation Tree Logic） μ計算（m-Ｃａｌｃｕｌｕｓ） モデル検査 時相論理で表現された性質を システムが満たすかどうかを検査すること

11 Petersonのアルゴリズムの正当性の 時相論理による表現
安全性 LTL（Linear Time Temporal Logic) G(￢(pc0=4 ∧ pc1=4)) CTL（Computation Tree Logic） AG(￢(pc0=4 ∧ pc1=4)) 活性（飢餓が起きないこと） LTL G(pc0=0 ⇒ F(pc0=4)) CTL AG(pc0=0 ⇒ AF(pc0=4)) 公平性（fairness） LTL G(pc0=0 ⇒ F(pc0=1)) ∧ ... LTLならば書けるが、CTLでは書けない。

12 証明支援系 HOL 高階論理 Isabelle 高階論理, 集合論, … PVS 高階論理, 依存型 Coq 高階型理論
上記のシステムに共通の機構 高階論理（higher-order logic） 帰納的定義（inductive definition） データ型 述語 ACL2 Boyer-Moore

13 状態探索系・モデル検査系 SMV CTL, BDD SPIN LTL, Promela Murf 状態探索 FDR CSP
SAL PVSの記号モデル検査系 HyTech 時間オートマトン Uppaal 時間オートマトン Kronos 時間オートマトン PRISM 確率オートマトン

14 事例 分散アルゴリズム 認証プロトコル JavaとJavaCard 実時間システム 仕様・アルゴリズム 仕様・アルゴリズム・設計
実装（ソースコード・レベル） 実装(バイトコード・レベル） 実時間システム

15 分散アルゴリズム 事例：Byzantine General 仮定：Oral Message SRIのPVSによる有名なケース・スタディ
将軍も含めて裏切り者がいるかもしれない。 裏切っていない隊長たちがコンセンサスを得る。 仮定：Oral Message 故障していないプロセッサ間の通信は信頼できる。 メッセージの受信者は送信者を特定できる。 メッセージの消失を検知できる。

16 Byzantine General OMBG(0) 将軍はすべての隊長に命令を送る。 各隊長は、命令を受信すればそれを用いる。
命令を受信しなければ「退却」を用いる。 OMBG(m), m>0 隊長iは、命令を受信すればそれをviとする。 命令を受信しなければ「退却」をviとする。 隊長iは、他のn-2人の隊長に対して、 将軍となってOMBG(m-1)を実行する。 ステップ2でOMBG(m-1)の実行により 隊長j（j≠i）から受信した命令をvjとする。 命令を受信しなければ「退却」 をvjとする。 隊長iは、v1,…,vn-1で多数決を行い、その結果を用いる。

17 OMBG(m)の性質 裏切り者の数が高々kで、n>2k+mのとき、 将軍が裏切り者でなければ、
裏切り者でない隊長は将軍の命令を用いる。 裏切り者の数が高々mで、n>3mのとき、 裏切り者でない隊長は同じ命令を用いる。 形式的証明：10年以上の長い歴史 Boyer-Moore, EHDM, PVS, …（証明支援系） 後の形式的証明へ継承 Byzantine fault-tolerant clock synchronization TTA（Time Triggered Architecture）

18 モデル検査 一方、モデル検査においても、 分散アルゴリズムは重要な対象。 例えば、SPINのIEEE/SEの論文には、
Process scheduling algorithm Leader election algorithm Sliding window protocol ただし、有限モデルに制限する必要がある。 もしくは、適切な抽象化による 抽象モデル検査を行う。

19 認証プロトコルの検証 各種方法論の競演（古館伊知郎風に言えば） 様相論理 状態探索・モデル検査 ⇒ アタックの発見 論理プログラミング
FDR, Murf 論理プログラミング 帰納的定義と証明支援系 ⇒ 形式的証明 Isabelle 多重集合書き換え 静的検査（型とeffect） ストランド空間 ⇒ 数学的証明 Athena（専用の自動証明系）

20 Needham-Schroeder公開鍵プロトコル
{NB , B}KA A B {NB, NA}KB {NA}KA

21 C A B C Loweのアタック {NB , B}KA {NB , B}KC {NB, NA}KB {NB, NA}KB {NA}KA
{NA}KC

22 Loweのアタック Bが不用意に信頼できない主体Cと プロトコルを開始してしまう。 Aは、Bと通信していると信じている。
Loweは、FDRを用いてこのようなアタックの 存在を発見したとされている。 実は、その前に手作業で発見していた。

23 Javaの形式化と検証 ここでも各種方法論の競演 証明支援系 静的解析 … 型システム 時相論理 モデル検査 … バイトコードのモデル検査
Isabelle, ACL2, … Java言語の操作的意味論・型システム・コンパイラ インヘリタンス、インタフェース 静的解析 … 型システム JVM言語の型システム サブルーチン、オブジェクト初期化、クラスローダ Java言語のソースコードの静的検査 ESC/Java 時相論理 セキュリティ・マネージャの形式化 モデル検査 … バイトコードのモデル検査

24 JavaCardの形式化と検証 Javaの形式化と検証に加えて ヨーロッパのプロジェクト 証明支援系 VerifiCard
University of Nijmegen, The Netherlands (Coordination) INRIA, France Technical University of Munich, Germany University of Kaiserslautern, Germany Swedish Institute of Computer Science, Sweden SchlumbergerSema INRIAの旧プロジェクト 証明支援系 JCVMの形式化 CertiCarte Coq Offensive and Defensive Virtual Machine ByteCode Verifier コンテキスト・スイッチ

25 JavaCardの形式化と検証 仕様記述言語 JaKarTaプロジェクト LOOPプロジェクト CertiCarteから発展
JSL（JaKarTa Specification Langauage） JMLに発展したのか？ LOOPプロジェクト JML（Java Modeling Language） Hoare論理の再来 Proof obligationをPVSもしくはIsabelleへ変換 APIの仕様記述と検証 AbstractCollection AID JCSystem ファイアウォール、トランザクション、トランジェント・オブジェクト Transacted memory

26 JavaCardの形式化と検証 事例：電子財布 Gemplus Multi-appletアプリケーション ESC/Javaによる静的検査
共有オブジェクトによる通信 Purse Deposit Debit Loyalty 「ポイント・カード」 ESC/Javaによる静的検査 JML

27 実時間システム 事例：Byzantine clock synchronization
各プロセスは、すべてのプロセスのクロックの値を読み込み、自分のクロックをそれらの値の平均にセットする。ただし、平均を計算する際には、自分のクロック値に対してδより大きくずれているクロック値は無視して、その代わりに自分のクロック値を用いる。 形式的証明：やはり10年以上の長い歴史 EHDM, PVS, …（証明支援系） TTAなどの基礎

28 時間オートマトンのモデル検査 一方、モデル検査においても、 実時間システムの検証技術の研究が活発。 様々な実時間システム
時間オートマトン（timed automaton） ハイブリッド・オートマトン（hybrid automaton） 時間ペトリネット 時間付き多重集合書き換え 実時間を扱う時相論理 TCTL 多くのモデル検査系

29 時間オートマトン 離散的な制御＋連続的な時間経過 エッジによる遷移＋時間経過による遷移 クロック変数：x, y, z, ...
A x  2 C B エッジによる遷移＋時間経過による遷移 クロック変数：x, y, z, ... ロケーションとエッジに対する制約 クロック値はユニフォームの増加する。 エッジによる遷移の際に 指定されたクロック変数がリセットされる。

30 事例：Uppaalから Bang & Olufsen Audio/Video Protocol
Bang & Olufsen Power Down Protocol Bounded Retransmission Protocol Collision Avoidance Protocol Gearbox Controller LEGOｮ MINDSTROMSTM Systems - Control Program Synthesis LEGOｮ MINDSTROMSTM Systems - Verification of RCXTM Systems Lip Synchronization Algorithm Multimedia Stream Mutual Exclusion Protocol Philips Audio Protocol Philips Audio Protocol with Bus Collision TDMA Protocol Start-Up Mechanism