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

2001 Fiscal Year Annual Research Report

• Project/Area Number: 12133203
• Research Institution: The University of Tokyo
• Principal Investigator: 米澤 明憲 東京大学, 大学院・情報学環, 教授 (00133116)
• Co-Investigator(Kenkyū-buntansha): 遠藤 敏夫 東京大学, 大学院・情報学環, 特別研究員 ; 住井 英二郎 東京大学, 大学院・情報学環, 助手 (00333550) ; 田浦 健次朗 東京大学, 大学院・情報理工学系研究科, 講師 (90282714)
• Keywords: プログラミング言語 / セキュリティ / 型システム / C言語 / Java / Linux / ラムダ計算 / パイ計算

Research Abstract

プログラミング言語の安全性にかかわる諸問題について、理論と実用の両面から研究をおこなった。以下に、本年度の代表的な個別成果を要約する。
1.暗号λ計算:暗号を利用するプログラムの安全性を数理論理学的に議論するために、プログラミング言語の代表的なモデルであるλ計算を暗号操作で拡張した暗号λ計算の体系を定義した。さらに、λ計算の一種である多相λ計算におけるパラメタ性の理論を、自明でない方法で暗号λ計算に導入し、暗号を利用したプログラムについて、(暗号系が完全ならば)実際に秘密情報が漏洩しないことを厳密に証明するための理論を確立した。
2.Fail-SafeなC言語処理系:たとえプログラムに欠陥があっても「コンピュータを乗っ取られる」「データが壊される」といった致命的影響がない(=Fail-Safeな)C言語の実装方式を提案・実験した。
3.Javaにおけるオブジェクト使用解析:代表的なオブジェクト指向プログラミング言語であるJavaを対象に、オブジェクトに対して可能な操作の集合のみならず順序をも解析・検査する体系を定義した。
4.Linux/TAL:オープンソースのOSであるLinuxにおいて、型により安全性が保証されたアセンブリのユーザプログラムを、カーネルモードで実行する方式を実装した。
5.分散計算におけるアクセス制御のための型システム:分散計算のモデルであるπ計算において、通信チャネルの形で表された計算リソースに対するアクセス制御のための型システムを定義した。

Research Products

• [Publications] Eijiro Sumii, Benjamin C.Pierce: "Logical Relations for Encryption"14th IEEE Computer Security Foundations Workshop. 256-269 (2001)
• [Publications] 大岩 寛, 住井 英二郎, 米澤 明憲: "安全性を保証するANSI-C実行系の実装手法"コンピュータソフトウェア. (掲載予定). (2002)
• [Publications] Daisuke Hoshina, Eijiro Sumii, Akinori Yonezawa: "A Typed Process Calculus for Fine-Grained Resource Access Control in Distributed Computation"Fourth International Symposium on Theoretical Aspects of Computer Software (TACS 2001), Lecture Notes in Computer Science. Vol. 2215. 64-81 (2001)
• [Publications] 前田 俊行, 住井 英二郎, 米澤 明憲: "Linux/TAL:型付きアセンブリプログラムのカーネルモード実行方式"第4回プログラミングおよびプログラミング言語ワークショップ(PPL2002). (掲載予定). (2002)
• [Publications] 浜中 信行, 住井 英二郎, 小林 直樹, 米澤 明憲: "Javaバイトコードにおけるオブジェクト使用解析のための型システム"第4回プログラミングおよびプログラミング言語ワークショップ(PPL2002). (掲載予定). (2002)
• [Publications] 関口 龍郎, 大岩 寛, 米澤 明憲: "オブジェクト指向言語によって記述された、携帯電話・PDAのアプリケーションプログラム圧縮方式"コンピュータソフトウェア. 第19巻・第1号. 1-9