2003 Fiscal Year Annual Research Report
| Project/Area Number |
12133202
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
小林 直樹 東京工業大学, 大学院・情報理工学研究科, 助教授 (00262155)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
五十嵐 淳 京都大学, 大学院・情報学研究科, 講師 (40323456)
|
|---|
| Keywords | 型システム / セキュリティ / 並行プログラム / 安全性 / 定理証明支援器 / 様相論理 / 情報流解析 / Coq |
|---|
| Research Abstract |
近年のコンピュータネットワークの普及により,信頼できない相手からソフトウェアがWWWや電子メールを介して受け取る機会が増えている.本研究の目的は,そのような状況において受け取ったソフトウェアが既存のシステムに危害を及ぼさないことを型システムを用いて静的に保証することである.本年度の研究成果は以下の通り.
1.情報流解析の拡張・改良とそれに基づく検証器の実装
並行プログラムが機密情報を漏らさないかどうかを解析するための一般的な型システムを構築し,その正しさを証明した.ロックや通信などの並行プリミティブを扱ったプログラムについて,情報漏洩の可能性を既存の並行プログラムの情報流解析と比べてより正確に判定することができる.
2.並行プログラムの検証のためのCoqライブラリの構築:
Coqなどの定理証明器を用いてプログラムの検証を行うことができるが,メールサーバのような並行プログラムの検証を定理証明器を用いて一から行うためには多大な労力が必要となり,現実的ではない.そこで,Coqを用いた並行プログラムの検証を容易にするためのライブラリを構築した.
3.様相論理に基づく情報流解析の理論
近年,型システムに基づく情報流解析手法が多数提案されているが,それらは対象言語毎に少しずつ異なる型システムを設計しているため,手法の細かな比較が困難になっている.そこで我々は,情報流解析の型システムを様相論理の見地から見直し,それら多数の型システムの基礎付けとなるような型システムを考案した.その結果,情報流解析の正当性の証明が,これまで提案された手法に対しての証明よりも,遥かに簡単に行なえることが明らかになった.
|
-
[Publications] Atsushi Igarashi, Naoki Kobayashi: "Resource Usage Analysis"ACM Transactions on Programming Languges and Systems. (出版予定). (2004)
-
[Publications] Atsushi Igarashi, Naoki Kobayashi: "A Generic Type System for the Pi-Calculus"Theoretical Computer Science. 311・1-3. 121-163 (2004)
-
[Publications] 小林 直樹, 白根 慶太: "低レベル言語のための情報流解析のための型システム"コンピュータソフトウェア. 20・2. 2-21 (2003)
-
[Publications] M.Sato, T.Sakurai, Y.Kameyama, A.Igarashi: "Calculi of Meta-variables"Proceedings of Computer Science Logic(CSL'03), Springer LNCS. 2803. 484-497 (2003)
-
[Publications] R.Affeldt, N.Kobayashi: "Verification of a Mail Server in Coq"Software Security-Theories and Systems, Springer LNCS. 2609. 217-233 (2003)
-
[Publications] 吉林和明, 小林 直樹: "Javaバイトコードのための情報流解析"オブジェクト指向シンポジウム2003論文集. 201-202 (2003)
