自動証明・検証技術 論理（基礎） 検証技術 対象（応用） 計算システムの「正しさ」を 保証する理論や技術

Presentation on theme: "自動証明・検証技術 論理（基礎） 検証技術 対象（応用） 計算システムの「正しさ」を 保証する理論や技術"— Presentation transcript:

1 自動証明・検証技術 論理（基礎） 検証技術 対象（応用） 計算システムの「正しさ」を 保証する理論や技術
高階述語論理、ロジカル・フレームワーク 時相論理 検証技術 証明支援系 モデル検査系 対象（応用） ハードウェア プロトコル（セキュリティ関連を含む） ソフトウェア・アルゴリズム（特に並列・分散） プログラミング言語（例えばコンパイラ） 計算システムの「正しさ」を 保証する理論や技術

2 論理（基礎） 高階述語論理 ロジカル・フレームワーク ∀f. --- 任意の関数 f について… 関数や述語に関する量化（∀∃）が可能な論理
型付きλ計算 カリー・ハワードの対応に従って、 証明をλ項で表現する。 依存型（dependent type）があると、 高階述語論理を表現することができる。 様々な論理を表現する枠組　論理の論理

3 カリー・ハワードの対応 命題 … 型 A⊃B … A→B AならばB … AからBへの関数の型 命題Aの証明 … Aを型として持つ項
構成的な証明の考えに基づいている。 直観主義論理

4 依存型 int[n]を大きさnの整数の配列の型とする。 例えば、非負整数nをもらって、 大きさnの整数の配列を返す関数の型？
int→int[n] … nが浮いている。 Πn:int. int[n] … 関数をタプルと考えると自然。 カリー・ハワードの対応では、 ∀n:int. int[n] に対応する。 依存関数型（依存直積） 依存直和: Σn:int. int[n] … ∃n:int. int[n]

5 帰納的定義 多くの証明支援系には、 帰納的定義によって論理を拡張する機能が 備わっている。 型の帰納的定義 … 再帰的データ型
述語の帰納的定義 カリー・ハワードの対応のもとでは同じ原理

6 再帰的データ型 自然数 Oは自然数である。 xが(既に作られた)自然数ならば、 s(x)も自然数である。 以上のようにして作られるもののみが
datatype NAT = O | s of NAT; ML load "Datatype"; open Datatype; Hol_datatype `NAT = O | s of NAT`; HOL

7 再帰的データ型 自然数を葉に持つ二分木 datatype BINTREE = leaf of NAT
| cons of BINTREE*BINTREE; ML Hol_datatype `BINTREE = | cons of BINTREE=>BINTREE`; HOL

8 述語の帰納的定義 even(x)の定義 even(O)が成り立つ。 even(x)が成り立てば、 even(s(s(x)))も成り立つ。
load "IndDefLib"; open IndDefLib; new_simple_inductive_definition [ ``T ==> even O``, ``even x　==> even (s (s x))``]; HOL

9 帰納的述語の証明 even(x)の証明 even1の型は、 Πx:NAT. even(x) → even(s(s(x)))
even0はeven(O)の証明である。 Xがeven(x)の証明ならば、 even1(x, X) – より正確にはeven1(x)(X) – は、 even(s(s(x)))の証明である。 以上のようにして作られるもののみが、 even(x)の証明である。 even1の型は、 Πx:NAT. even(x) → even(s(s(x)))

10 再帰的データの構成に関する帰納法 P(x)を自然数に関する述語とする。 任意の自然数xに対してP(x)が成り立つ。
P(O)が成り立ち、 任意の自然数xに対して、 P(x)ならばP(s(x))が成り立てば、 任意の自然数xに対してP(x)が成り立つ。 P(x)を二分木xに関する述語とする。 任意の自然数iに対してP(leaf(i))が成り立ち、 二分木xとyに対してP(x)かつP(y)ならば P(cons(x,y))も成り立てば、 任意の二分木xに対してP(x)が成り立つ。

11 帰納的述語の導出に関する帰納法 自然数の述語Pに関して、 の二つの条件が満たされているならば、 任意の自然数xに対して、
P(O)が成り立つ。 P(x)が成り立つならば、P(s(s(x)))が成り立つ。 の二つの条件が満たされているならば、 任意の自然数xに対して、 even(x) ⊃ P(x) が成り立つ。 even(x)の証明の構成に関する帰納法

