A unified theory and application of information hiding by program verification

程序验证信息隐藏的统一理论与应用

• 批准号: 18680003
• 负责人: SUMII Eijiro
• 金额: $ 10.15万
• 依托单位: Tohoku University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (A)
• 财政年份: 2006
• 资助国家: 日本
• 起止时间: 2006 至 2008
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-18680003/
• 关键词: プログラム言語; 情報セキュリティ; プログラム等価性; 双模倣; ラムダ計算; パイ計算; 高階計算; 型理論; プログラミング言語; 計算モデル; λ計算; π計算; 操作的意味論; 文脈等価性; 論理関係; 環境双模倣; 多相λ計算; 高階π計算; 存在型・再帰型システム; ポインタ演算; C言語; Fail-Safe C to Java; Objective Caml

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

The basic theory of unified information protection is studied in this paper. The proof method of information protection mathematical theory in computing system has been established for the first time in the world. The Journal of the ACM and LICS is the highest level of international papers collected and published by International Society.

项目成果

Javaへの変換による安全なC言語の実装

通过转换为 Java 实现安全的 C 语言实现

• 发表时间: 2007
• 期刊: 第9回プログラミングおよびプログラミング言語ワークショップ論文集
• 作者: 上嶋祐紀;住井英二郎
• 通讯作者: 住井英二郎

A Theory of Non-Monotone Memory (Or: Contexts for free)

非单调记忆理论（或者：免费上下文）

• 发表时间: 2009
• 期刊: Proceedings of 18th European Symposium on Programming, (Lecture Notes in Computer Science, Springer-Verlag, Germany) vol. 550
• 作者: Atsushi Mitsuda;Tetsu Iwata;Tetsu Iwata;Eijiro Sumii
• 通讯作者: Eijiro Sumii

spi計算における暗号プロトコルの形式的検証

spi计算中密码协议的形式化验证

• 发表时间: 2007
• 期刊: 応用数理, (岩波書店) 17巻4号
• 作者: 上嶋 祐紀;住井 英二郎;住井 英二郎
• 通讯作者: 住井 英二郎

spi計算における暗号プロトコルの形式的検証について

spi计算中密码协议的形式化验证

• 发表时间: 2006
• 作者: 藤 尚稔;住井 英二郎;住井 英二郎
• 通讯作者: 住井 英二郎

A Bisimulation for Dynamic Sealing. Theoretical Computer Science

动态密封的互模拟。

• 发表时间: 2007
• 期刊: Elsevier Science, (issues 1-3) vol. 375
• 作者: Davide Sangiorgi;Naoki Kobayashi;and Eijiro Sumii;Eijiro Sumii and Benjamin C. Pierce
• 通讯作者: Eijiro Sumii and Benjamin C. Pierce