2002 Fiscal Year Annual Research Report

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

Research Project

Project/Area Number	12133203
Research Institution	The University of Tokyo
Principal Investigator	米澤明憲東京大学, 大学院・情報学環, 教授 (00133116)
Co-Investigator(Kenkyū-buntansha)	住井英二郎東京大学, 大学院・情報学環, 助手 (00333550) 増原英彦東京大学, 大学院・総合文化研究科, 助教授 (40280937) 田浦健次朗東京大学, 大学院・情報理工学系研究科, 助教授 (90282714)
Keywords	プログラミング言語 / セキュリティ / Fail-Safe C言語 / Kernel Mode Linux / 正規表現型 / インターフェース定義言語(IDL) / 型システム / 型推論
Research Abstract	昨年度に引き続き、コンピュータソフトウェアの欠陥を防止するための安全なプログラミング言語システムについて研究を行った。本年度の主要な成果を以下に挙げる。 1.安全なC言語処理系:基本的な方式の提案とプロトタイプによる実験の結果を、論文誌ならびに国際会議で発表するとともに、本格的な実装に取り組んだ。また、外部のソフトウェアとの相互運用性を向上するために、インターフェース記述言語(IDL)を設計・開発した。 2.ユーザプログラムをカーネルモードで実行可能なLinux:型検査等の実行前検証により安全性が事前に保証されているユーザプログラムをカーネルモードで実行できるLinux(オープンソースのUNIXの一種)を開発・公開した。基礎的な実験によれば、システムコール自体にかかるオーバーヘッドは、約1ミリ秒から30ナノ秒程度に減少した。また、より様々なプログラムで大規模な実験を行うために、標準ライブラリ(libc)を移植する作業を行った。 3.文字列処理のための正規表現型:正規表現を文字列の型とみなして型検査や型推論を行うことにより、文字列処理の検証・解析を実現する型システムについて、基礎となる型付け規則と型推論の方式を提案し、それらの正当性を証明した。 4.安全なプログラミング言語の応用:MLやSchemeといった安全なプログラミング言語や、それらの言語における研究の成果を、JavaやC++といった従来の言語に適用したり、メールシステム、暗号プロトコル、移動コードによるパケットフィルタリング、ゲノム解析、対戦プログラムといった様々な領域の問題に応用し、そのような言語ないし研究が(従来の技術と比較しても)有用であることを実証した。

Research Products

(6 results)

All Other

All Publications (6 results)

[Publications] 大岩寛, 住井英二郎, 米澤明憲: "安全性を保証するANSI-C実行系の実装手法"コンピュータソフトウェア. 19巻3号. 39-44 (2002)
[Publications] Naoshi Tabuchi, Eijiro Sumii, Akinori Yonezawa: "Regular Expression Types for Strings in a Text Processing Language"Electronic Notes in Theoretical Computer Science, (Proceedings of Workshop on Types in Programming). (to appear).
[Publications] Reynald Affeldt, Naoki Kobayashi: "Formalization and Verification of a Mail Server in Coq"Lecture Notes in Computer Science, (Hot Topics : Software Security -Theories and Systems). 2609(to appear). (2003)
[Publications] Yutaka Oiwa, Tatsuro Sekiguchi, Eijiro Sumii, Akinori Yonezawa: "Fail-Safe ANSI-C Compiler : An Approach to Making C Programs Secure (Progress Report)"Lecture Notes in Computer Science, (Hot Topics : Software Security -Theories and Systems). 2609(to appear). (2003)
[Publications] 田渕直, 住井英二郎, 米澤明憲: "テキスト処理言語における文字列のための正規表現型"情報処理学会論文誌:プログラミング. (採録決定).
[Publications] Eijiro Sumii, Benjamin C.Pierce: "Logical Relations for Encryption"Journal of Computer Security. (to appear).

2002 Fiscal Year Annual Research Report

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

Principal Investigator

米澤 明憲 東京大学, 大学院・情報学環, 教授 (00133116)

Research Products

[Publications] 大岩寛, 住井英二郎, 米澤明憲: "安全性を保証するANSI-C実行系の実装手法"コンピュータソフトウェア. 19巻3号. 39-44 (2002)

[Publications] Naoshi Tabuchi, Eijiro Sumii, Akinori Yonezawa: "Regular Expression Types for Strings in a Text Processing Language"Electronic Notes in Theoretical Computer Science, (Proceedings of Workshop on Types in Programming). (to appear).

[Publications] Reynald Affeldt, Naoki Kobayashi: "Formalization and Verification of a Mail Server in Coq"Lecture Notes in Computer Science, (Hot Topics : Software Security -Theories and Systems). 2609(to appear). (2003)

[Publications] Yutaka Oiwa, Tatsuro Sekiguchi, Eijiro Sumii, Akinori Yonezawa: "Fail-Safe ANSI-C Compiler : An Approach to Making C Programs Secure (Progress Report)"Lecture Notes in Computer Science, (Hot Topics : Software Security -Theories and Systems). 2609(to appear). (2003)

[Publications] 田渕 直, 住井 英二郎, 米澤 明憲: "テキスト処理言語における文字列のための正規表現型"情報処理学会論文誌:プログラミング. (採録決定).

[Publications] Eijiro Sumii, Benjamin C.Pierce: "Logical Relations for Encryption"Journal of Computer Security. (to appear).

米澤明憲東京大学, 大学院・情報学環, 教授 (00133116)

[Publications] 田渕直, 住井英二郎, 米澤明憲: "テキスト処理言語における文字列のための正規表現型"情報処理学会論文誌:プログラミング. (採録決定).