Survey: A Type System for Certified Binaries

Slides:



Advertisements
Similar presentations
プログラミング言語論 第10回(演習) 情報工学科 木村昌臣   篠埜 功.
Advertisements

Coq を使った証明 : まとめ 稲葉.
ソフトウェア基礎科学 授業資料: 論理関係(logical relations)のお話
2006/11/30 山下 諒蔵 佐藤 春旗 前田 俊行 大山 恵弘 佐藤 秀明 住井 英二郎
プログラミングパラダイム さまざまな計算のモデルにもとづく、 プログラミングの方法論 手続き型 関数型 オブジェクト指向 代数 幾何.
2006/10/12 山下 諒蔵 佐藤 春旗 前田俊行 大山 恵弘 佐藤 秀明 住井 英二郎
演習3 最終発表 情報科学科4年 山崎孝裕.
型宣言 (Type Declarations)
型宣言(Type Declarations)
論理式の表現を数学的に取り扱いやすくするために代数学の助けを借りる.
Natural Semantics 実行過程の、最初と最後の状態(state)の関係を考える。
条件式 (Conditional Expressions)
9.NP完全問題とNP困難問題.
データ構造と アルゴリズム 知能情報学部 新田直也.
2007/1/11 山下 諒蔵 佐藤 春旗 前田 俊行 大山 恵弘 佐藤 秀明 住井 英二郎
Tokuda Lab. NISHIMURA Taichi
米澤研究室 全体ミーティング 2010/12/22 M2 渡邊裕貴.
ML 演習 第 7 回 新井淳也、中村宇佑、前田俊行 2011/05/31.
表現系工学特論 項書換え系(4) 完備化 1.語問題と等式証明 2.合流性とチャーチ・ロッサ性 3.完備化手続き.
プログラミング言語論 第12回 関数型プログラミング 情報工学科 篠埜 功.
Solving Shape-Analysis Problems in Languages with Destructive Updating
TAL : Typed Assembly Language について
型付きアセンブリ言語を用いた安全なカーネル拡張
PROGRAMMING IN HASKELL
第25章 単一始点最短路 3節 Bellman-Fordのアルゴリズム
PROGRAMMING IN HASKELL
暗黙的に型付けされる構造体の Java言語への導入
形式言語の理論 5. 文脈依存言語.
Macro Tree Transducer の 型検査アルゴリズム
お仕事にまったく役にたたない内容のコードレビューやりたいと思います。
A Provably Sound TAL for Back-end Optimization について
国立情報学研究所 ソフトウェア研究系 助教授/
 型推論1(単相型) 2007.
依存型で型付けされた 副作用のある関数のための 型保存コンパイラ
25. Randomized Algorithms
Structural operational semantics
ATTAPL輪講 (第4回) 続 Dependent Types
SUNFLOWER B4 岡田翔太.
 型推論3(MLの多相型).
2007/6/12(通信コース)2007/6/13(情報コース) 住井
Type Systems and Programming Languages
米澤研究室 全体ミーティング 2010/07/07 M2 渡邊裕貴.
国立情報学研究所 ソフトウェア研究系 助教授/
Type Systems and Programming Languages ; chapter 13 “Reference”
第7回  命題論理.
PROGRAMMING IN HASKELL
プログラミング言語論 第10回 情報工学科 篠埜 功.
~sumii/class/proenb2010/ml2/
述語論理式の構文と意味 一階述語論理式の構文 一階述語論理式の意味 述語,限量記号 自然言語文の述語論理式表現 解釈 妥当,充足不能
矛盾した知識 デフォルト推論 仮説を用いた推論 準無矛盾推論 デフォルト規則 デフォルト理論の拡張 → デフォルト証明 シナリオ
2006/6/27(通信コース)2006/7/5(情報コース) 住井
~sumii/class/proenb2009/ml6/
PROGRAMMING IN HASKELL
Eijiro Sumii and Naoki Kobayashi University of Tokyo
関数型言語の基礎 型なしl計算 型理論 構成的プログラミング GUIにあらわれる関数概念 PBD VL
18. Case Study : Imperative Objects
全体ミーティング 2010/05/19 渡邊 裕貴.
SMP/マルチコアに対応した 型付きアセンブリ言語
コンパイラ 2012年10月11日
プログラミング入門2 第6回 関数 情報工学科 篠埜 功.
PROGRAMMING IN HASKELL
全体ミーティング(6/3) 修士2年 飯塚 大輔.
型理論 ラッセルのパラドックス: 「集合の集合」は矛盾を引き起こす。 ラッセル、ホワイトヘッド 「プリンキピアマセマティカ」
参考:大きい要素の処理.
Haskell Programming Language
線形符号(10章).
全体ミーティング(9/15) 村田雅之.
 型理論の初歩 2007 fall.
