| 研究概要 |
近年のコンピュータネットワークの普及により,信頼できない相手からソフトウェアがWWWや電子メールを介して受け取る機会が増えている.本研究の目的は,そのような状況において受け取ったソフトウェアが既存のシステムに危害を及ぼさないことを型システムを用いて静的に保証することである.本年度の研究成果は以下の通り.
1.計算資源に対するアクセス方法の正しさの検証のための型システムの考案 計算機システムにおいては,プログラムは記憶領域(メモリ),ネットワーク,CPU,ファイルなどさまざまな資源を共有して動作しており,あるプログラムが不正に資源にアクセスを行うと,計算機システム全体の動作に悪影響を与える.本研究では各プログラムが正しいプロトコルで資源にアクセスすることを検証するための型システムの確立に成功した.この型システムを用いることにより例えば,(1)新たにメモリを獲得したらいずれそのメモリを解放する.すでに解放したメモリ領域への読み書きを行わない,(2)ファイルを開いたらいずれ閉じる.閉じたあとは読み書きを行わない,(3)ある資源にアクセスする前には必ずその資源に関するロックを獲得してから行う.ロックを獲得したらいずれ解放する.
2.低レベル言語のための情報流解析の型システムの考案 上の通信の整合性を検証とする型システムでは,π計算と呼ばれる複数のプロセスが通信チャネルを介して通信して同期をとるモデルを対象としたが,プログラミング言語によっては,Javaのようにロックの獲得・解放を通して同期や排他制御をとるモデルを採用しているものも多い.本研究ではJava言語のバイトコード中でのオブジェクトのロックの獲得・解放の整合性を検査する型システムを考案した.
|
