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 LTOｒTrue 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