野口研究奨励賞受賞

住井 英二郎（すみい えいじろう） 東北大学大学院情報科学研究科 情報基礎科学専攻

研究の概要:

様々な社会基盤がコンピュータに依存する現代社会において、実際にコンピュー
タを制御する「ソフトウェア」の信頼性向上は最重要課題の一つである。この
一年だけでも毎月のように、一般紙の第一面で報道されるほどの重大な問題が
続発している。特に（偶然の事故だけでなく）意図された攻撃に対する「セキュ
リティ」は、一見すると些細な欠陥が問題となるケースがほとんどで、プログ
ラマやユーザの注意やテストだけでは保証できていない。


そこで、数学的帰納法を一般化した「構造的帰納法」や、その双対である「余
帰納法」などの数理論理学的アプローチにより、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.