自動証明・検証技術 - HAGIYA Laboratory

自動証明・検証技術
• 論理（基礎）
– 高階述語論理、ロジカル・フレームワーク
– 時相論理
• 検証技術
– 証明支援系
– モデル検査系
計算システムの「正しさ」を
保証する理論や技術
• 対象（応用）
–
–
–
–
ハードウェア
プロトコル（セキュリティ関連を含む）
ソフトウェア・アルゴリズム（特に並列・分散）
プログラミング言語（例えばコンパイラ）
論理（基礎）
• 高階述語論理
– ∀f. --- 任意の関数 f について…
– 関数や述語に関する量化（∀∃）が可能な論理
• ロジカル・フレームワーク
– 型付きλ計算
– カリー・ハワードの対応に従って、
証明をλ項で表現する。
– 依存型（dependent type）があると、
高階述語論理を表現することができる。
– 様々な論理を表現する枠組論理の論理
カリー・ハワードの対応
• 命題 … 型
A⊃B … A→B
AならばB … AからBへの関数の型
• 命題Aの証明 … Aを型として持つ項
A⊃Bの証明 … Aの証明をもらって
Bの証明を返す関数
• 構成的な証明の考えに基づいている。
• 直観主義論理
依存型
• 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]
帰納的定義
• 多くの証明支援系には、
帰納的定義によって論理を拡張する機能が
備わっている。
• 型の帰納的定義 … 再帰的データ型
• 述語の帰納的定義
• カリー・ハワードの対応のもとでは同じ原理
再帰的データ型
• 自然数
– Oは自然数である。
– xが(既に作られた)自然数ならば、
s(x)も自然数である。
– 以上のようにして作られるもののみが
自然数である。
datatype NAT = O | s of NAT; ML
load "Datatype"; open Datatype;
Hol_datatype
`NAT = O | s of NAT`; HOL
再帰的データ型
• 自然数を葉に持つ二分木
datatype BINTREE =
leaf of NAT
| cons of BINTREE*BINTREE; ML
Hol_datatype `BINTREE =
leaf of NAT
| cons of BINTREE=>BINTREE`; HOL
述語の帰納的定義
• even(x)の定義
– even(O)が成り立つ。
– even(x)が成り立てば、
even(s(s(x)))も成り立つ。
– 以上のようにしてevenが導かれるときのみ、
evenが成り立つ。
load "IndDefLib"; open IndDefLib;
new_simple_inductive_definition [
``T ==> even O``,
``even x ==>
even (s (s x))``]; HOL
帰納的述語の証明
• even(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)))
再帰的データの構成に関する帰納法
• 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)が成り立つ。
帰納的述語の導出に関する帰納法
• 自然数の述語Pに関して、
– P(O)が成り立つ。
– P(x)が成り立つならば、P(s(s(x)))が成り立つ。
の二つの条件が満たされているならば、
任意の自然数xに対して、
even(x) ⊃ P(x)
が成り立つ。
• even(x)の証明の構成に関する帰納法
論理（基礎）
• 時相論理
–
–
–
–
–
時間の概念の入った論理
様相論理の一種
状態遷移系に関する言明
◇P --- 将来、いつか必ず、P が成り立つ。
P until Q … Qが成り立つまで P が成り立ち続ける。
• 分類
–
–
–
–
線形時間 --- ある決まった実行経路に関する言明
分岐時間 --- 実行経路全体に関する言明
実時間を扱える時相論理もある。ハイブリッド系
確率的な状態遷移系を扱える時相論理もある。
線形時間と分岐時間
• 線形時間
–
–
–
–
ある決まった実行経路に関する言明
π: 実行経路
φ: 時相論理式
π|= φ: πにおいてφが成り立つ。
• 分岐時間
–
–
–
–
各状態から始まる実行経路全体に関する言明
s : 状態
φ: 時相論理式
s |= EGφ: s から始まる実行経路が存在して、
その経路上の任意の状態においてφが成り立つ。
検証技術
• 証明支援系
–
–
–
–
–
–
証明チェッカ
人間が書いた形式的な証明をチェックする。
半自動の自動証明機能 --- tactic
主として高階述語論理やロジカル・フレームワーク
汎用 --- 記述力は大きい。
システム例:
• HOL、Isabelle、PVS
• Coq、Mizar
• 実はML（meta language）は、証明支援系を
実装するための言語なのであった。
検証技術
• 状態探索系
– 状態遷移系の全数探索を行うことにより、
安全性や活性（liveness）の検証を行う。全自動
– システム例:
• Murφ
• モデル検査系
– 時相論理の論理式が検証できる状態探索系
– 様々な時相論理
– システム例:
• SMV … 分岐時間、記号モデル検査
• SPIN … 線形時間
状態遷移系の記述
• そもそも、状態遷移系を記述する枠組みは、
実に様々。
– 各種オートマトン
– プロセス計算
•
•
•
•
CSP、Promela（SPINの記述言語）
CCS、π計算
Ambient calculus --- 移動コード
Spi calculus --- セキュリティ
– 代数的枠組、カテゴリー理論
• coalgebra、hidden algebra、…
– 多重集合書き換え（multiset rewriting）
記号モデル検査
• モデル検査の効率化技術
– 主として、分岐時間の時相論理
• 状態をブール変数の組で表す。
– 状態遷移は、遷移前状態の変数の組と、
遷移後状態の変数の組に関する述語: R(x,y)
– 初期状態を表す述語: I(x)
– すると、状態xで時相論理式φが成立することを表す
述語を、R と I とから構成できる。
• さらに、論理式をBDDで表現する。
– 類似した状態の計算を共有することができる。
対象（応用）
• ハードウェア
– 順序回路
• 分岐時間の時相論理
• モデル検査、特に記号モデル検査
– 非同期回路
• 実時間の入った時相論理
• 実時間記号モデル検査
対象（応用）
• プロトコル・ソフトウェア・アルゴリズム
（特に並列・分散）
–
–
–
–
状態遷移系としてモデル化
プロセス計算などを用いた記述
状態探索による検証・モデル検査
有限化の必要性
• 単純に大きさを制限する。
• 抽象化技術
対象（応用）
• プログラミング言語
– 型システム
• 例えば、型安全性、型保存性
• 証明支援系＋帰納的定義
• 帰納的定義によって、意味論や型システムを定義。
– プログラム変換
• 変換前と変換後の等価性
• 上と同様
– コンパイラ
• これも、広い意味でプログラム変換
事例 --- 並行ゴミ集め
• 計算プロセスとゴミ集めのプロセスが、
並行に動く。
• On The Fly (Dijkstra '78)
• Snapshot (Yuasa '90)
• Very Concurrent GC (Huelsbergen and
Winterbottom, ISMM'98)
事例 --- 並行ゴミ集め
• モデル化
– システム全体の状態
• ヒープ
– 各セルの内容
• プロセスの状態
– プログラム・カウンタ、レジスタ、…
– 状態の変化の仕方 … 状態遷移
• 各プロセスがどのようにヒープを書き換え、
• どのようにその状態を変化させるか。
事例 --- 並行ゴミ集め
• 検証条件
– 使用中のセルがゴミにならない。
– ゴミは必ずいつかは回収される。
• 検証
– 有限モデルの状態を網羅する。
– 完全に自動的な証明
• 資料
– http://nicosia.is.s.u-tokyo.ac.jp/members/hagiya.html
– check.c
– 並行ゴミ集めの簡単な検証プログラム
並行ゴミ集めのモデル
C[4]F[4]
R[0]
R[1]
7
7
C[7]F[7]
6
C[6]F[6]
R[2]
0
registers
C[9]F[9]
cells
Heap
並行ゴミ集めのモデル
• Registers
– R : register_index → cell_index∪{0}
• Heap
– 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}
The Mutator
• R[i] :=
• R[i] :=
• R[i] :=
• R[i] :=
• F[R[i]]
j (if C[j]=Free)
0
R[j]
F[R[j]]
:= R[j]
The Mutator
R[i] := F[R[j]] (On The Fly)
R[i]
R[j]
The Mutator
F[R[i]] := R[j] (Snapshot)
R[i]
R[j]
Side Effects
• R[i] := 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)
The Collector
•
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へ。
The Collector
• shade
• mark
検証事項
• 安全性(safety)
『ルートから到達可能なセルが
回収される(Freeになる)ことはない。』
• 活性(liveness)
『ルートから到達可能でなくなった
セルは、いつかは回収される。』
有限モデル検査
• Havelund (’96)
• Bruns (’97)
• 萩谷 (’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
状態の抽象化ー on the fly の安全性
• セルの抽象化ー抽象セル
–
–
–
–
(セル自身の)色
ルートからの直接的な到達可能性
ルートからの到達可能性
参照しているセルの色
• 状態の抽象化
– collector のステップ
– 抽象セルの(有限)集合
F
T
抽象遷移
register
T
R0
T
register
T
F
T nil
T
abs_R0
F
F
F
T
F
T nil
F
F nil
抽象化の正当性
具体遷移
s0 → s1 → s2 → … → sn
抽象遷移
t0 → t1 → t2 → … → tn
If t is an abstraction of s and s → s’ ,
there exists t’ such that
t’ is an abstraction of s’ and t → t’ .
抽象化の正当性を
証明支援系（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)))``];
抽象遷移の正当性の検証
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
...
...
...
...
...
事例 --- コンパイラ
• モデル化
–
–
–
–
–
ソース言語
ターゲット言語（機械語）
構文論
意味論
型システム
• 帰納的定義
– SOS (Structured Operational Semantics)
事例 --- コンパイラ
• 検証条件
– ソース・プログラムとターゲット・プログラムの
意味が同じ。
– 帰納的な述語を含む高階述語論理
• 検証
– 帰納的定義から導出される帰納法を用いた証明
– 高階述語論理の証明支援系（HOL）
小さなコンパイラの検証
• 資料
– http://nicosia.is.s.u-tokyo.ac.jp/members/hagiya.html
– indnew
• 帰納的定義と数学的帰納法の解説
• コンパイラの形式化
– theory_compiler.txt
• 山本光晴氏によるHOLを用いた実際の検証
演習III課題（自動証明・検証）
（１）自動証明・検証
– 計算システムの正しさを保証する技術に関して学びます．
cf.計算機言語論
– 証明支援系(高階論理やλ計算をもとにした半自動的な証明
系)
• 高階論理やλ計算，証明支援系の基礎に関する学習(文献購読など)
• 適当な対象に対する証明の実験(コンパイラなど)
– モデル検査(状態の全数探索による自動的な証明手法)
• モデル検査の基礎(時相論理など)に関する学習(文献購読など)
• 検証の実験
• 分散・並列アルゴリズム，ハードウェア(cache coherenceなど)
– 検証系を利用したアルゴリズム探索の実験
– ハイブリッド系
• 実時間に依存するシステムの検証技術と応用例，検証の実験
• 確率的に振舞うシステムの検証技術と応用例，検証の実験
演習III課題（セキュリティ技術）
（２）セキュリティ技術
– 検証技術の応用として，プログラミング言語のセキュリティや
ネットワーク・セキュリティに関連した技術について学びます．
cf.計算機言語論
– ネットワーク・セキュリティ
• セキュリティ・プロトコルの検証技術に関する文献の購読
• 実際のプロトコルの解析や検証
– SSH、SSL、Kerberos、e-Commerce（SETなど）、Smart Card、…
– SPKI、…
– Anonymizer、…
– Javaセキュリティ
• Javaセキュリティに関する文献の購読
• バイトコード検証，ローディング制約，アクセス制御，情報漏洩
• 簡単なモデル上での検証の実験
認証プロトコルの解析と検証のための
形式的手法
• 有限状態解析(finite state analysis)
– 計算機による自動的な解析
– 攻撃の可能性の探索
– 自動的な解析のために状態空間を有限に限定。
• 帰納的定義(inductive definition)に基づく証明
– プロトコルの実行の可能性を帰納的に定義
– 高階論理の証明支援系を用いて半自動化
• 様相論理(modal)を用いた分析
– BAN論理などのbelief logic
– 直感的な議論を適切に表現可能
– モデルが明らかでない。完全性は成り立たない。
• 型とeffectによる解析
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
色々なプロトコル
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
演習III課題（分子計算）
（３）生命情報(分子計算)
– 生物の持つ計算能力の解析，および，生物を用いた
新しい計算機(計算する人工生物)の可能性につい
て探求します．cf.生命情報論
– 分子計算(DNA計算)に関する論文購読，シミュレー
ション，実験?
– 「検証・自動証明」との関連は小さいが、
• 並行計算としての分子反応のモデル化
• その解析・予測
• そのシミュレーション … ハイブリッド系
演習III課題（分子計算）
• 最近のNatureやScienceなどの論文を読む。
• 実験技術に関して調べる。
– CRESTのプロジェクトに関連した実験
• 実験？
– 希望があれば。見学は毎年やっている。
• 配列の設計
– 符号理論に基づく配列セットの設計
– 与えられた構造をとるような配列の設計
（inverse folding） CRESTのプロジェクトに関連
• 分子計算のシミュレーション

Download Report