12 論理（基礎） 時相論理 分類 時間の概念の入った論理 様相論理の一種 状態遷移系に関する言明
◇P --- 将来、いつか必ず、P が成り立つ。 P until Q … Qが成り立つまで P が成り立ち続ける。 分類 線形時間 --- ある決まった実行経路に関する言明 分岐時間 --- 実行経路全体に関する言明 実時間を扱える時相論理もある。　ハイブリッド系 確率的な状態遷移系を扱える時相論理もある。

13 線形時間と分岐時間 線形時間 分岐時間 ある決まった実行経路に関する言明 π: 実行経路 φ: 時相論理式
π|= φ: πにおいてφが成り立つ。 分岐時間 各状態から始まる実行経路全体に関する言明 s : 状態 s |= EGφ: s から始まる実行経路が存在して、 その経路上の任意の状態においてφが成り立つ。

14 検証技術 証明支援系 実はML（meta language）は、証明支援系を 実装するための言語なのであった。 証明チェッカ
人間が書いた形式的な証明をチェックする。 半自動の自動証明機能 --- tactic 主として高階述語論理やロジカル・フレームワーク 汎用 --- 記述力は大きい。 システム例: HOL、Isabelle、PVS Coq、Mizar 実はML（meta language）は、証明支援系を 実装するための言語なのであった。

15 検証技術 状態探索系 モデル検査系 状態遷移系の全数探索を行うことにより、 安全性や活性（liveness）の検証を行う。全自動
システム例: Murφ モデル検査系 時相論理の論理式が検証できる状態探索系 様々な時相論理 SMV … 分岐時間、記号モデル検査 SPIN … 線形時間

16 状態遷移系の記述 そもそも、状態遷移系を記述する枠組みは、 実に様々。 各種オートマトン プロセス計算 代数的枠組、カテゴリー理論
CSP、Promela（SPINの記述言語） CCS、π計算 Ambient calculus --- 移動コード Spi calculus --- セキュリティ 代数的枠組、カテゴリー理論 coalgebra、hidden algebra、… 多重集合書き換え（multiset rewriting）

17 記号モデル検査 モデル検査の効率化技術 状態をブール変数の組で表す。 さらに、論理式をBDDで表現する。 主として、分岐時間の時相論理
状態遷移は、遷移前状態の変数の組と、 遷移後状態の変数の組に関する述語: R(x,y) 初期状態を表す述語: I(x) すると、状態xで時相論理式φが成立することを表す述語を、R と I とから構成できる。 さらに、論理式をBDDで表現する。 類似した状態の計算を共有することができる。

18 対象（応用） ハードウェア 順序回路 非同期回路 分岐時間の時相論理 モデル検査、特に記号モデル検査 実時間の入った時相論理
実時間記号モデル検査

19 対象（応用） プロトコル・ソフトウェア・アルゴリズム （特に並列・分散） 状態遷移系としてモデル化 プロセス計算などを用いた記述
状態探索による検証・モデル検査 有限化の必要性 単純に大きさを制限する。 抽象化技術

20 対象（応用） プログラミング言語 型システム プログラム変換 コンパイラ 例えば、型安全性、型保存性 証明支援系＋帰納的定義
帰納的定義によって、意味論や型システムを定義。 プログラム変換 変換前と変換後の等価性 上と同様 コンパイラ これも、広い意味でプログラム変換

