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 Accuracy クラッシュしたプロセスを 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 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 を homomorphism-substitution 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) ～ ここで A (agent) = (νa)(σ,P) σ(= substitution from variables to terms) : “敵”が知り得るデータ a : “敵”が知らない names

Labeled Semantics … 続き

Labeled Bisimilarity … の準備

Labeled Bisimilarity