| 研究課題/領域番号 |
12133204
|
|---|
| 研究種目 |
特定領域研究
|
| 配分区分 | 補助金 |
|---|
| 審査区分 |
理工系
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
米崎 直樹 東京工業大学, 大学院・情報理工学研究科, 教授 (00126286)
|
|---|
| 研究分担者 |
吉浦 紀晃 群馬大学, 総合情報処理センター, 助教授 (00302969)
西崎 真也 東京工業大学, 大学院・情報理工学研究科, 助教授 (90263615)
米田 友洋 国立情報学研究所, 情報基盤研究系, 教授 (30182851)
友石 正彦 東京工業大学, 大学院・情報理工学研究科, 助手 (60262284)
|
|---|
| 研究期間 (年度) |
2000 – 2003
|
| キーワード | Safety critical system / 仕様解析 / 安全なプログラム合成 / ネットワークの安全性解析 / セキュリティプロトコル / 安全なシステムアーキテクチャ / 暗号方式の安全性 / ハードウェアの安全性 |
|---|
| 研究概要 |
1)Safety critical systemの安全性を保するための検証や合成手法
リアクティブシステムの仕様を解析し、いかなる外部環境の変化に対しても、正しく意図通りに動作するシステムが存在するかどうかを予め調べるための解析方法と、その効率的実装方式を与えた。同様の手法を用いて非同期回路の合成と検証方式についても、効率的な実装を行った。
2)ネットワークの安全性のための形式手法
認証プロトコルの安全性を代数的に或は論理的に行う方注を与えたと同時に、オークションプロトコルで不正行為が行えないことの解析方式を与えた。一方で、証明方法を基にした検証済みの構成方法を、構造用件を基に記述し、これを用いてより少ない計算コストでより安全なプロトコルの自動生成を行えるようにした。さらに、ネットワークサービスに対する脅威となりつつあるサーピス不能攻撃の可能性解析を行う方式を確立した。
3)安全なシステムアーキテクチャの構築
一旦UNIXシステムにセキュリティホールを利用して侵入すると、ネットワークを通じて、他のシステムに侵入することは容易である。ここではUNIXのユーザ切り替え機構にパスワード認証を導入すると同時に、それを迂回しようとする攻撃に対しても耐性のある一般ユーザ権限の保護されたシステムを提案した。
4)基礎理論
より基礎的な研究成果としては、公理的な解釈により暗号方式やハッシュ関数を解析し、各暗号方式、ハッシュ関数を用いた暗号化テキストの部分的な内容が漏れないという安全性を厳密に定義し、それらの十分条件を示した。公理的なアプローチによるこのような性質の解析は、初めての試みである。また、有限時間論理の証明方法を与え、この完全性を証明した。この時間論理のモデルの時間推移関係に関する制約は一階述語論理で記述することが出来ないため、完全な証明方法を構築することは自明では無かった。
|
