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

Slides:



Advertisements
Similar presentations
プログラミング言語論 第3回 BNF 記法について(演習付き) 篠埜 功. 構文の記述 プログラミング言語の構文はどのように定式化できるか? 例1 : for ループの中に for ループが書ける。 for (i=0; i
Advertisements

一階述語論理 (first-order predicate logic) 一階述語論理入門 構文論(論理式の文 法) 意味論(論理式の解 釈) 認知システム論 知識と推論(4) 知識と論理でを組み合わせて問題を解決する.
紹介担当: 石尾 隆(大阪大学) Q11.  Feature Model によって定義される「プロダクトの集合」 (プロダクトライン)の振舞いを検証する手法の拡張 ◦ 通常の振舞い検証: たとえば Promela を使って,1プロダクトの 振舞いを表現したオートマトンの取りうる状態遷移を調べる ◦
和田俊和 資料保存場所 /2/26 文法と言語 ー正規表現とオートマトンー 和田俊和 資料保存場所
プログラミング言語論 第10回(演習) 情報工学科 木村昌臣   篠埜 功.
モデル検査の応用 徳田研究室 西村太一.
人工知能特論2011 No.4 東京工科大学大学院 担当教員:亀田弘之.
ソフトウェア基礎科学 授業資料: 論理関係(logical relations)のお話
チュートリアル 形式的検証技術 Logical Framework と Modal Logic
班紹介 描画班一同.
プログラミングパラダイム さまざまな計算のモデルにもとづく、 プログラミングの方法論 手続き型 関数型 オブジェクト指向 代数 幾何.
データ構造と アルゴリズム 理工学部 情報システム工学科 新田直也.
5.チューリングマシンと計算.
5.チューリングマシンと計算.
計算の理論 I ー DFAとNFAの等価性 ー 月曜3校時 大月 美佳.
演習3 最終発表 情報科学科4年 山崎孝裕.
プログラミング言語論 第6回 型 情報工学科 篠埜 功.
論理式の表現を数学的に取り扱いやすくするために代数学の助けを借りる.
人工知能特論2011 資料No.6 東京工科大学大学院 担当教員 亀田弘之.
Semantics with Applications
条件式 (Conditional Expressions)
データ構造と アルゴリズム 知能情報学部 新田直也.
Systems and Software Verification 10. Fairness Properties
CSP記述によるモデル設計と ツールによる検証
米澤研究室 全体ミーティング 2010/12/22 M2 渡邊裕貴.
ML 演習 第 7 回 新井淳也、中村宇佑、前田俊行 2011/05/31.
Solving Shape-Analysis Problems in Languages with Destructive Updating
チューリング機械 状態の有限集合 ヘッドの方向を表す。 L:1コマ左へ R:1コマ右へ テープ記号の有限集合 入力記号の有限集合 動作関数
第2章 「有限オートマトン」.
型付きアセンブリ言語を用いた安全なカーネル拡張
不完全な知識 不完全な知識に基づく問題解決 フレーム問題 制約条件記述問題 非単調推論 極小限定 常識の定式化 並列極小限定.
プログラミング言語論 第3回 BNF記法について(演習付き)
第25章 単一始点最短路 3節 Bellman-Fordのアルゴリズム
形式言語の理論 5. 文脈依存言語.
モデル検査 状態遷移系 PLTL(propositional linear-time temporal logic) PLTLのモデル検査
7.4 Two General Settings D3 杉原堅也.
オートマトンとチューリング機械.
 型推論1(単相型) 2007.
依存型で型付けされた 副作用のある関数のための 型保存コンパイラ
Structural operational semantics
ATTAPL輪講 (第4回) 続 Dependent Types
知能情報システム特論 Introduction
第5章 計算とプログラム 本章で説明すること ・計算の概観と記述法 ・代表的な計算モデル ・プログラムとプログラム言語.
プログラミング言語論 第9回 情報工学科 木村昌臣 篠埜 功.
 型推論3(MLの多相型).
モデル検査(5) CTLモデル検査アルゴリズム
計算の理論 I 決定性有限オートマトン(DFA) と 非決定性有限オートマトン(NFA)
INTRODUCTION TO SOFTWARE ENGINEERING
5.チューリングマシンと計算.
Type Systems and Programming Languages ; chapter 13 “Reference”
人工知能特論II 第8回 二宮 崇.
第7回  命題論理.
東京工科大学 コンピュータサイエンス学部 亀田弘之
東京工科大学 コンピュータサイエンス学部 亀田弘之
ガウス分布における ベーテ近似の理論解析 東京工業大学総合理工学研究科 知能システム科学専攻 渡辺研究室    西山 悠, 渡辺澄夫.
PROGRAMMING IN HASKELL
プログラミング言語論 第10回 情報工学科 篠埜 功.
アルゴリズムとデータ構造1 2009年6月15日
述語論理式の構文と意味 一階述語論理式の構文 一階述語論理式の意味 述語,限量記号 自然言語文の述語論理式表現 解釈 妥当,充足不能
計算の理論 I -講義について+αー 月曜3校時 大月美佳 平成31年5月18日 佐賀大学理工学部知能情報システム学科.
4.プッシュダウンオートマトンと 文脈自由文法の等価性
PROGRAMMING IN HASKELL
オブジェクト指向言語論 第二回 知能情報学部 新田直也.
コンパイラ 2012年10月11日
アルゴリズムとデータ構造 2010年6月17日
PROGRAMMING IN HASKELL
情報数理Ⅱ 第10章 オートマトン 平成28年12月21日.
計算の理論 I -講義について+αー 火曜3校時 大月美佳 平成31年8月23日 佐賀大学理工学部知能情報システム学科.
オブジェクト指向言語論 第三回 知能情報学部 新田直也.
Static Enforcement of Security with Types
Presentation transcript:

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

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

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

依存型 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 = | cons of BINTREE=>BINTREE`; HOL

述語の帰納的定義 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

帰納的述語の証明 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)))

再帰的データの構成に関する帰納法 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)が成り立つ。

帰納的述語の導出に関する帰納法 自然数の述語Pに関して、 の二つの条件が満たされているならば、 任意の自然数xに対して、 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 から始まる実行経路が存在して、 その経路上の任意の状態においてφが成り立つ。

検証技術 証明支援系 実はML(meta language)は、証明支援系を 実装するための言語なのであった。 証明チェッカ 人間が書いた形式的な証明をチェックする。 半自動の自動証明機能 --- 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)

記号モデル検査 モデル検査の効率化技術 状態をブール変数の組で表す。 さらに、論理式をBDDで表現する。 主として、分岐時間の時相論理 状態遷移は、遷移前状態の変数の組と、 遷移後状態の変数の組に関する述語: 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 並行ゴミ集めの簡単な検証プログラム

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

並行ゴミ集めのモデル 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}

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]

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 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)

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へ。

The Collector shade mark

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

有限モデル検査 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

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

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

抽象化の正当性 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’ .

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

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

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

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 

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

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

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