住井 英二郎 助教授が
情報処理学会東北支部の野口研究奨励賞を受賞
|
|
|
■受賞の感想
一般にいわゆる「プログラム理論」の研究は、ともすると「易しいことを難しく言っているだけで役に立たない」等と言われた頃もあったと聞きますが、情報処理システムの不具合や脆弱性が社会問題化するに至り、ここに来て急速に注目されつつあるように感じています。そのような中で、「実学」の伝統があるという東北地域において、今回のような賞をいただけたことは、非常に光栄であると共に身の引き締まる思いです。これも今まで御指導いただいた先生方のおかげかと思います。今後も皆様の貴重なご指導をたまわりながら、「良い基礎研究こそ真の実用価値につながる」という信念を持って、より一層の勉学に励みたいと思います。 |
|
 |
| 住井 英二郎 先生 |
■研究の概要
様々な社会基盤がコンピュータに依存する現代社会において、実際にコンピュータを制御する「ソフトウェア」の信頼性向上は最重要課題の一つである。この一年だけでも毎月のように、一般紙の第一面で報道されるほどの重大な問題が続発している。特に（偶然の事故だけでなく）意図された攻撃に対する「セキュリティ」は、一見すると些細な欠陥が問題となるケースがほとんどで、プログラマやユーザの注意やテストだけでは保証できていない。
そこで、数学的帰納法を一般化した「構造的帰納法」や、その双対である「余帰納法」などの数理論理学的アプローチにより、C, Java, MLといったプログラミング言語の意味論を定式化し、（特定の意味で）プログラムが安全であることを証明する手法が注目されている。
本研究では、暗号やデータ抽象といった機構により情報を保護するプログラムの安全性を、余帰納法によって証明するための理論を定義した。これは、「あるシステムf(x)がxの値を漏洩しない」という性質を「x1≠x2であっても、外から観察すればf(x1)とf(x2)が等価に見える」と定義し、f(x1)とf(x2)に対して可能な観察の列が一致することを示す、というアプローチである。
今回の手法は、従来の手法と異なり、現実のプログラムで必要となるループや再帰、並行処理、高階関数なども扱うことができる。また、暗号とデータ抽象のように、一見するとまったく異なるように思われる情報保護の機構にも一様に適用でき、プログラミング言語における「情報隠蔽」の本質を捉えた方式と考えられる。実際、国内外の研究者により、本研究と直接的に関連した結果が次々と発表されている。
|
■論文等
[対象論文] Logical Relations for Encryption. Eijiro Sumii and Benjamin
C. Pierce.
Journal of Computer Security, IOS Press, vol. 11, no. 4, pp. 521-554, 2003.
[参考論文1] A Bisimulation for Dynamic Sealing. Eijiro Sumii and Benjamin
C. Pierce.
Proceedings of 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of
Programming
Languages, pp. 161-172, 2004. (Full version accepted in Theoretical Computer Science, Elsevier
Science.)
[参考論文2] A Bisimulation for Type Abstraction and Recursion. Eijiro Sumii
and Benjamin C. Pierce.
Proceedings of 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of
Programming
Languages, pp. 63-74, 2005. |
|
