2001 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 / 情報流解析 |
|---|
| Research Abstract |
近年のコンピュータネットワークの普及により,信頼できない相手からソフトウェアがWWWや電子メールを介して受け取る機会が増えている.本研究の目的は,そのような状況において受け取ったソフトウェアが既存のシステムに危害を及ぼさないことを型システムを用いて静的に保証することである.本年度の研究成果は以下の通り.
1.計算資源に対するアクセス方法の正しさの検証のための型システムの考案 計算機システムにおいては,プログラムは記憶領域(メモリ),ネットワーク,CPU,ファイルなどさまざまな資源を共有して動作しており,あるプログラムが不正に資源にアクセスを行うと,計算機システム全体の動作に悪影響を与える.本研究では各プログラムが正しいプロトコルで資源にアクセスすることを検証するための型システムの確立に成功した.この型システムを用いることにより例えば,(1)新たにメモリを獲得したらいずれそのメモリを解放する.すでに解放したメモリ領域への読み書きを行わない,(2)ファイルを開いたらいずれ閉じる.閉じたあとは読み書きを行わない,(3)ある資源にアクセスする前には必ずその資源に関するロックを獲得してから行う.ロックを獲得したらいずれ解放する.
2.低レベル言語のための情報流解析の型システムの考案 上の通信の整合性を検証とする型システムでは,π計算と呼ばれる複数のプロセスが通信チャネルを介して通信して同期をとるモデルを対象としたが,プログラミング言語によっては,Javaのようにロックの獲得・解放を通して同期や排他制御をとるモデルを採用しているものも多い.本研究ではJava言語のバイトコード中でのオブジェクトのロックの獲得・解放の整合性を検査する型システムを考案した.
|
-
[Publications] A.Igarashi, N.Kobayashi: "Resource Usage Analysis"Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages (POPL2002). 331-342 (2002)
-
[Publications] Naoki Kobayashi: "A Type System for Lock-Freedom"Information and Computation. (出版予定). (2002)
-
[Publications] 岩間太, 小林直樹: "JVMにおけるロックの整合圧検証のための新しい型システム"コンピュータソフトウェア. (出版予定). (2002)
-
[Publications] 小林直樹, 白根慶太: "低レベル言語における情報流解析のための型システム"第4回プログラミングおよびプログラミング言語に関するワークショップ(PPL2002)論文集. (出版予定). (2002)
-
[Publications] 浜中信行, 住井英二郎, 小林直樹, 米澤明憲: "Javaバイトコードにおけるオブジェクト使用解析のための型システム"第4回プログラミングおよびプログラミング言語に関するワークショップ(PPL2002)論文集. (出版予定). (2002)