プログラミング言語論 プログラミング言語論 演習7 解答と解説 演習7 解答と解説 1.
Static Enforcement of Security with Types
Presentation transcript:

Survey: A Type System for Certified Binaries <tossy-2@yl.is.s.u-tokyo.ac.jp>

論文ソース Z. Shao, V. Trifonov, B. Saha and N. Papaspyrou. A Type System for Certified Binaries. ACM Transactions on Programming Languages and Systems (TOPLAS), 27(1), pp.1-45, 2005.

この論文の目的 Certified Binary に関する型理論フレームワークの構築 高階述語論理と同等な記述力での定理記述を可能にする Foundational Proof-Carrying Code 検証が決定可能になるように設計する 依存型を応用し、型検査の問題に帰着 型「推論」ではありません

Proof-Carrying Code (PCC) コードと一緒に安全性に関する数学的証明を 添付して配布 コード送信者が証明を作成する 手による、または自動で コード受信者はその証明を検証する 耐タンパ性がある コードだけ変えれば、コードが証明と矛盾を起こす 証明も変えれば、セキュリティポリシーと矛盾を起こす どちらにも当てはまらないならば、セキュリティポリシーに合致しているので安全なまま

Proof-Carrying Code (PCC) 関連 型付きアセンブリ言語 [Morrisett ら, 1998] アセンブリ言語(≒ 機械語)に対して型を導入 メモリアクセスの安全性などを型によって保証するという アプローチ Foundational PCC [Appel, 2001] Trusted Computing Base を小さくする研究 検証器(VCgen: Verification Condition Generator)を 実装しなくても、定理証明系を使えばいい 高階述語論理による PCC の構成 定理証明系はいろいろある

Certified Binaries とは何か コードの挙動(性質)に関する数学的証明を添付されたコード 要するに PCC と同じです 性質の例: 関数 f は素数を受け取ると必ず終了し、返り値も また素数である 高階述語論理による記述 型付きアセンブリ言語 (Morrisett ら, 1998) などよりも記述力が高い

方針 定理と証明を取り扱える型付き言語を設計 証明を保存するプログラム変換の定義 論理を記述する型言語 TL の設計 それを用いた計算言語 λH の設計 証明を保存するプログラム変換の定義 CPS 変換、Closure 変換 λK、λC などの言語を定義し、変換 記述された性質が保存されることを証明

