抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証

ソフトウェアの検証
• 成熟した方法論・ツール
• しかし、非常に高いコスト
• 人間的要因＞アルゴリズム・設計・実装
• 開発方法論に部分的に埋め込むのが現実的
– Lightweight verification
• 厳格な形式的検証は、コストが見合う分野
に！
– Safety critical software
Safety Critical Software
• 組み込みシステム
– 自動車・航空機・衛星
– 医療機器
• 制御システム
– プラント制御
– 鉄道制御
実時間システム
ハイブリッド・システム
Fault-tolerant, dependable
e.g., 電子商取引
• セキュリティ
– 認証プロトコル
– サーバ・クライアント
– スマートカード
リアクティブ・システム
トランザクション
Secure
検証の階層
•
•
•
•
•
•
仕様
アルゴリズム
設計
実装（ソースコード・レベル）
実装（バイトコード・レベル）
実装（機械語レベル）
方法論・ツール
• 証明支援系
– 高階論理・高階型理論＋帰納的定義
– 半自動証明＋対話的証明
– 証明手続き＝タクティク
• 状態探索系・モデル検査系
– 状態遷移系
– 時相論理（離散・連続・確率）
– 全自動証明
– 静的検査を包含している。
• dataflow analysis as model checking
• 融合
例：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
}
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}
Petersonのアルゴリズムの正当性
• 安全性
二つのプロセスが同時にはcritical sectionに入らない。
pc0=pc1=4にはならない。
• 活性（飢餓が起きないこと）
プロセスがヘッダ部に入ったら、
必ずいつかはcritical sectionに入ることができる。
• 活性が成り立つためには公平性が必要
どちらのプロセスも必ず進んでいなければならない。
ここでは，critical sectionで無限ループに陥らないと仮定。
• 公平性（fairness）
どちらのプロセスも無限回実行される。
（unconditional fairness）
例：活性の検証
• ヘッダ部に入ったにもかかわらず、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に進むことができ
る。これは矛盾である。
二つのアプローチ
• 証明支援系（proof assistant）
– 先のスライドのような議論を形式論理の中で行う。
• 主として高階論理＋帰納的定義
– 処理系の中で形式的な証明を構築しチェックする。
– 半自動的な証明機能（タクティク）
• 状態探索系・モデル検査系（model checker）
– 有限個の状態を機械的に網羅し、
活性を破るような無限経路がないことを確認する。
• 状態：(pc0, pc1, flags[0], flags[1], turn)
–
–
–
–
状態の網羅⇒有限の状態遷移系（グラフ）
無限経路＝グラフ上のループ
状態遷移系を記述する言語 ⇒ プロセス代数など
状態遷移系の性質を記述する言語 ⇒ 時相論理
時相論理（Temporal Logic）
• 状態の遷移や時間の経過の観点より
システムの性質を記述するための論理体系
• 線形時間時相論理
– LTL（Linear Time Temporal Logic)
• 分岐時間時相論理
– CTL（Computation Tree Logic）
– μ計算（m-Ｃａｌｃｕｌｕｓ）
• モデル検査
– 時相論理で表現された性質を
システムが満たすかどうかを検査すること
Petersonのアルゴリズムの正当性の
時相論理による表現
• 安全性
– LTL（Linear Time Temporal Logic)
G(￢(pc0=4 ∧ pc1=4))
– CTL（Computation Tree Logic）
AG(￢(pc0=4 ∧ pc1=4))
• 活性（飢餓が起きないこと）
– LTL
– CTL
G(pc0=0 ⇒ F(pc0=4))
AG(pc0=0 ⇒ AF(pc0=4))
• 公平性（fairness）
– LTL
G(pc0=0 ⇒ F(pc0=1)) ∧ ...
– LTLならば書けるが、CTLでは書けない。
証明支援系
•
•
•
•
•
HOL
高階論理
Isabelle
高階論理, 集合論, …
PVS
高階論理, 依存型
Coq
高階型理論
上記のシステムに共通の機構
– 高階論理（higher-order logic）
– 帰納的定義（inductive definition）
• データ型
• 述語
• ACL2
Boyer-Moore
状態探索系・モデル検査系
•
•
•
•
•
•
•
•
•
SMV
SPIN
Murf
FDR
SAL
HyTech
Uppaal
Kronos
PRISM
CTL, BDD
LTL, Promela
状態探索
CSP
PVSの記号モデル検査系
時間オートマトン
時間オートマトン
時間オートマトン
確率オートマトン
事例
• 分散アルゴリズム
– 仕様・アルゴリズム
• 認証プロトコル
– 仕様・アルゴリズム
• JavaとJavaCard
– 仕様・アルゴリズム・設計
– 実装（ソースコード・レベル）
– 実装(バイトコード・レベル）
• 実時間システム
– 仕様・アルゴリズム・設計
分散アルゴリズム
• 事例：Byzantine General
– SRIのPVSによる有名なケース・スタディ
– 将軍とn-1人の隊長
– 将軍も含めて裏切り者がいるかもしれない。
– 裏切っていない隊長たちがコンセンサスを得る。
• 仮定：Oral Message
– 故障していないプロセッサ間の通信は信頼できる。
– メッセージの受信者は送信者を特定できる。
– メッセージの消失を検知できる。
Byzantine General
OMBG(0)
•
将軍はすべての隊長に命令を送る。
•
各隊長は、命令を受信すればそれを用いる。
命令を受信しなければ「退却」を用いる。
OMBG(m), m>0
1. 将軍はすべての隊長に命令を送る。
2. 隊長iは、命令を受信すればそれをviとする。
命令を受信しなければ「退却」をviとする。
隊長iは、他のn-2人の隊長に対して、
将軍となってOMBG(m-1)を実行する。
3. ステップ2でOMBG(m-1)の実行により
隊長j（j≠i）から受信した命令をvjとする。
命令を受信しなければ「退却」をvjとする。
隊長iは、v1,…,vn-1で多数決を行い、その結果を用いる。
OMBG(m)の性質
• 裏切り者の数が高々kで、n>2k+mのとき、
将軍が裏切り者でなければ、
裏切り者でない隊長は将軍の命令を用いる。
• 裏切り者の数が高々mで、n>3mのとき、
裏切り者でない隊長は同じ命令を用いる。
• 形式的証明：10年以上の長い歴史
– Boyer-Moore, EHDM, PVS, …（証明支援系）
• 後の形式的証明へ継承
– Byzantine fault-tolerant clock synchronization
– TTA（Time Triggered Architecture）
モデル検査
• 一方、モデル検査においても、
分散アルゴリズムは重要な対象。
• 例えば、SPINのIEEE/SEの論文には、
– Process scheduling algorithm
– Leader election algorithm
– Sliding window protocol
• ただし、有限モデルに制限する必要がある。
– もしくは、適切な抽象化による
抽象モデル検査を行う。
認証プロトコルの検証
• 各種方法論の競演（古館伊知郎風に言えば）
– 様相論理
– 状態探索・モデル検査 ⇒ アタックの発見
• FDR, Murf
– 論理プログラミング
– 帰納的定義と証明支援系 ⇒ 形式的証明
• Isabelle
– 多重集合書き換え
– 静的検査（型とeffect）
– ストランド空間 ⇒ 数学的証明
• Athena（専用の自動証明系）
Needham-Schroeder公開鍵プロトコル
{NB , B}KA
A
{NB, NA}KB
{NA}KA
B
Loweのアタック
{NB , B}KA
A
C
{NB, NA}KB
{NA}KA
{NB , B}KC
{NB, NA}KB
C
{NA}KC
B
Loweのアタック
• Bが不用意に信頼できない主体Cと
プロトコルを開始してしまう。
• Aは、Bと通信していると信じている。
• しかし、ノンスはCに漏洩してしまっている。
• Loweは、FDRを用いてこのようなアタックの
存在を発見したとされている。
• 実は、その前に手作業で発見していた。
Javaの形式化と検証
• ここでも各種方法論の競演
• 証明支援系
– Isabelle, ACL2, …
– Java言語の操作的意味論・型システム・コンパイラ
• インヘリタンス、インタフェース
• 静的解析 … 型システム
– JVM言語の型システム
• サブルーチン、オブジェクト初期化、クラスローダ
– Java言語のソースコードの静的検査
• ESC/Java
• 時相論理
– セキュリティ・マネージャの形式化
• モデル検査 … バイトコードのモデル検査
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
コンテキスト・スイッチ
JavaCardの形式化と検証
• 仕様記述言語
– JaKarTaプロジェクト
• CertiCarteから発展
• JSL（JaKarTa Specification Langauage）
– JMLに発展したのか？
– LOOPSプロジェクト
•
•
•
•
JML（Java Modeling Language）
Hoare論理の再来
Proof obligationをPVSもしくはIsabelleへ変換
APIの仕様記述と検証
– AbstractCollection
– AID
– JCSystem
» ファイアウォール、トランザクション、トランジェント・オブジェクト
• Transacted memory
JavaCardの形式化と検証
• 事例：電子財布
– Gemplus
– Multi-appletアプリケーション
• 共有オブジェクトによる通信
• Purse
– Deposit
– Debit
• Loyalty
– 「ポイント・カード」
– ESC/Javaによる静的検査
– JML?
実時間システム
• 事例：Byzantine clock synchronization
各プロセスは、すべてのプロセスのクロックの
値を読み込み、自分のクロックをそれらの値
の平均にセットする。ただし、平均を計算する
際には、自分のクロック値に対してδより大き
くずれているクロック値は無視して、その代わ
りに自分のクロック値を用いる。
• 形式的証明：やはり10年以上の長い歴史
– EHDM, PVS, …（証明支援系）
• TTAなどの基礎
時間オートマトンのモデル検査
• 一方、モデル検査においても、
実時間システムの検証技術の研究が活発。
• 様々な実時間システム
– 時間オートマトン（timed automaton）
– ハイブリッド・オートマトン（hybrid automaton）
– 時間ペトリネット
– 時間付き多重集合書き換え
• 実時間を扱う時相論理
– TCTL
• 多くのモデル検査系
時間オートマトン
離散的な制御＋連続的な時間経過
A
x2
B
x>1
x := 0
エッジによる遷移＋時間経過による遷移
• クロック変数：x, y, z, ...
• ロケーションとエッジに対する制約
• クロック値はユニフォームの増加する。
• エッジによる遷移の際に
指定されたクロック変数がリセットされる。
C
事例：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

Download Report