2002 Fiscal Year Annual Research Report
| Project/Area Number |
12133202
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
小林 直樹 東京工業大学, 大学院・情報理工学研究科, 助教授 (00262155)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
五十嵐 淳 京都大学, 大学院・情報学研究科, 講師 (40323456)
|
|---|
| Keywords | 型システム / セキュリティ / 並行プログラム / 安全性 / 定理証明支援器 / Java / 情報流解析 / Coq |
|---|
| Research Abstract |
近年のコンピュータネットワークの普及により,信頼できない相手からソフトウェアがWWWや電子メールを介して受け取る機会が増えている.本研究の目的は,そのような状況において受け取ったソフトウェアが既存のシステムに危害を及ぼさないことを型システムを用いて静的に保証することである.本年度の研究成果は以下の通り.
1.計算資源に対するアクセス方法の正しさの検証のための型システムの改良と実装
計算機システムにおいては,プログラムは記憶領域(メモリ),ネットワーク,CPU,ファイルなどさまざまな資源を共有して動作しており,あるプログラムが不正に資源にアクセスを行うと,計算機システム全体の動作に悪影響を与える.そこで昨年度我々は,プログラムが正しいプロトコルで資源にアクセスすることを検証するための型システムをに開発した.本年度は,その型システムを改良するとともに,具体的な応用例としてJavaのバイトコードが正しくロックの獲得と解放を行っているかを検査するための検証器を作成した.
2.低レベル言語のための情報流解析の型システムの拡張と実装
昨年度研究を行ってきたJavaのバイトコードがパスワードなどの機密情報を漏らさないかを検査するための型システムを拡張し,実装を行った.
3.メールサーバの形式的検証
定理証明支援システムCoqを用い,メールサーバプログラムのモデル化および検証を行った.
|
-
[Publications] Naoki Kobayashi: "Time regions and effects for resource usage analysis"Proceedings of ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (TLDI'03). 50-61 (2003)
-
[Publications] F.Iwama, N.Kobayashi: "A New Type system for JVM Lock Primitives"Proceedings of ACM SIGPLAN Workshop on Asia-PEPM'02. 156-168 (2002)
-
[Publications] R.Affeldt, N.Kobayashi: "Verification of a Mail Server in Coq"Software Security -Theories and Systems, Springer LNCS. (出版予定). (2003)
-
[Publications] Atsushi Igarashi, Mirko Viroli: "On Variance-Based Subtyping for Parametric Types"Proceedings of the Sixteenth European Conference on Object-Oriented Programming (ECOOP2002), Springer LNCS. 2374. 441-469 (2002)
-
[Publications] 山本 和樹, 岡本 暁広, 五十嵐淳, 佐藤 雅彦: "擬似引用を持つ型付計算体系λq"日本ソフトウェア科学会第5回プログラミングおよびプログラミング言語ワークショップ(PPL2003)論文集. 87-102 (2003)
-
[Publications] 小林 直樹, 白根 慶太: "低レベル言語のための情報流解析のための型システム"コンピュータソフトウェア. 2(出版予定). (2003)
