プログラム検証による情報保護の統一理論とその応用

• 研究課題/領域番号: 18680003
• 研究種目: 若手研究(A)
• 配分区分: 補助金
• 研究分野: ソフトウエア
• 研究機関: 東北大学
• 研究代表者: 住井 英二郎 東北大学, 大学院情報科学研究科, 准教授 (00333550)
• 研究期間 (年度): 2006 – 2008
• 研究課題ステータス: 完了 (2008年度)
• 配分額: 15,860千円 (直接経費: 12,200千円、間接経費: 3,660千円); 2008年度: 4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円); 2007年度: 5,070千円 (直接経費: 3,900千円、間接経費: 1,170千円); 2006年度: 6,240千円 (直接経費: 4,800千円、間接経費: 1,440千円)
• キーワード: プログラム言語 / 情報セキュリティ / プログラム等価性 / 双模倣 / ラムダ計算 / パイ計算 / 高階計算 / 型理論 / プログラミング言語 / 計算モデル / λ計算 / π計算 / 操作的意味論 / 文脈等価性 / 論理関係 / 環境双模倣 / 多相λ計算 / 高階π計算 / 存在型・再帰型システム / ポインタ演算 / C言語 / Fail-Safe C to Java / Objective Caml

研究概要

コンピュータプログラムやネットワークにおける暗号化や抽象化など、さまざまな形の情報保護の統一的基礎理論を研究した。特に、ループないし再帰関数、再帰型(リストや木など)、多相型ないしジェネリックス、抽象データ型ないしオブジェクトなど、幅広い現実的機能を有する計算体系における情報保護の数理論理学的証明手法を世界で初めて確立し、Journal of the ACMやIEEE LICSなど最高水準の国際論文誌・国際学会に採録・発表された。

研究成果

• [雑誌論文] A Theory of Non-Monotone Memory (Or: Contexts for free) (2009)
  • 著者名/発表者名: Eijiro Sumii
  • 雑誌名: Proceedings of 18th European Symposium on Programming, (Lecture Notes in Computer Science, Springer-Verlag, Germany) vol. 550 ページ: 237-251
  • 査読あり
• [雑誌論文] A Theory of Non-Monotone Memory(Or : Contexts for free) (2009)
  • 著者名/発表者名: Eijiro Sumii
  • 雑誌名: Lecture Notes in Computer Science (Proceedings of 18th European Symposium on Programming) 5502 ページ: 237-251
  • 査読あり
• [雑誌論文] MinCamlコンパイラ (2008)
  • 著者名/発表者名: 住井 英二郎
  • 雑誌名: コンピュータソフトウェア, (岩波書店) 25巻2号 ページ: 28-38
  • NAID: 130004549107
  • 査読あり
• [雑誌論文] MinCamlコンパイラ (2008)
  • 著者名/発表者名: 住井英二郎
  • 雑誌名: コンピュータソフトウェア 25 ページ: 28-38
  • NAID: 130004549107
  • 査読あり
• [雑誌論文] Java言語への変換によるポインタ演算の安全な実装方式 (2008)
  • 著者名/発表者名: 上嶋 祐紀, 住井 英二郎
  • 雑誌名: コンピュータソフトウェア (採録決定)
  • NAID: 130004549129
  • 査読あり
• [雑誌論文] spi計算における暗号プロトコルの形式的検証 (2007)
  • 著者名/発表者名: 住井 英二郎
  • 雑誌名: 応用数理, (岩波書店) 17巻4号 ページ: 16-26
  • 査読あり
• [雑誌論文] A Bisimulation for Type Abstraction and Recursion (2007)
  • 著者名/発表者名: Eijiro Sumii and Benjamin C. Pierce
  • 雑誌名: Journal of the ACM, (issue 5, article 26) vol. 54 ページ: 1-43
  • 査読あり
• [雑誌論文] Environmental Bisimulations for Higher-Order Languages (2007)
  • 著者名/発表者名: Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii
  • 雑誌名: Proceedings of Twenty-Second Annual IEEE Symposium on Logic in Computer Science ページ: 293-302
  • 査読あり
• [雑誌論文] A Bisimulation for Dynamic Sealing. Theoretical Computer Science (2007)
  • 著者名/発表者名: Eijiro Sumii and Benjamin C. Pierce
  • 雑誌名: Elsevier Science, (issues 1-3) vol. 375 ページ: 169-192
  • 査読あり
• [雑誌論文] Logical Bisimulations and Functional Languages (2007)
  • 著者名/発表者名: Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii
  • 雑誌名: Post-Proceedings of IPM International Symposium on Fundamentals of Software Engineering, (Lecture Notes in Computer Science, Springer-Verlag, Germany) vol. 4767 ページ: 364-379
• [雑誌論文] A Bisimulation for Type Abstraction and Recursion (2007)
  • 著者名/発表者名: Eijiro Sumii and Benjamin C. Pierce
  • 雑誌名: Journal of the ACM 54-5-26 ページ: 1-43
  • 査読あり
• [雑誌論文] A Bisimulation for Dynamic Sealing (2007)
  • 著者名/発表者名: Eijiro Sumii, Benjamin C. Pierce
  • 雑誌名: Theoretical Computer Science 375・1-3 ページ: 169-192
• [雑誌論文] 型安全な通信ライブラリQuicksilverとその改良 (2007)
  • 著者名/発表者名: 須藤尚稔, 住井英二郎
  • 雑誌名: 第9回プログラミングおよびプログラミング言語ワークショップ論文集 ページ: 39-51
• [雑誌論文] Javaへの変換による安全なC言語の実装 (2007)
  • 著者名/発表者名: 上嶋祐紀, 住井英二郎
  • 雑誌名: 第9回プログラミングおよびプログラミング言語ワークショップ論文集 ページ: 52-66
• [学会発表] A Theory of Non-Monotone Memory (Or : Contexts for free) (2009)
  • 著者名/発表者名: Eijiro Sumii
  • 学会等名: 18th European Symposium on Programming
  • 発表場所: ヨーク(イギリス)
  • 年月日: 2009-03-26
• [学会発表] 型安全な通信ライブラリQuicksilverとその改良 (2007)
  • 著者名/発表者名: 藤 尚稔, 住井 英二郎
  • 学会等名: 日本ソフトウェア科学会 プログラミング論研究会 第9回プログラミングおよびプログラミング言語ワークショップ
  • 発表場所: 石川県加賀市
  • 年月日: 2007-03-08
• [学会発表] spi計算における暗号プロトコルの形式的検証について (2006)
  • 著者名/発表者名: 住井 英二郎
  • 学会等名: 日本応用数理学会 数理的技法による情報セキュリティ研究部会 第二回研究集会
  • 発表場所: 東京大学駒場キャンパス
  • 年月日: 2006-12-22
• [学会発表] 2時間で真似(まね)ぶ関数型言語のコンパイラ (2006)
  • 著者名/発表者名: 住井 英二郎
  • 学会等名: 日本ソフトウェア科学会 プログラミング論研究会 第44回プログラミングおよびプログラミング言語サマースクール
  • 発表場所: 東京大学本郷キャンパス
  • 年月日: 2006-09-12
• [備考]
  • URL: http://www.kb.ecei.tohoku.ac.jp/~sumii/
• [備考]
  • URL: http://www.kb.ecei.tohoku.ac.jp/~sumii/pub/