|
平成26年度の交付申請書に記載した「研究の目的」および「研究実施計画」は次のとおりであった。
研究の目的（抜粋）：研究代表者らの「環境双模倣」の理論を発展させ、公開通信路上でソフトウェアを送受信・実行する高階オープンシステムを数理的に検証するための基盤を確立する。
研究実施計画：環境双模倣の機械的検証に向けて、定理証明支援器Coq上で環境双模倣の定義を形式化し、いくつかの例を形式的に証明する。具体的にはSatoとSumiiの高階値呼び応用π計算[APLAS2009]とその環境双模倣をCoq上で定義し、当該論文の二つの主な例（ソフトウェアアップデートシステムおよびWebメールシステム）の環境双模倣による安全性証明を形式化する。環境双模倣は様々な（高階の）言語に対して定義することが可能だが、高階値呼び応用π計算およびそれに対する環境双模倣は最も定義が複雑なものの一つであり、人手による証明は誤りが起きやすいと考えられる。Coq上で定義および自明でない例の証明を形式化し、それらに必要なライブラリを整備することにより、誤りの可能性が極めて小さい検証ツールを提供するとともに、その有効性を確認する。
計画にしたがい、高階値呼び応用π計算とその環境双模倣を、研究協力者とともにCoq上で形式化した。定義にあたっては、いくつか独自の部分があった。1. 当理論では、変数には（変数について）閉じた値のみが代入される一方、通信路(channel)や暗号鍵を表す名前(name)は自由に出現しうるため、de Bruijn index等の変数表現ではなく通常の変数名（を表す自然数）を用いた。2. Coq標準の多相list型は要素の型について共変であることが表せないため、帰納的定義に問題が生じ、独自の単相list型が必要となった。3. 文脈の穴の数に対応し、長さの情報を含むlist型が必要になった。
|
