１．申請領域の研究の必要性と緊急性
２１世紀の人類が豊かな発展を遂げるには、近年その重要性が飛躍的に高まりつつある情報科学技術に基づく社会基盤の高度化が不可欠であることは論を待たない。たとえば、エネルギーの生産・分配管理の先進化、医療技術やサービスの発展と広範な浸透、教育の高度化・多様化、各種交通・通信システムの効率化、電子商取引などの新しい経済活動形態の発展、知的生産物の流通の飛躍的促進、さらには広範な産業や高度な科学技術の発展など、人類のおよそ全ての営為の発展・深化がこの情報社会基盤によって支えられると言っても過言ではない。そしてこの情報社会基盤は、大規模かつ広域に分散しつつ多岐にわたるコンピュータ群のネットワークとして、膨大なコンピュータソフトウェアによって実現されている。（図１参照）
図１ 社会基盤としてのコンピューティングインフラ
一方この情報社会基盤は、極めて急速かつ高度に発展し複雑化しつつある情報科学技術に立脚するもので、その安全性や信頼性を保証するテクノロジー（理論と実践技術）の追従が遅れ勝ちである。にもかかわらず、そのテクノロジーさえも駆使せずに現実の社会基盤が構築されつつある。また、急速に発展する技術とそれがもたらす利便性に触発された個人の様々な欲求故に、拙速な技術的裏付けのみで製品化され社会に流布したものさえある。また、人類の平和な繁栄にとってクリティカルな産業・福祉（・防衛）システムには、多数のコンピュータ制御の電子装置が組み込まれている。そして、その制御ソフトウェアの安全性が技術的に未保証に近い状態のまま使用されているのが現状であり、さらにこの現状に対する社会的認識も十全であるとは言いがたい。このような状況を放置しておくことは、将来にわたって多大な危険性を内包する社会基盤を構築してしまう結果とになる。従って、本領域研究の対象とする問題は火急かつ速やかに解決すべきものである
ここに申請する領域の研究は、上で手短に述べた二つの背景、すなわち（１）情報社会基盤の高度な発展が不可欠である点、および（２）その基盤の安全性が、技術的に必ずしも保証されたものではないという事実を踏まえ、直面する重大な社会的課題の技術的解決を目的としており、その研究成果に対する社会的要請が極めて高いものである。同時に、この領域が視野に入れるソフトウェアシステム機能の急激な高度化に即応した形で、ソフトウェアの安全性を保証する技術研究が進展しきれていないという事実を鑑みれば、その研究の整合性ある発展の観点から、その進展には特別の配慮を必要とすると考えられる。また、そのような研究の成果は国家利益に直接結びつく例が多く、欧米を中心とする諸外国では、その成果が国外へ遺漏することを避ける傾向にある。そこで、わが国自身の研究資金によって研究者の精鋭を結集して、独自の研究成果を保有することは様々な意味からも枢要と考えられる。
さて、この研究領域の重要性に対する理解をもう少し深めさせて頂くために、少し直感的な例を用いて、この研究領域が対象とする社会基盤コンピューティングシステムの安全性を脅かす脅威について説明しよう。一般にコンピューティングシステムに対する脅威の例を、非常に大づかみに述べると、
図２ 危険な現状
（１）計算・通信用のハードウエアの故障、
＊（２）計算機で（並列でなく）逐次実行するように書かれたプログラムにある誤り（バク）に起因する誤動作、
＊（３）二つ以上のプログラムが同時に実行されたり、互いに通信しながら実行する時に生じる誤動作、
＊（４）あるコンピュータ上で実行されることを想定して書かれたプログラムが、別のコンピュータに移動（移住）して実行されるときに、新しい環境に適応できないことに起因する誤動作、
＊（５）他人のプログラム中に浸入し、故意に他人のプログラムを動かなくしたり、浸入したプログラムの実行環境を破壊したりする、いわゆる「コンピュータウイルス」や危険かつ不正なコードに起因する異常動作、
＊（６）悪意をもったユーザ（クラッカーとかハッカーとか呼ばれる個人）がネットワーク内のコンピュータに浸入し、そのコンピュータの正当なユーザに成りすまし、他人の情報を盗んだり、システムの正常な運用に必要な情報を改変する脅威、
（７）ネットワークで結ばれたコンピュータの間で転送される（暗号化された）情報が傍受されて解読されたり改竄される脅威、
などがあげられる。この中で、われわれの研究で対処しようとする脅威は、＊印をつけた（２）から（６）を対応する。（図２参照）一方（１）への対処法は、各方面で別途研究開発が活発に行われている。（７）への対処法は、基本的に（公開鍵、非公開鍵方式等の研究を含む）暗号･復号化方式の数学的研究の成果によってもたらされるもので、大変重要なテーマであり、やはり関係方面で大きな研究テーマとして取り上げられているものである。
我々が研究（および開発）しようとする（２）から（６）の問題は、それに対する良い纏まりをもった研究体制が組み易い。さらに暗号・復号方式の研究成果によって（７）への対処法が将来確立された場合でも、依然として研究しなければならない重要な課題であることを強調しておく。
（付記： 本申請書の「６．その他」の部分に用語の解説集をつくり付加しておいた。適宜参考にされ、この申請書を読む上での一助とされたい。）
２． 申請領域の国内・外の研究状況
国内では、本申請に類似する重点・特定研究は過去に実施されたことはない。通産省の外郭団体である情報処理振興事業協会（IPA)による創造的ソフトウェア育成事業として、横浜国大の松本勉氏と日本IBMの田村哲也氏が実施した「対タンパ（改竄）モジュールの構築と利用のための高度暗号技術の開発」は国内では、我々の領域研究に唯一最も関連が深い。ここでの成果の１つであるPCカードと耐改竄モジュールの構成法や機能証明技術などは、我々の研究を進める上で利用できる技術といえる。しかし、提案された機能証明技術では、仕様どおりに機能が実現されているかを検証するメカニズムを提供しておらず、下で述べる本申請領域の研究項目A０１の成果無しに、利用することは安全でない。
欧米諸国ではコンピュータセキュリティに関する研究プロジェクトは相当数にのぼる。（たとえば、米国においては、ネットワーク上の単一計算機内におけるセキュアコンピューティングやトラステッドコード(trusted code)に関する研究の歴史が長い。また、ヨーロッパでもたとえばEuropean Symposium on Research in Computer Security会議の開催は既に6回に及んでいる。）しかしながら、我々が申請している領域研究に類似するものは見当たらない。
一方、米国国防省の研究プログラム局DARPAが1997年3月に開催したDARPA Foundations for Secure Mobile Code Workshopでのテーマが、本申請領域のテーマと非常に近いものである。このワークショップで、議論された内容は、後で概要を示する研究項目A01,A02,A03と関係しているが、問題解決の方法に関する発表というより、問題提議タイプのものが多く、これらのテーマが重要な課題であるという共通認識に立ったにすぎないといえる。
米国の計算機科学における最先端大学であるカーネギーメロン大学においては、Tyger教授のグループがシステムレベルの研究として、専用付属プロセッサを持ったシステムのために、オペレーティングシステムDyadを開発している。このシステムでは、cryptopagingの手法などが試作されているが、特殊なハードウェア支援を前提としている点が我々の研究のアプローチとはまったく異なる。またMITでは、Goldwasser教授のグループが、米国国防省の研究プログラムの一環として分散セキュアシステムに関する研究をしている。しかし、研究の中心は、公開鍵方式による暗号システムやディジタル署名に関するテーマにあり、本申請領域では対象としないものである。
３．申請までの準備研究・調査の状況
本領域研究の申請に先立って、科学研究補助金基盤研究による調査研究は特に実施しなかった。しかしながら、本申請の代表者である米澤が昨年度から運営委員長を務める、（国内の主要情報通信産業１０社が支援する）産学による「戦略的ソフトウェア研究フォーラム（SSR)」（事務局： 公益増進財団法人「情報科学国際交流財団」）において、H１０年度には「グローバルコンピューティング」研究会、H１１年度には「エンタープライズセキュリティ」研究会の開催を、本申請の計画研究の代表者の多くを中心に重ねてきた。これにより社会基盤としてのグローバルネットワークとそのセキュリティを中心とした調査研究を実施し、本領域申請のための準備を進めてきたという経緯がある。さらに計画研究の代表者の多くは重点（特定A)領域「ソフトウェア発展」（代表者：片山卓也、北陸先端大）に参加し、その中で特別の研究連絡会を開催し、本申請の準備にあたってきた。
また、通産省傘下の情報処理振興事業協会（IPA)の助成を得て、計画研究の代表者の一人である溝口文雄（東京理科大）が調査研究を実施し、「耐改竄・ソフトウェア技術の移動エージェントへの応用」に関する調査報告書をH１１年２月にまとめている。さらに、個別の計画研究申請調書の中でそれぞれ述べられているように、本申請への参加研究者は本領域の十分な事前研究の実績がある。
一方、上で触れた「ソフトウェア発展」重点領域に参加する何人かの研究者は、６．２で示すように、本申請の特定領域に代表者あるいは分担者として参加している。しかし、研究の目的、対象、方法などにおいて力点や焦点の置き方が異なり、本申請特定領域と類似するものではない。また過去に実施された重点領域、特定領域に本申請に類似するものは皆無である。
４．特定領域を推進するにあたっての基本的な考え方
我々の事前調査や研究の結論として、我々が研究対象とする（２）から（６）に相当する脅威に対処し、社会基盤としての安全性が保証されたコンピューティングシステムを実現するためには、３つのアプローチが必要であることが明らかになった。（暗号・復号方式の研究は上述した理由で、我々の守備範囲としない。）これらのアプローチは、脅威の種類や抽象度、あるいは対処手法の性質などによって、比較的独立しかつ互いに補完しあうものである。また、この３つのアプローチで得られる研究成果を駆使し、その実用化への大きな可能性を示すために、比較的小規模ではあるが社会基盤の一つとみなせるシステムとして、（学生数約２００００人を想定した）大学キャンパス向けに、安全性を強く保証した情報基盤システムのプロトタイプを構築する。これによってこの研究領域の研究成果の明確な検証を行うとともに、具体的な目標を掲げることにより、研究の一層の推進をはかる。
４.１. 研究項目の立て方
上で触れた３つのアプローチをより具体的にのべると次のようになり、この３つのアプローチに対応して３つの研究項目を立てた。
（A01) 形式論理等の体系を用いることによって、基盤システムの安全性への要請を理論的に証明・検証する。
（A02) 安全性を保証し易く、かつ高い機能を実現するプログラム（ソフトウェア）を書くための言語・記述系を設計し、その効率のよい実行システムを実装する。
（A03) 言語・記述系の実現の土台となり、同時に言語・記述系では防ぎ得ない脅威に対処できるソフトウェアインフラストラクチャや軽量の公開鍵方式を実現する。
図３ 我々の安全へのアプローチ
４.２. 研究組織のあり方
３つの研究項目の中では、手法の違いや対象の違いに従い各々３つの計画研究を配し、国際的に評価の高いわが国の精鋭研究者を結集してそれぞれの計画研究を実行できるように心がけた（６．４を参照）。また、組織全体のサイズは、異なるアプローチの研究者間で全体的討論が可能でありかつ効率のよい緊密な連携が保てるよう、比較的小規模に抑えた。
さらに、３つのアプローチを統合して研究するための調整や、統合システムを実現する目的で総括班を設けた。総括班は当然のことながら、領域研究の推進とその評価も行うが、それとともに、研究成果発表と国際的交流・発信を目的とする国際ワークショップの隔年開催に大きな役割をはたす。総括班は計画研究を実施する比較的年長の研究者と、（１）情報社会基盤システム、（２）並列分散コンピューティングシステム、（３）形式的理論の枠組み、（４）ソフトウェア構成方式、などについて高い見識を持つ外部の研究者や、文部省外の研究機関の指導者（安西祐一郎、田中英彦、稲垣康善、伊藤貴康、片山卓也、諏訪基、の各先生方）により構成される。
４.３. 研究期間の設定について
細部は個別の計画研究により異なるが、おおむね全期間を３期に分け、I期（H12-H13年度）は基本概念や基本技術の提案・深化にあて、II期（H13-H14年度）ではシステムを設計・実現し、III期（H14-H15年度）にアプリケーションの構築による実証を行う。さらにこのスケジュールで、実質３年半の期間中に統合システムのプロトタイプの実現を期す。
４.４. 研究経費の考え方
各計画研究は研究上の特徴や手法の違いによって、総予算、各年度予算額は異なる。最終年度には設備費をあまり必要としないが、各計画でのプロトタイプソフトウェアシステムの実現のために謝金の要求が多い。
総括班においては班員による研究推進・評価のための旅費のほか、隔年（H13,H15)に国際ワークショップを開催するための費用を計上している。また最終年度には、統合システムの実現のために必要となる補助的経費を計上している。
５．特定領域の内容
５.１. 申請領域の研究の概要
すでに述べたように、以下の３つのアプローチ、（A01)形式論理等の体系を用いた基盤システムの安全性要請の理論的な証明・検証、（A02)安全性を保証しやすくかつ高い機能を実現するプログラム（ソフトウェア）を書くための言語・記述系の設計、およびその効率のよい実行システムの実装、（A03)言語・記述系の実現の土台となり、言語・記述系では防ぎ得ない脅威に対処できるソフトウェアインフラストラクチャや軽量の公開鍵方式の実現、を行うとともに、さらに３アプローチの有用性を統合的に検証するために、（学生数約２００００人を想定した）大学キャンパス向けに、安全性を強く保証した情報基盤システムのプロトタイプを構築する。
５.２. 研究項目の研究内容
各研究項目とその中の計画研究内容の概要を下に示す｡
研究項目A01 システムセキュリティのための形式的検証法の研究
概要：システムがセキュアであることの厳密な意味での確証を得るためには、システムセキュリティを形式的な枠組みの中で記述し検証する方法が究極的であると考えられている。この考え方は形式手法と呼ばれ、ここ十年あまりの間、特に並行分散システムに対して適用が考えられて来た。最近では、公的な検査機関を組織してこのような検証を行い、システムのセキュリティのレベルを確保しようという動きもある。本研究では、このような技術の適用領域を広げるとともに、規模の増大にも対処するための方式について、論理的枠組み、代数的枠組み、型システムの3つの観点から以下の研究を行う。
Safety criticalなシステム、特にリアクティブシステムや、商取引プロトコルに関して、あるいは、移動コードやネットワークやプロセッサをまたがりデータや資源を共有しながら同時に動作するプログラム群を対象として、論理的に記述された仕様に対する実現可能性の検証、システム実現の正しさの検証、特に安全性に関する検証、検証システムの正しさの検証、システムへの攻撃に対する耐性の検証方式を与える。
図４ 研究項目間の関係
研究項目A01-研究計画（２） 代表者 米崎直樹
「論理的仕様を基礎としたセキュアシステムの検証法」
概要：Safe criticalなシステム、特にリアクティブシステムや、商取引プロトコルに関して、論理的に記述された仕様に対する実現可能性の検証、システム実現の正しさの検証、検証システムの正しさの検証、システムへの攻撃に対する耐性の検証方式について、現実的規模のシステムの検証に必要な技術及びその理論的基礎を与える。特に検証の再利用性や、抽象モデルによる検証、検証のスケーラビリティについて明らかにする。
研究項目A01-研究計画（３） 代表者 小林直樹
「セキュアコンピューティングのための型システム」
概要：セキュアコンピューティングの実現のためには，各プログラムについてそれが単体として正しく動作するだけでなく，ネットワークやプロセッサをまたがりデータや資源を共有しながら同時に動作する他のプログラムに悪影響を及ぼさないことの保証が必要不可欠である。本研究では，プログラムの仕様を記述・検証するための枠組みの一種である型システムに基づき，それらの性質を保証するための枠組みを構築する。
研究項目A01-研究計画（４） 代表者 二木厚吉
「振舞仕様に基づく安全性検証の研究」
概要：セキュアコンピューティングを支える最重要の基盤技術として移動コードを取り上げ，汎用性と適応性に優れ，検証の自動化も容易な安全性検証技術を研究開発する．安全性検証のための，意味定義，保障すべき性質の定義，十分条件の生成と検証を，提案者が独自に開発した振舞仕様の理論/技術に基づく統一的な理論体系と解析法に基づいて行なうことで，所望の性能を実現する。
研究項目A02： セキュアシステムのためのソフト記述/実行機構システムの研究
概要：移動コードを利用したネットワークアプリケーションは、近年、遠隔メンテナンス・電子商取引などの応用が増加しつつある。これらをセキュアに実行するためには、ウィルスのような移動コードによってシステムが悪用されることを防ぐことと、移動コード自身の誤動作を防ぐことの両者が重要である。そのため、システム内の操作を正当なものと不当なものとに区別し、不当な操作を排除することや、システムの故障や環境の変化に柔軟に対応できるプログラム記述系が必要となる。これらの問題に対し、(1)プログラム解析技術およびプログラム実行時に不当な操作を禁止する枠組、(2)正当な操作を定義するための支援環境、(3)故障や環境の変化に対応するための機構、の3点について研究を行う。
研究項目A02-計画研究（５） 代表者 米澤明憲
「移動コードを基本としたセキュアなプログラミング言語処理系」
概要：ネットワーク上をプログラムコードが移動するような場合に、(1)ウィルスのようなコードからシステムを守ることができ、(2)計算機やネットワークの故障に際しても正しく動作させることを目標とする。そのために、プログラム言語の設計・コンパイラ・実行時系等の側面において、プログラムの解析手法を提案し、例外処理の理論的扱いの深化等を行い、言語処理系として実現する。
研究項目A02-計画研究（６） 代表者 渡部卓雄
「拡張/適応可能ソフトウェアのセキュアな構成方式」
概要：移動コードを用いて構成されるソフトウェアシステムに，(1)新しい機能を獲得する能力(拡張性)，および(2)ネットワーク・実行環境の変化や故障に対処する能力(適応性)を，安全な方式で導入することを目標とする．そのための，(a)自己観測・操作(自己反映動作)に基く拡張・適応機構の提案，(b)その理論的扱いの深化，および(c)言語機構(またはミドルウェア)としての実現を行う．
研究項目A02-計画研究 （７） 代表者 柴山悦哉
「セキュリティーポリシーの記述体系とその交渉モデルに関する研究」
概要：セキュアコンピューティングの前提として，正当な操作と不当な操作の区別が必要となる．しかし，そのための定義は複雑で困難なものとなりがちである．そこで，本研究では，正当な操作の定義を容易に行うためのビジュアル支援環境を設計・開発する．また，操作の正当性の定義は一般に組織毎に異なる．本研究では，さまざまな正当性の定義に適応できるソフトウェアの構築方法論の開発も行う．
研究項目A03: セキュアシステムのためのインフラストラクチャの研究
概要：計算機システムの屋台骨を支えるインフラストラクチャ・ソフトウェアは，計算機ハードウェアが誕生して以来の長い歴史をもつが，これまでは，提供されるサービスとユーザのすべてが，基本的にシステム管理者によって把握可能であるという，閉じた環境を前提とした設計がなされてきた．そこで本研究では，インフラストラクチャ・ソフトウェアを根本から見直し，意図的・非意図的を問わず，計算機資源を冒す可能性を孕んだソフトウェアをセキュアに取り扱う基盤ソフトウェア技術に関する研究開発を行う．具体的には，(1)オペレーティングシステム支援機構，(2) ソフトウェア実行系，(3)エンタープライズセキュリティのためのシステム基盤ソフトウェア，の3点について研究を行う．
オペレーティングシステムの支援機構については，ネットワーク上を移動するアプリケーションを安全に実行するために必要となるオペレーティングシステムの機構を研究する．また、ソフトウェア実行系については，ソフトウェアの実行という点に焦点を絞り，実行するサイトが自身のもつ計算機資源の安全性を守りながらソフトウェアを実行する機構を研究する．さらに、エンタープライズセキュリティについては，企業間にまたがって運用されるネットワークアプリケーションを安全に運用する枠組みに関する研究を行う．
研究項目A03-研究計画（８） 代表者 徳田英幸
「セキュアなモバイルアプリケーションのためのオペレーティングシステム支援機構」
概要：本研究では、セキュアなモバイルアプリケーションの実行環境を実現するためのオペレーティングシステム支援機構を開発し、実装評価を行う。モバイルアプリケーションに対しては、偽ホスト、偽ホストオペレーティングシステム、偽モバイルエージェントなどによるさまざまな「なりすまし攻撃」、データやプログラムに対する「改ざん攻撃」、サービス妨害（Denial of Service）などを受ける可能性がある。これらに対してセキュアな作業の保証、作業継続性の保証、動的適応機構について研究する。
研究項目A03-計画研究（９） 代表者 加藤和彦（筑波大学電子・情報工学系・助教授）
「セキュアなソフトウェア実行系」
概要：オペレーティングシステムに代表されるこれまでの基盤ソフトウェアシステムでは，計算機利用環境が閉じている(closed)ことを暗黙のうちに仮定してきた．しかし，現在広く普及しつつあるインターネット環境はオープンであり，そこで流通しているソフトウェアはさまざまな危険性をはらんだものである可能性がある．本研究では，危険性を含むソフトウェアであっても，それを実行する計算機システムが自分の身を自分で守りつつ，安全に実行するソフトウェア実行系を研究開発する．
研究項目A03-計画研究（１０）代表者 溝口文雄
「エンタープライズセキュリティのためのシステム基盤ソフトウェアの研究」
概要：イントラネットやエクストラネットのような企業内の様々な情報システムへのアクセスを、ネットワークを介して行う状況で、システムの安全な運用やリスク回避を可能にする枠組みとそのためのシステムの構築について研究する。具体的には、軽量公開鍵システムの実装方式や役割に基づくアクセス制御方式などを研究開発する。また、生産工場や家庭内も情報化が進み、そこで情報機器のリモート制御もインターネットで行うことが可能となる。こうした企業内・生産工場内・家庭内でのインターネット利用に関して、安全な運用を実施する枠組みをエンタープライズセキュリテイと呼び、そのためのシステム基盤ソフトウェアを研究・開発する。