2000 Fiscal Year Annual Research Report
| Project/Area Number |
12133202
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research on Priority Areas (B)
|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
小林 直樹 東京工業大学, 大学院・情報理工学研究科, 助教授 (00262155)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
五十嵐 淳 東京大学, 大学院・総合文化研究科, 助手 (40323456)
|
|---|
| Keywords | 型システム / セキュリティ / 並行プログラム / 安全性 / ライブロック / Java |
|---|
| Research Abstract |
近年のコンピュータネットワークの普及により,信頼できない相手からソフトウェアがWWWや電子メールを介して受け取る機会が増えている.本研究の目的は,そのような状況において受け取ったソフトウェアが既存のシステムに危害を及ぼさないことを型システムを用いて静的に保証することである.本年度の研究成果は以下の通り.
1.並行プログラムのための統一的型システムの考案
前年度までに特定の性質を保証するための型システムを数種類構築することに成功したが,現実には保証したい性質はシステムごとに異なり,保証する性質ごとに検証システムを構築するのは非現実的である.そこで,さまざまな性質を統一的に検証するための型システムを考案した.この型システムに基づいて検証システムを構築すれば,一部を変更するだけで,さまざまな性質を検証することが可能になる.
2.ライブロックフリーダムを保証する型システムの考案
並行プログラムにおいて,特定の通信がいずれ必ず成功することを保証する型システムを構築した.さらにその発展として,一定時間内に通信が必ず成功することを保証する型システムも構築した.
3.考案済みの型システムの現実のプログラミング言語への応用
前年度までに考案した個々の性質を保証するための型システムの現実のプログラムに対する有効性を検証し,必要であれば上記統一的型システムに改良を加えるために,現実のプログラミング言語に適用する試みを開始した.具体的には(1)並行プログラミング言語CMLのためのデッドロックフリーダムの検証器の構築,(2)Java言語のバイトコード中でのオブジェクトのロックの獲得・解放の整合性を検査するシステムの構築を開始した.
|
-
[Publications] A.Igarashi and N.Kobayashi: "Type Reconstruction for Linear Pi-Calculus with I/O Subtyping"Information and Computation. 161. 1-44 (2000)
-
[Publications] Naoki Kobayashi: "Type Systems for Concurrent Processes : From Deadlock-Freedom to Livelock-Freedom, Time-Boundedness"Proceedings of IFIP TCS2000, Springer LNCS. 1872. 365-389 (2000)
-
[Publications] N.Kobayashi,S.Saito,and E.Sumii: "An Implicitly-Typed Deadlock-Free Process Calculus"Proceedings of CONCUR2000, Springer LNCS. 1877. 489-503 (2000)
-
[Publications] A.Igarahi and N.Kobayashi: "A Generic Type System for the Pi-Calculus"Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages(POPL2001). 128-141 (2001)
