移動コードを基本としたセキュアなプログラミング言語処理系

2000 年度 実績報告書

• 研究課題/領域番号: 12133203
• 研究種目: 特定領域研究(B)
• 研究機関: 東京大学
• 研究代表者: 米澤 明憲 東京大学, 大学院・理学系研究科, 教授 (00133116)
• 研究分担者: 遠藤 敏夫 東京大学, 大学院・理学系研究科, 日本学術振興会特別研究員(DC2) ; 田浦 健次朗 東京大学, 大学院・理学系研究科, 助手 (90282714) ; 増原 英彦 東京大学, 大学院・総合文化研究科, 講師 (40280937) ; 住井 英二郎 東京大学, 大学院・理学系研究科, 日本学術振興会特別研究員(DC1)
• キーワード: 細粒度保護機構 / 保護モデル / 暗化λ計算 / プログラム検証 / 通信秘密性 / 移動コード / バイトコード変換 / 仮想機械

研究概要

本年度は、安全性や移動コードに関する基本的な技術の研究を行った。その成果は以下の3つに大別できる:
[プログラムを安全かつ効率的に実行するための保護機構の研究]
これまでの研究において、「異なる開発者の手によるプログラム部品が1つのメモリ空間上で混在して実行される」プログラム部品間の安全性をきめ細く保証する保護機構の研究を行ってきたが、それを拡張し、「異なる実行者のスレッドが混在して実行される」状況下で、スレッド間の安全性を保証する保護モデルを提案し、機械語書き換え技術によって効率的に実現する方法を示した。
[プログラムが行う通信の秘密性のための計算系と解析手法の研究]
暗号化技術を用いたプログラムが情報を漏らさないことを保証するための計算系-暗号λ計算-と解析手法を提案した。解析手法としては「暗号化された値を置き換えてもプログラムの結果が変わらない」ような論理関係によって秘密性を定義し、この論理関係を、プログラムの型に関する帰納法によって証明する。これにより、他のプログラムとともに実行した場合でも秘密が保たれることが証明できる。
[移動コードに関する基本技術の深化]
これまで移動コードに関する研究を進め(1)例外処理などの既存の言語機能を利用することでプログラムを移動可能にする手法の提案とその実現方式(2)プログラムの実行時に、プログラムの実行環境に応じたコンパイルや特化を行うことで効率を改善する手法の提案(3)安全性や耐故障性の解析を行うための移動可能言語の設計(4)効率的かつ移植性の高い仮想機械語の設計、といった成果を得た。

研究成果

• [文献書誌] Hashimoto,Yonezawa:: "MobileML : A Programming Language for Mobile Computation"International Conference on Coordination Languages and Models (COORDINATION 2000). LNCS1906. 198-215 (2000)
• [文献書誌] Sakamto,Sekiguchi,Yonezawa: "Bytecode Transformation for Portable Thread Migration in Java"Agent Systems, Mobile Agents, and Applications (ASAMA2000). LNCS1882. (2000)
• [文献書誌] Masuhara,Sugita,Yonezawa:: "Dynamic Compilation of a Reflective Language Using Run-Time Specialization"International Symposium on Principles of Software Evolution (ISPSE2000). 125-134 (2000)
• [文献書誌] Sekiguchi,Sakamoto,Yonezawa: "Portable Implementation of Continuation Operators in Imperative Languages by Exception Handling"Advances in Exception Handling Techniques. (発表予定). (2001)
• [文献書誌] Sekiguchi,Yonezawa: "A Code Representation for Heterogeneous Mobile Computation and its Implementation"Transactions of Information Processing Society of Japan. (発表予定). (2001)
• [文献書誌] Masuhara,Yonezawa: "Run-time Bytecode Specialization : A Portable Approach to Generating Optimized Specialized Code"Second Symposium on Programs as Data Objects (PADO-II). (発表予定). (2001)