TOKYO TECH CYBERSECURITY

西崎研究室の研究テーマ

検証

・ブロードキャスト通信を行う分散システムに対するモデル検査これまでのモデル検査システムにおいては，検証されるモデルの記述は，状態遷移図，もしくは，プロセス間の一対一通信機構や変数の共有機構をもつ並行プログラミング言語により記述する必要があった。したがって，ブロードキャストを通信手段とする分散システムは，そのようなモデル記述言語では直接記述することはできない。本研究では，ブロードキャスト通信に対してモデル検査を適用する手法を提案した。

・モデル検査と離散シミュレータを用いた統合的な検査環境モデル検査は，検証対象となるシステムを，抽象化・単純化してモデル化することが必須である。抽象化の過程において，現実のシステムと，抽象化されたモデルとの間でギャップが生じ，モデル検査の検査結果が，現実のシステムにおける意味を理解することが困難となることがある。このような問題に対し本研究は，モデル検査とネットワークシミュレータ NS2 を用いた離散シミュレーションとを統合的に用いたシステムの検証環境を提案した。

DoS 攻撃耐性

・プロトコルのサービス不能攻撃耐性解析のための計算系
安全性を必要とするプロトコルにおいて，形式的な手法について盛んに研究されてきたが，それらの研究は，主に認証性，完全性，機密性に関するものであった．サービス不能攻撃 (DoS 攻撃 ) とは，サーバーが本来のサービスを提供することを妨害するような攻撃であり，近年深刻化している．大量のアクセスによるサービス妨害が典型的なものであるが，TCP の SYN 溢れ攻撃のように，プロトコルがもつ設計上の欠陥を悪用するようなサービス不能攻撃もあり，この種の DoS 攻撃を本研究では研究対象とした。
本研究では，プロトコルが持つサービス不能攻撃耐性を解析するための計算体系として，"spice 計算" を提唱した。これは並行計算のモデルであるπ計算を応用したものであり，型システムを応用することにより，計算機毎のコストを解析することを可能していることが特徴である。例として，TCP の SYN 溢れ攻撃の他，その防御法 "SYN-cookie 法" を spice 計算の下で形式的に記述することを通じて，その有用性を示した。

環境計算

・単純型付環境計算
本研究では，単純型付λ計算にファーストクラス環境を組み込んだ体系，単純型付環境計算を提唱し，その解析を行なった．単純型付λ計算とは，型変数と関数型からなる型をもつような関数型プログラミング言語のモデルであり，型理論のうちで最も基本的なものである。型理論に関する基本的性質である，主部簡約定理 ( 簡約において型が保存されること，型 付けの健全性 ) と強正規化可能性定理 ( 型が付いている式は簡約が必ず停止すること ) とを示した。また，単純型理論に関する型推論アルゴリズムを与え，その基本的性質である健全性 ( 求めた型付けの正当性 )，完全性 ( 型付けが存在するならば必ず答が出力される )，主要型付け定理 ( 求めた答えが最も一般的であること ) を証明した．また，合流性 ( どのような順番で簡約しても結果は同じになるということ ) は，単純型付環境計算において示したが，これは，型なし環境計算の合流性としても読み替えることができる。

・ML 多相環境計算
ML 多相型体系は，プログラミング言語 ML の型体系として広く知られている。
この型体系に基づく環境計算を提唱しその基本的性質を解明した．主部簡約定理を示し，型推論アルゴリズムを与え，主要型付け定理を証明した．通常のλ計算においても，ML 多相型体系に対する型推論アルゴリズムは，単純型体系に対する型推論アルゴリズムより複雑であり，その主要型付け定理の証明も複雑であることが知られている。また，λ計算における ML 多相性は，let 式で束縛される式に関する多相性であるが，ML 多相環境計算では，環境の束縛における多相性として与えられており，従来の ML 多相性と比べて真に拡張がなされている。

継続計算と線形論理

・継続計算と線形論理
プログラミング言語において，継続とは，計算の残りの部分を意味し，処理系においては実行時のスタックに対応する概念である．Scheme 等のプログラミング言語では，整数値や論理値のように関数の引数にしたり返値にしたりすることが可能となっており，「ファーストクラス継続」と呼ばれる。ファーストクラス継続をもつプログラミング言語のモデルである継続計算に関して，数理論理学的な分析を行なった。具体的には，計算結果である " 値 " と計算の残りである " 継続 " との対称性が，線型論理の否定として捉えられることを示した。言い換えると，本研究は，型付λ計算と直観主義論理との対応関係である Curry-Howard 同型の概念を，継続計算と線型古典論理と対応関係にまで拡張したものである。