Static Enforcement of Security with Types

概要 現行の JDK のセキュリティアーキテクチャに替わる、セキュリティの為の型システムを提案する。

現行システムの問題点 現在の JDK のアーキテクチャでは… セキュリティチェックをメソッド呼出しとして実現 チェックは実行時 読みにくい 間違いやすい チェックは実行時 効率が悪い コンパイラの最適化の邪魔

この論文の提案 JDK のセキュリティと同等のことを、静的に行いたい。 そのために、型システムを使う。 ⇒ 読みやすさ・効率の良さを同時に実現。

論文の内容 セキュリティの為の型システム 対象は Java の Stack Inspection Stack Inspection の形式化 型システムの定義と安全性の証明 型推論アルゴリズム など

Stack Inspection の形式化 (1/2) 言語 λsec (Fig. 1) λ計算に権限チェックのprimitiveを追加 Princ: コード所有者(principal)の集合 Privs: 権限(privilage)の集合 letpriv/checkpriv A: 各所有者の持つ権限への写像 S: Security Stack. 所有者と権限の集合のペア<p, P> のリスト

Stack Inspection の形式化 (2/2) 「安全な」プログラム ⇔ Fig. 2 の operational semantics で secfail にならない。 より具体的には、checkpriv で指定されたチェックが失敗しない。 チェックは inspect アルゴリズムで行われる。

Top level stack プログラム実行の出発点として、トップレベルの所有者 pιとスタック Sι= <pι,Pι>::nil を仮定する。ただし Pι = A(pι)

Inspect アルゴリズム 権限 π を要求する操作が実行可能か、スタックを辿ってチェックする。 inspect(nil, π, A) = false inspect(<p, P>::S, π, A) = if π∉ A(p) then false else if π∊ P then ture else inspect(S, π, A) プログラムの「安全性」は A のとり方にも依存。

例 cp id は常に secfail (lp cp) id は A(p) のとり方による。 id = pλx.x lp = pλf.λx. letpriv π in f x cp = pλx. checkprive π for x cp id は常に secfail (lp cp) id は A(p) のとり方による。

λsec のセキュリティ型 λsec に型システムを導入。 「Well-typed なプログラムは stack inspection で失敗しない」ことを、subject reduction により示す。

型システムの構文 制約ベースの型システム 構文は Fig. 3 関数型に付く privstruct Π は、その関数が必要とする権限の集合 PC は、各Π が満たすべき、権限に関する制約 TC は通常の型に関する制約

例 型付け規則は Fig. 5 {} ├A id : t → t ρ ρ ├A pλg.g(id) : (τid → t’) → t’ / {ρ⊑ A(p) } 2. では g の必要とする権限が具体的に分からないので、変数 ρ を当てている。

代入と解釈 (1/2) 代入 S = {P1/ρ1 … Pn/ρn} は Π の中の変数 ρi を具体的な権限で置き換える。 解釈 [Π] は privstruct Π が表す具体的な権限の集合を与える。形式的な定義は [P] = P [Π1⊔Π2] = [Π1]∪[Π2] [Π⊝ P] = [Π] - [P] [ρ] = undefined

代入と解釈 (2/2) 用語の定義 Π ∊ Dom(S) ⇔ [SΠ] が defined Π ⊆ Π’ ⇔ Π,Π’ ∊ Dom(S) である任意のSについて、[SΠ] ⊆ [SΠ’] π ∊ Π ⇔ Π ∊ Dom(S) である任意のSについて、 π ∊ [SΠ] S ≤ S’ ⇔ Π ∊ Dom(S)∩ Dom(S’) である任意のΠについて、 [SΠ] ⊆ [S’Π]

充足可能性 (1/3) 型の制約 TC の closure、close(TC) とは TC ⊆ TC’ Π Π’ τ1→ τ2 <: τ’1→ τ’2 ∊ TC ⇒ τ’1<:τ1, τ2<:τ’2 ∊ TC’ τ1<:τ2, τ2<:τ3 ∊ TC’ ⇒ τ1<:τ3 ∊ TC’ を満たす最小の TC’ 直感的には、Fig.4 の subtype relation により、TC が暗黙に満たすべき制約を明示したもの。

