ASIAN’03 報告

ASIAN 2003 報告
前田俊行
Achieving Type Safety
for Low-Level Code
• Cyclone プロジェクトの現状について
– Cyclone = 安全な C 言語の方言
• C プログラマが書きたくなるようなメモリ操作を型付けしたい
– 様々なポインタ型の導入 *, ?, @, zero-terminated pointer
• その上で、既存の C コードはなるべく簡単に使いまわしたい
• 様々なプログラム解析技術を結集
– Region inference
– Linear type (alias analysis)
– など
– どうやらOSを書くのに使いたい、らしい
• http://www.cs.cornell.edu/projects/cyclone/
Self-configurable Mirror Servers for
Automatic Adaptation
• クライアントからの要求の増減に自動的に適応して
サーバ数を調節するシステムの研究
– P2P型のシステム
• 暇なノードは近隣ノードに「暇なんですけど」と宣伝する
• 忙しいノードは暇なノードに「働いて下さい」とお願いする
– スケーラブル
– No single point of failure
– 宣伝やお願いを発行するポリシーをプログラミングできる
– ちゃんと上手く動くっぽい実証データあり
(ただしシミュレーション)
シミュレーション実験
• ミラーサーバ群で2種類のサービスA, B を提供
• クライアントからのサービス要求を動的に変化さ
せて以下の数字を計測
– サービスを実行しているノード数
– 1ノードあたりのアクセス数
– など
• ポリシー
– 実験1ではサービスA, Bとも同優先度
– 実験2ではサービスB の優先度を上げてある
実験1の結果 (ノード数のみ)
実線: サービスA
点線: サービスB
P2Pシステムでも
動的適応できた
実験2の結果 (ノード数のみ)
実線: サービスA
点線: サービスB
P2Pシステムでも
優先度づけできた
Unreliable Failure Detectors
via Operational Semantics
• Unreliable FDs (failure detectors) という分
散アルゴリズムの解析手法をスモールステッ
プ operational semantics で言い換えてみま
したという研究
– 言い換えによって見通しがよくなる、らしい
– 言い換えが正しいことが証明してある
Failure Detector: FD
• FD = (F, H)
• F : T(time) → 2P
failure pattern
(例) F(42) = { 3, 7 } ⇒ 時間 [0, 42] の間にプロセス
3と 7 がクラッシュする
• H : T × P → 2p
failure detector histories
(例) H(42, 5) = { 6, 7 } ⇒ 時間 42 においてプロセ
ス 5 はプロセス 6 と 7 がクラッシュしていると考える
• 上記 H は F と違っていてもよい = Unreliable
FDの性質
• Completeness と Accuracy であらわす
• Completeness
– クラッシュしたプロセスを suspect すること
• Accuracy
– クラッシュしていないプロセスを suspect しないこと
プロセス i がプロセス j を suspectする =
j ∈H (t, i)
2種類のCompleteness
crashed(F) = ∪tF(t)
correct(F) = P＼crashed(F)
8種類のAccuracy (1)
8種類のAccuracy (2)
Operational Semantics Scheme
N = 全プロセスの状態
Γ = (TI, C)
TI = trusted-immortal processes
C = crashed processes
Operational Semantics Scheme
? @ i = プロセス i が何かアクション ? を実行する、という意味
suspect j @ i = プロセス i はプロセス j はクラッシュしたと見なす
Operational Semantics Scheme
condition χ (Γ, j) = 要求する accuracy によって異なる
Operational Semantics
Eventual weak accuracy をいうには◇-SUSPECT に加え、
∃t. (TIt, Ct) Nt with TIt ≠ 0
を満たす必要がある
Operational Semantics
Eventual strong accuracy をいうには◇-SUSPECT に加え、
∃t. (TIt, Ct) Nt with TIt ∪ Ct = 全プロセス
を満たす必要がある
Deaccumulation
- Improving Provability
• Accumulate されたプログラムの自動検証は難しいので、自
動的に元のプログラムに変換する方法の研究
(例)
– P : f (S x1) y1 y2 = f x1 (S (S y1)) (y1 : y2)
f 0
y1 y2 = y2
– A : g x1 = f x1 []
を、以下のように deaccumulate する
– D : f (S x1) = sub (f x1) (S (S 0)) (0 : [])
f 0
= []
• 方法: 1-state macro tree transducer を homomorphismsubstitution modular tree transducer に変換する
A Calculus for Secure Mobility
• Crypto-loc calculus という安全なモバイル計算のモデル
(プロセス計算)を提案
– 以下の3つの概念をまとめて導入している
• Location
• Code mobility (weak mobility)
• Cryptography
– Observational equivalence でセキュリティプロパティを定義
– さらにセキュリティプロパティの証明のために labeled
bisimilarity というものを定義
• Observational equivalence == Labeled bisimilarity を証明した
Syntax: terms
Syntax: processes
Structural Equivalence
Reduction Relations
Observational Equivalence
ここで P↓a とはプロセスPが(チャネル) a に何か output すること
C はいわゆる evaluation context
また、C{P} が closed なとき
C は P のclosing evaluation context であるという
Labeled Semantics
～
ここで A (agent) = (νa)(σ,P)
σ(= substitution from variables to terms) : “敵”が知り得るデータ
a : “敵”が知らない names
Labeled Semantics … 続き
Labeled Bisimilarity … の準備
Labeled Bisimilarity

Download Report