社会基盤としてのセキュアコンピューティングの実現方式の研究
研究領域代表者 米澤明憲（東京大学大学院・情報学環・教授）
研究代表者からの申請総額6億5000万円
研究期間 平成12年−平成16年
インターネットの爆発的な普及により、コンピュータとそのネットワークの利用は目に見える形だけでなく、人間社会のほとんどあらゆる部分で利用されるようになってきた。 このためコンピュータネットワークは、人間の社会生活や産業を支える、水道、ガス、電気、交通施設などと同じような、一つの社会基盤となっている。
この新しい情報社会基盤は、その便利さが強調される一方、その安全性（セキュリティ）は確かに保証されていないという実状は、あまり知られてなかったようである。実際、本年1月には、省庁が持つ公共情報を公開している多くのホームページが何者かによって悪意をもって書き換えら（改ざんさ）れたり、5月には、電子メールによって大量のコンピュータウイルスが世界中のコンピュータに送り込まれ、ネットワークにつながっているコンピュータが使用不能になり、地球規模での大混乱が起きたことは、記憶に新しい。
この情報社会基盤を実現しているコンピュータやネットワークにおいて、特にその安全性に心配があるのは、コンピュータを動かしネットワークを制御している様々な応用プログラムやシステム・ソフトウエアです。我々の研究は、このようなプログラムやソフトウエアを安全なものとして実現すし、かつ安全なものであることを保証するための科学技術を開発・深化させるものです。
我々が研究・開発しようとしている、安全な社会基盤ソフトウエアシステムの実現方式は、3重構造によってその安全性を保証する。それは、（１）そのプログラム群すなわちソフトウエアシステムを作るための、安全なプログラム言語の設計・開発、（２）外敵の侵入を食い止め、ソフトウエア・システムの安全かつ効率よい実行を保証するオペレーティングシステムなどの設計・開発、（３）安全性の要求や基準を数理論理の言葉で記述し、かつソフトウエアシステムが実際にその基準や要求を満たしていることを理論的に証明する方式の設計・開発、の3つのアプローチを併用するという特徴がある。