21 事例 --- 並行ゴミ集め 計算プロセスとゴミ集めのプロセスが、 並行に動く。 On The Fly (Dijkstra '78)
Snapshot (Yuasa '90) Very Concurrent GC (Huelsbergen and Winterbottom, ISMM'98)

22 事例 --- 並行ゴミ集め モデル化 システム全体の状態 状態の変化の仕方 … 状態遷移 ヒープ プロセスの状態
各セルの内容 プロセスの状態 プログラム・カウンタ、レジスタ、… 状態の変化の仕方 … 状態遷移 各プロセスがどのようにヒープを書き換え、 どのようにその状態を変化させるか。

23 事例 --- 並行ゴミ集め 検証条件 検証 資料 使用中のセルがゴミにならない。 ゴミは必ずいつかは回収される。
有限モデルの状態を網羅する。 完全に自動的な証明 資料 check.c 並行ゴミ集めの簡単な検証プログラム

24 並行ゴミ集めのモデル cells registers Heap C[4]F[4] R[0] 7 C[7]F[7] 6 R[1] 7
R[2] cells registers Heap

25 並行ゴミ集めのモデル Registers Heap R : register_index → cell_index∪{0}
C : cell_index → colors F : cell_index → cell_index∪{0} register_index = {1,2,…,m} cell_index = {1,2,…,n} colors = {Black,Gray,White,Free}

26 The Mutator R[i] := j (if C[j]=Free) R[i] := 0 R[i] := R[j]
R[i] := F[R[j]] F[R[i]] := R[j]

27 The Mutator R[i] := F[R[j]] (On The Fly) R[i] R[j]

28 The Mutator F[R[i]] := R[j] (Snapshot) R[i] R[j]

29 Side Effects R[i] := j R[i] := F[R[j]] F[R[i]] := R[j]
C[j] = Gray (On The Fly) C[j] = Black (Snapshot, VCGC) R[i] := F[R[j]] C[F[R[j]]] = Gray (On The Fly) F[R[i]] := R[j] C[F[R[i]]] = Gray (Snapshot) M = M ∪ {R[i]} (VCGC)

30 The Collector collector_step = {shade, mark, append, unmark}
shade ルートから直接に指されているWhiteのセルを Grayにする。 mark Grayのセルがあれば一つ選んでBlackに。 そこから指されているセルはGrayに。 Grayのセルがなければappendへ。 append WhiteのセルをFreeに。 Whiteのセルがなければunmarkへ。 unmark BlackかGrayのセルをWhiteに。 なければshadeへ。

31 The Collector shade mark

32 検証事項 安全性(safety) 『ルートから到達可能なセルが 回収される(Freeになる)ことはない。 』 活性(liveness)
『ルートから到達可能でなくなった セルは、いつかは回収される。 』

33 有限モデル検査 Havelund (’96) Bruns (’97) 萩谷 (’98) ー 安全性
萩谷 (’98) ー 安全性 cell_index = {1, 2, 3} register_index = {1, 2, 3} 状態: 2 + 2 * 3 + (2 + 2) * 3 = 20 bits 到達可能状態: on the fly 257,730 snapshot 227,285

34 状態の抽象化 ー on the fly の安全性 セルの抽象化 ー 抽象セル 状態の抽象化 collector のステップ (セル自身の)色
ルートからの直接的な到達可能性 ルートからの到達可能性 参照しているセルの色 状態の抽象化 collector のステップ 抽象セルの(有限)集合 F T

35 抽象遷移 register register R0 T T abs_R0 F T nil F T nil F F T F nil

36 抽象化の正当性 s0 → s1 → s2 → … → sn → t1 → t2 → … → tn t0 具体遷移 抽象遷移
If t is an abstraction of s and s → s’ , there exists t’ such that t’ is an abstraction of s’ and t → t’ .

37 抽象化の正当性を 証明支援系（HOL)で検証する試み
レジスタからの到達可能性の形式化 帰納的定義の利用 val direct_reachable_DEF = Define `direct_reachable (r:num->num option) (h:num->color#num option) k = ?i. (r i = SOME k)`; val (REACHABLE_thm1,REACHABLE_thm2,REACHABLE_thm3) = IndDefLib.new_simple_inductive_definition [ ``direct_reachable r h k ==> reachable r h k``, ``reachable (r:num->num option) (h:num->color#num option) k ∧ IS_SOME (field (h k)) reachable r h (THE (field (h k)))``];

38 抽象遷移の正当性の検証 val R0_safe = STORE_THM("R0_safe",
``!(s:step) (r:num->num option) (h:num->color#num option) s' r' h' i (as:step) (ah:color->color option->bool->bool->bool) as' ah'. R0 s r h s' r' h' i ∧ abs_R0 as ah as' ah' ∧ abstract_relation s r h as ah ==> abstract_relation s' r' h' as' ah'``, REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC [abstract_relation_DEF] THEN STRIP_TAC ...

39 事例 --- コンパイラ モデル化 帰納的定義 ソース言語 ターゲット言語（機械語） 構文論 意味論 型システム
SOS (Structured Operational Semantics)

40 事例 --- コンパイラ 検証条件 検証 ソース・プログラムとターゲット・プログラムの 意味が同じ。 帰納的な述語を含む高階述語論理
帰納的定義から導出される帰納法を用いた証明 高階述語論理の証明支援系（HOL）

41 小さなコンパイラの検証 資料 http://nicosia.is.s.u-tokyo.ac.jp/members/hagiya.html
indnew 帰納的定義と数学的帰納法の解説 コンパイラの形式化 theory_compiler.txt 山本光晴氏によるHOLを用いた実際の検証

42 演習III課題（自動証明・検証） （１）自動証明・検証 計算システムの正しさを保証する技術に関して学びます． cf.計算機言語論
証明支援系(高階論理やλ計算をもとにした半自動的な証明系) 高階論理やλ計算，証明支援系の基礎に関する学習(文献購読など) 適当な対象に対する証明の実験(コンパイラなど) モデル検査(状態の全数探索による自動的な証明手法) モデル検査の基礎(時相論理など)に関する学習(文献購読など) 検証の実験 分散・並列アルゴリズム，ハードウェア(cache coherenceなど) 検証系を利用したアルゴリズム探索の実験 ハイブリッド系 実時間に依存するシステムの検証技術と応用例，検証の実験 確率的に振舞うシステムの検証技術と応用例，検証の実験

43 演習III課題（セキュリティ技術） （２）セキュリティ技術
検証技術の応用として，プログラミング言語のセキュリティやネットワーク・セキュリティに関連した技術について学びます．cf.計算機言語論 ネットワーク・セキュリティ セキュリティ・プロトコルの検証技術に関する文献の購読 実際のプロトコルの解析や検証 SSH、SSL、Kerberos、e-Commerce（SETなど）、Smart Card、… SPKI、… Anonymizer、… Javaセキュリティ Javaセキュリティに関する文献の購読 バイトコード検証，ローディング制約，アクセス制御，情報漏洩 簡単なモデル上での検証の実験

44 認証プロトコルの解析と検証のための形式的手法
有限状態解析(finite state analysis) 計算機による自動的な解析 攻撃の可能性の探索 自動的な解析のために状態空間を有限に限定。 帰納的定義(inductive definition)に基づく証明 プロトコルの実行の可能性を帰納的に定義 高階論理の証明支援系を用いて半自動化 様相論理(modal)を用いた分析 BAN論理などのbelief logic 直感的な議論を適切に表現可能 モデルが明らかでない。完全性は成り立たない。 型とeffectによる解析

45 A®B : {A,NA}KB B®A : {NA,NB}KA A®B : {NA}KB
Needham-Schroederのプロトコルと その修正版 A®B : {A,NA}KB　 B®A : {NA,NB}KA A®B : {NA}KB　 A®B : {A,NA}KB　 B®A : {B,NA,NB}KA A®B : {NA}KB　

46 A®B : {A,NA}KB B®A : {NA,NB}KA A®B : {B,NA}KA－1
色々なプロトコル A®B : {A,NA}KB　 B®A : {NA,NB}KA A®B : {B,NA}KA－1　 A®B : {A,NA}KB B®A : {{NA}KA, {B,NB}KA} A®B : {NA,NB}KB B®A : {Ack}NA

47 演習III課題（分子計算） （３）生命情報(分子計算)
生物の持つ計算能力の解析，および，生物を用いた新しい計算機(計算する人工生物)の可能性について探求します．cf.生命情報論 分子計算(DNA計算)に関する論文購読，シミュレーション，実験? 「検証・自動証明」との関連は小さいが、 並行計算としての分子反応のモデル化 その解析・予測 そのシミュレーション … ハイブリッド系

48 演習III課題（分子計算） 最近のNatureやScienceなどの論文を読む。 実験技術に関して調べる。 実験？ 配列の設計
CRESTのプロジェクトに関連した実験 実験？ 希望があれば。見学は毎年やっている。 配列の設計 符号理論に基づく配列セットの設計 与えられた構造をとるような配列の設計 （inverse folding） CRESTのプロジェクトに関連 分子計算のシミュレーション