{ 言語の設計 (sketch) 型付きλ計算を基にする 4 つの階層(大きくは 2 つ)に分けて設計 Fω [Girard ら, 1972] に類似 4 つの階層(大きくは 2 つ)に分けて設計 { 証明の記述を 行う プログラムを 表現

Dependent product type (全称量化子 ∀ に対応) 証明の記述 (sketch) 論理式を型によって表現 高階述語論理 ⇔ 依存型 Formulae-as-Types, Curry-Howard 対応とも呼ばれる 定理証明 ⇔ 型検査 Dependent product type (全称量化子 ∀ に対応)

依存型 (Dependent Type) 値に依存する型を取り扱うための理論 Dependent product, Dependent sum このあと出てくるのは dependent product だけ なので、こちらのみ解説する 高階述語論理と同等の記述力を持つ Curry-Howard 対応

依存型 (Dependent Type) Dependent Product (Π) Dependent function とも呼ばれる Vec(n) : n 要素のベクトル という型は n という値に依存 「自然数(Nat 型) n をとり Vec(n) を返す関数」の型 → Πn:Nat. Vec(n) たとえばベクトルの作成などはこのような型 Πx:τ. τ’ において τ’ が x に依存しない場合は、関数 τ→τ’ と同じ したがって、一般の関数は Π を用いて記述できる

Curry-Howard 対応 [Howard, 1980] Formulae-as-types correspondence とも呼ばれる 命題をそれぞれ型と対応させる Logical connective ⇔ Functor P ⇒ Q ⇔ P → Q 型 P ∧ Q ⇔ P×Q 型 値はそれぞれの命題の証明を表すと考える 命題 P の証明 ⇔ P 型の項 P ⇒ Q の証明 ⇔ P → Q 型の関数項 量化子は dependent product, dependent sum に対応 ∀x∈S. P(x) ⇔ Πx:S. P(x) Dom(この関数) = S

依存型における問題 プログラムの型付けが非決定的になる可能性 型を保存したコンパイルが難しい など 実際のプログラムでは、副作用や無限ループが存在しうる 型を求めるためには値を計算する必要 型を保存したコンパイルが難しい CPS 変換において継続の型は? [Barthe ら, 1999] など

これらの問題を解決するために… 型が値に依存していることが原因 ⇒ 依存する部分を「上に持ち上げる」 値(計算言語)と型(論理記述)を切り離せばよい ⇒ 依存する部分を「上に持ち上げる」 依存「型」ではなく、依存「類」などにする 値と、型以上の部分を分離することができる 類は型に依存してもよい

Type Language TL 3 つの階層 Π はそれぞれ下のレベルでの λ-抽象と適用に対応 Type 計算を抽象化したモデルを記述 Kind モデルに関する性質を記述 Kscm 性質に関する性質を記述 Π はそれぞれ下のレベルでの λ-抽象と適用に対応 たとえば、λt:κ.τ は Πt:κ.κ’ と型付けされる Type のレベルに Π は含まれていない

Type Language TL Ω (=計算式)の定義は帰納的であると仮定 生成: Ctor, 破壊: Elim 一般的な枠組み: Ind (at kind level) プログラム変換が証明を保存することが議論可能に プログラム変換とは、Ω → Ω’ の変換であるが、このようにすることで帰納的な Ω は統一的に扱える

TL による記述の例 Ctor Elim Inductive Nat: Kind := zero: Nat | succ: Nat → Nat plus: Nat → Nat → Nat plus(zero) = λt:Nat. t plus(succ t) = λt’:Nat. succ ((plus t) t’) ifez: Nat → (Πk:Kind. k → (Nat → k) → k) ifez(zero) = λk:Kind. λt1:k. λt2:Nat → k. t1 ifez(succ t) = λk:Kind. λt1:k. λt2:Nat → k. t2 t Ctor Type Elim Kscm

TL による記述の例 zero = Ctor(1, Nat), succ = Ctor(2, Nat) の省略と考える Nat : Kind = Ind(X: Kind) { X; X→X } plus : Nat→Nat→Nat = λt:Nat. Elim[Nat, Nat→Nat→Nat] (t) { λt’:Nat. t’ ; λt’:Nat. succ (plus t t’) } zero = Ctor(1, Nat), succ = Ctor(2, Nat) の省略と考える Nat に関するι簡約 Elim[Nat. A”] (zero) {B0; Bs} →ι B0 Elim[Nat, A”] (succ N) {B0; Bs} →ι Bs N A” は証明に用いられる Inductive Nat: Kind := zero: Nat      | succ: Nat → Nat plus: Nat → Nat → Nat plus(zero) = … plus(succ t) = …

類似研究 Pure Type Systems, λU [Barendregt, 1991] [Werner, 1994] Coq/CIC [Huet ら, 2000] System Notation TL Kind Kscm Ext Werner Set Type Coq/CIC Set, Prop Type(0) Type(1) Barendregt * □ △

TL の性質 型付け規則 λ抽象と適用 Πに関して ただし R = Ext は Kscm のもう一つ上のレベル

Ci が類 X の well-formed constructor である TL の性質 型付け規則 帰納的類に関して 類定義 コンストラクタ デストラクタ Ci が類 X の well-formed constructor である とりあえず細かいので省略

コンストラクタ 引数を本体に適用 するメタ関数 TL の性質 簡約関係 β簡約、η簡約 : 通常のλ計算と同様 帰納的な型に関するι簡約 なお、上においてΦは次のように定義される コンストラクタ 引数を本体に適用 するメタ関数

TL の性質 ι簡約の例 plus (succ zero) zero  ⇒ succ zero になればよい

TL の性質 ι簡約の例 plus (succ zero) zero → (λt:Nat. Elim[Nat, A”] (t) {…}) (succ zero) zero

TL の性質 ι簡約の例 plus (succ zero) zero → (λt:Nat. Elim[Nat, A”] (t) {…}) (succ zero) zero → β Elim[Nat, A”] (succ zero) {…} zero

Elim[Nat, A”] (succ t) {B0; Bs} TL の性質 ι簡約の例 plus (succ zero) zero → (λt:Nat. Elim[Nat, A”] (t) {…}) (succ zero) zero → β Elim[Nat, A”] (succ zero) {…} zero →ι (λt:Nat. λt’:Nat. succ (plus t t’)) zero zero Elim[Nat, A”] (succ t) {B0; Bs} →ι Bs t

TL の性質 ι簡約の例 plus (succ zero) zero → (λt:Nat. Elim[Nat, A”] (t) {…}) (succ zero) zero → β Elim[Nat, A”] (succ zero) {…} zero →ι (λt:Nat. λt’:Nat. succ (plus t t’)) zero zero →β (λt’:Nat. succ (plus zero t’)) zero →β succ (plus zero zero) → succ ((λt:Nat. Elim[Nat, A”] (t) {…}) zero zero) →β succ (Elim[Nat, A”] (zero) {…} zero)

Elim[Nat, A”] (zero) {B0; Bs} TL の性質 ι簡約の例 plus (succ zero) zero → (λt:Nat. Elim[Nat, A”] (t) {…}) (succ zero) zero → β Elim[Nat, A”] (succ zero) {…} zero →ι (λt:Nat. λt’:Nat. succ (plus t t’)) zero zero →β (λt’:Nat. succ (plus zero t’)) zero →β succ (plus zero zero) → succ ((λt:Nat. Elim[Nat, A”] (t) {…}) zero zero) →β succ (Elim[Nat, A”] (zero) {…} zero) →ι succ ((λt’:Nat. t’) zero) Elim[Nat, A”] (zero) {B0; Bs} →ι B0

TL の性質 ι簡約の例 plus (succ zero) zero → (λt:Nat. Elim[Nat, A”] (t) {…}) (succ zero) zero → β Elim[Nat, A”] (succ zero) {…} zero →ι (λt:Nat. λt’:Nat. succ (plus t t’)) zero zero →β (λt’:Nat. succ (plus zero t’)) zero →β succ (plus zero zero) → succ ((λt:Nat. Elim[Nat, A”] (t) {…}) zero zero) →β succ (Elim[Nat, A”] (zero) {…} zero) →ι succ ((λt’:Nat. t’) zero) →β succ zero ■

TL の性質 証明されている定理 β, η, ιの簡約について、以下を満たす また、論理の無矛盾性も証明可能 Preservation 簡約が judgement を保存する 全ての型付けされた項は強正規性を持つ すなわち、簡約が必ず停止する Church-Rosser 性 (合流性) βηι同値な項を簡約すると、同一の正規形に簡約される また、論理の無矛盾性も証明可能 ├ A: False となる項 A は存在しない ただし、False: Kind = Πk:Kind. k である 健全性を保証

Computation Language λH λ計算ベース 整数(n) と bool 値(tt, ff) パッケージ (<X=A, e:A’>, open…) タプル (<e0,…,en-1>, sel) If-then-else

Computation Language λH 意味論はほぼ自明なので省略 証明のために一部 [A] などが加えられている Λ(大文字に注意!)は型多相を表す 式の型定義 Ω 明らかに帰納的

Computation Language λH If [B, A](e, X1.e1, X2.e2) の意味は? 意味論より e は分岐条件 (bool 値に評価される式) A は B に関する証明を与える つまり B true または B false の証明 A : Bool→Kind X1, X2 は証明を格納される型変数 これにより、分岐においてどういう性質が用いられたかを 下のレベルに伝播させる sel などのプリミティブが内部で活用

Computation Language λH 式と型の間の対応をとるために Singleton Type を使用する 一つの自然数 A に対して一つの型 snat A が対応 snat A に対しパッケージ <t=A, e: snat t> が nat 型を持つ nat : Ω = ∃t:Nat. snat t 演算の表現  add = λx1:nat. λx2.nat. open x1 as <t1, x1’> in open x2 as <t2, x2’> in   <t = plus t1 t2, x1’+x2’ : snat t> 型と値の一対一対応

Example: Bound Check Elimination vec : Nat→Ω→Ω vec = λt:Nat. λt’:Ω. tup t (nth (repeat t t’)) nth, repeat はリスト上の操作 Inductive List : Kind := nil : List | cons : Ω→List→List repeat : Nat→Ω→List repeat zero = λt’:Ω. nil repeat (succ t) = λt’:Ω. T’::(repeat t) t’ nth : List→Nat→Ω nth nil = λt:Nat. void nth (cons t1 t2) = λt:Nat. ifez t Ω t1 (nth t2) tup : Nat→(Nat→Ω)→Ω

Example: Bound Check Elimination 自然数のタプルをとり要素の和を返す関数 sumVec sumVec : ∀t:Nat. snat t→vec t nat→nat = Λt:Nat. λn:snat t. λv:vec t nat.   (fix loop: nat→nat→nat. λi:nat. λsum:nat. open i as <t’, i’> in  if [LTOrTrue t’ t, ltPrf t’ t]  (i’ < n,    t1. loop (add i 1) (add sum (sel[t1](v, i’))),    t2. sum)) 0 0 タプルの範囲外をアクセスしないことを保証したい LTOrTrue, ltPrf を与えることによる

Example: Bound Check Elimination LTOrTrue LTOrTrue : Nat→Nat→Bool→Kind LTOrTrue = λt1:Nat.λt2:Nat.λt:Bool. Cond t (LT t1 t2) True Cond : Bool→Kind→Kind→Kind Cond(true) = λk1:Kind.λk2:Kind. k1 Cond(false) = λk1:Kind.λk2:Kind. k2 True : Kind = Πk:Kind. k→k ↑ True の証明としては恒等関数が与えられる ltPrf A A’ A < A’ ならば LT A A’ の証明(= 型)を返す A ≧ A’ の場合は特に何も返す必要はない そのために True を用いる

Example: Bound Check Elimination LT : Nat→Nat→Kind LT zero (succ t) LT t t’ ⇒ LT (succ t) (succ t’) 証明スケッチ if が true に分岐した場合について LT t’ t が成立していることが内部の式に伝播 sel においてその証明を用いられ、タプルの長さを超えたアクセスをしないことを証明する If が false に分岐した場合 True が渡されるが、これは情報を持たない

Proof-Preserving Compilation CPS Conversion λH を、下記の定義で表される λK に変換 Let-binding と conditional branch の sequence で構成されるプログラム λH, λK いずれも計算言語は帰納的に定義 証明を記述する型言語 TL は共通 式の型(: Ω) が変化するが、簡単に変換可能

Proof-Preserving Compilation CPS Conversion λK の型 ΩK λH に対する Ω とほぼ同じだが、CPS 変換後のコードは戻り値を持たないので、→ の定義が変化 Ω では →: Ω→Ω→Ω ΩK では →: ΩK→ΩK Ω と ΩK の対応

Proof-Preserving Compilation 要するに Kind, Kscm (定理の記述) Ω いろいろな型 ΩK λH λK 変換!

まとめ Certified Binary のための型付き言語を設計 この定義のもと、記述された性質を保存する プログラム変換を定義した Dependent Type の理論を応用し、高階述語論理と同等の記述性を持つ 型の簡約について強正規性が成り立ち、したがって検証は決定可能である 計算言語には自由度があり、Ω を設計すれば容易に組み込むことができる この定義のもと、記述された性質を保存する プログラム変換を定義した CPS 変換, Closure 変換

参考文献 G. Necula. Proof-Carrying Code. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 106-119, 1997. A. W. Appel. Foundational Proof-Carrying Code. In Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS), p. 247, 2001. Wikipedia. Intuitionistic Type Theory. http://en.wikipedia.org/wiki/Intuitionistic_Type_Theory