PC`, TC

Static Enforcement of Security
with Types
情報理工米澤研 M1
田渕直
概要
• 現行の 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 のとり方にも依
存。
例
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
{}
1. ├A id : t → t
2. ├ pλg.g(id) : (τ → t’)
ρ
ρ
→
t’
A
id
/ {ρ⊑ 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’
– τ →Πτ <: τ’ → τ’Π’∊ TC ⇒
1
2
1
2
τ’1<:τ1, τ2<:τ’2 ∊ TC’
– τ1<:τ2, τ2<:τ3 ∊ TC’ ⇒ τ1<:τ3 ∊ TC’
を満たす最小の TC’
• 直感的には、Fig.4 の subtype relation により、
TC が暗黙に満たすべき制約を明示したもの。
充足可能性 (2/3)
• 型の制約は、権限に関する制約を含む。
具体的には
τ1→Π τ2 <: τ’1→ τ’Π’2 ∊ TC ⇒ Π ⊑ Π’
• これをまとめた集合を、
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 が
– 権限の変数 (ρi) を含まず
– S, A├ e → v
– [Π] ⊆ {π| inspect(S, π, A) = true}
ならば、Γ,Π,p├A v : τ/ PC, TC
型システムの不完全性
•
明らかに安全なプログラムが型付けでき
ないこともある。
1. 項が使用されない場合
e.g. pλx. checkprive π for x (π∉ A(p) )
2. 到達しない条件分岐
e.g. pλx. if false then
checkprive π for x else x
3. その他、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

Download Report