充足可能性 (2/3) 型の制約は、権限に関する制約を含む。具体的には これをまとめた集合を、 で定義。 scs(TC) = {Π ⊑ Π| Π Π’ τ1→ τ2 <: τ’1→ τ’2 ∊ TC で定義。

充足可能性 (3/3) 定義: ペア PC, TC が充足可能 ⇔ PC∪scs(close(TC)) に含まれる、全ての 制約Π1 ⊑ Π2 について、[SΠ1] ⊆ [SΠ2] を満たす S が存在。

型の妥当性 定義: Γ,Π,p├A e : τ/ PC, TC がvalidとは ⇔ PC∪｛Π⊑ A(p)}, TC のペアを、前項の意味で充足するような代入 S が存在すること。 すなわち、推論でできた制約と、p に与えられた権限に矛盾しないような権限の集合が作れること。

略記方 {},Π,pι├A e : τ/ PC, TC を、 ├A e : τ/ PC’, TC のように略記することとする。 ただし、 PC’ = PC∪｛Π⊑ A(pι)}

セキュリティ型の安全性 (1/2) 定理:├A e : τ/ PC, TC が valid ならば、Sι,A├ e → secfail となることはない。 すなわち、closed, well-typed なプログラムは secfail にならない。 証明は subject reduction による。

セキュリティ型の安全性 (2/2) Subject reduction: Γ,Π,p├A e : τ/ PC, TC が S, A├ e → v [Π] ⊆ {π| inspect(S, π, A) = true} ならば、Γ,Π,p├A v : τ/ PC, TC

型システムの不完全性 明らかに安全なプログラムが型付けできないこともある。 項が使用されない場合 e.g. pλx. checkprive π for x (π∉ A(p) ) 到達しない条件分岐 e.g. pλx. if false then checkprive π for x else x その他、polymorphism が必要な場合など。

セキュリティ型の型推論 人手で型の annotation を付けるのでは型システムの魅力が半減なので、型推論のアルゴリズムを導入する。 アルゴリズムは、プログラム e を受け取って τ/ PC, TC を返す。 具体的な定義は Fig. 6, 7。

型推論アルゴリズムの性質 (1/3) 型推論アルゴリズム infer_secty の性質: 推論の結果は正しい。 推論で型が返されたら、それは最も「一般的な」型である。

型推論アルゴリズムの性質 (2/3) 型推論は正しい infer_secty(e) = τ/ PC, TC ⇔ ├A e : τ/ PC, TC は valid o.w. infer_secty(e) = sectyfail

型推論アルゴリズムの性質 (3/3) 推論の結果は最も一般的 infer_secty(e) = τ/ PC, TC ならば、任意の valid な導出├A e : τ’/ PC’, TC’ は、 何らかの型代入と権限の代入 Θ,S によって├A e :τ/ PC, TC から得られる。

まとめ JDK の実行時 stack inspection に替わる型システム 型システムの健全性の証明 型推論アルゴリズム

Future woks 型システムの拡張 (polymorphism etc.) JDK の他のアーキテクチャを含むセキュリティモデル 実用的な言語の開発

Related works (1/2) Static Enforcement of Security with Types. ICFP'00. Christian Skalka and Scott Smith. Java Security Architecture (JDK 1.2). L. Gong, http://java.sun.com/products/jdk/1.2/docs/guide/security/spec/security-spec.doc.html

Related works (2/2) Typed memory management in a calculus of capabilities. K. Crary, D. Walker and G. Morriset, Conference Record of the 26th Annual ACM Symp. on POPL, 1999 Safe kernel extensions without run-time checking. G.C. Necula and P. Lee, In 2nd Symp. on Operating System Design and Implementation, 1996