プログラム論証システムの信頼性と安全性に関する研究

点击翻译按钮获取中文摘要

今回の研究の対象とするモデルに関する2つの課題1.プログラムをデモする販売者とそれを購入しようとするユーザーという2者間のモデルを,通信機能を有するチューリング機械を用いて,厳密に定義する.2.さらに,この定義されたモデル上で,一切の情報をもらさない通信手段の条件を,ゼロ知識証明に基づき与える.は,満足のいく形で定式化できた.本研究の枠組では,与えられた問題に解がある場合も,解が存在しない場合も同時に扱う必要があり,従来の定理証明型対話証明の定義をそのままもちいることができない.このため,従来知識の健全性として定義されて概念をプログラム検証システムを用いて,プログラム論証モデルに拡張することにより,“証明者が本当に正しく動作するプログラムを所持する"という状態を厳密に定義できた.通信方式の安全性(ゼロ知識証明性)に関しては,従来の定理証明型対話証明の定義を自然に適用することで,問題なく定式化できた.さらに,研究計画の1つ"どのような問題に対する解決プログラムが我々が考えるモデル上で安全に論証できるか具体例を与える"に関して,特に解の存在,非存在に関する従来から知られた定理のゼロ知識証明をもつ問題に対して,それらの問題解法プログラムが,我々が考えるモデル上で安全に論証できるかいなかという問題は,グラフの同型判定問題に関する新しいプロトコルを設計しることで,肯定的に解決できた.このプロトコルは,計算機上のネット-ワーク通信を利用して,実験を行ない,正しく動作することも確認できた.また,ユーザーに論証可能なプログラムはすべて,有用な情報を漏らさない形で論証できるかどうか,その限界を,明らかにすることも重要な目標であったが,これに関して得られた結果は,否定的で,ある計算複雑性に関する仮定(予想)のもとでは,この通信方式を,一切の情報を漏らさない形には変形できないこと,もっと強く,その関数の値を計算するいかなるプログラム論証方式も,一切の情報を漏らさない形には変形できないことが数学的に証明できた.