耐タンパ証明携帯プログラム配信システム及びその方法
【課題】既存のゼロ知識証明携帯プログラム配信方式においては公開していた不変条件を秘匿し、不変条件及び証明本体に基づくリバースエンジニアリングを防止し、配信プログラムの耐タンパ性を向上させるプログラム配信方式を提供する。
【解決手段】本発明の耐タンパ証明携帯プログラム配信方式は、プログラムを配信する際、プログラムが安全に実行可能なことを対話的に通信して検証する配信であり、プログラムが正しいことを示すために、プログラムを実行する際に、プログラム中の複数ポイントで成立すべき不変条件からなる不変条件列を生成し、不変条件列に対するダミーの不変条件を複数含む不変条件列候補集合を生成し、プログラム，不変条件列及び不変条件列候補集合に基づき、プログラムの安全性を証明する命題論理式を生成し、開発者及び利用者間で、ゼロ知識証明プロトコルに従い、命題論理式の真偽を判定し、プログラムを実行する。
【解決手段】本発明の耐タンパ証明携帯プログラム配信方式は、プログラムを配信する際、プログラムが安全に実行可能なことを対話的に通信して検証する配信であり、プログラムが正しいことを示すために、プログラムを実行する際に、プログラム中の複数ポイントで成立すべき不変条件からなる不変条件列を生成し、不変条件列に対するダミーの不変条件を複数含む不変条件列候補集合を生成し、プログラム，不変条件列及び不変条件列候補集合に基づき、プログラムの安全性を証明する命題論理式を生成し、開発者及び利用者間で、ゼロ知識証明プロトコルに従い、命題論理式の真偽を判定し、プログラムを実行する。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ネットワークを介したプログラム配信において悪性プログラムによるホストヘの攻撃と、悪意のあるホストによるプログラムヘの攻撃との、双方を同時に防ぐセキュリティ技術としての耐タンパ証明携帯プログラム配信システム及びその方法に関する。
【背景技術】
【０００２】
今日、プログラム化された高機能コンテンツがＷＷＷブラウザや携帯端末に日常的にダウンロードされ実行されている。
また、パケットやノードなどのネットワーク構成要素をプログラマブルとすることで拡張性や耐故障性を増したアクティブネットワークの研究も進んでいる。
プログラムが流通する時代を迎え、悪性プログラムから計算機を守る新しい技術への需要が高まってきている。
【０００３】
ここで、上述したようなネットワークを介したプログラム配信においては、タイプの異なる次の２種類の攻撃を考慮する必要がある。
・タイプ１悪性プログラム
ウィルス・バッファ溢れのバグを悪用するプログラムなどによるホストコンピュータヘの攻撃。
・タイプ２悪意のあるホストコンピュータによるプログラムヘの攻撃
配布されたプログラムの解析・改ざん・リバースエンジニアリングなど。
【０００４】
上述したタイプ１の攻撃を防ぐための技術としては、プログラムに開発者の電子署名を付与し検証する方式，パタンマッチによるウィルス検知・駆除方式，仮想機械のバイトコード検証方式などが既に実用化されている。しかしながら、これらの方式はいずれも悪性プログラムの検出精度に限界があることが知られている。
この問題を解決する次世代技術として、証明携帯プログラム配信方式(Proof-Carrying Code)（例えば、特許文献１及び非特許文献１を参照）が提案されている。この証明携帯プログラム配信方式は、プログラム本体にそれが正しく安全に動作すること(例えば、与えられた入力条件のもとでプログラムを実行した場合、結果が出力条件を満たし、実行時には禁止されたメモリ領域へのアクセスがまったくないこと）の詳細な数学的証明を添付し両者を同時に流通させ、証明に誤りのあるプログラムを悪性として実行前に検出・駆除する方式である。このように、証明を精査することにより厳密なプログラム検証を行うため、精度の高い検出・駆除が可能である．
【０００５】
しかしながら、上述した証明携帯プログラム配信方式には、証明サイズが指数開数的に爆発するという問題がある。
この証明携帯プログラム配信方式の問題を解決するために、簡単な対話的通信により証明の部分的検証を繰り返す方式、すなわち、対話型証明携帯プログラム配信方式（例えば、特許文献２及び非特許文献２を参照）が提案されている。
【０００６】
一方、上記タイプ２の攻撃を防ぐための要素技術としては、難読化・暗号化・多様化・電子透かしなどが既に提案されている（例えば、非特許文献３参照）。
また、すでに述べたタイプ１の攻撃に対し有望な技術である証明携帯プログラム配信方式、または対話型証明携帯プログラム配信方式は、その証明に誤りのあるプログラムの検出処理の特性上、タイプ２の攻撃の防止に対しては弱い。すなわち、悪性プログラムからホストを守るために安全性の証拠として添付する証明自体が、逆に悪意のあるホストに盗用・悪用されかねないという問題があるからである。
【０００７】
一般に、安全性の証明は、プログラム本体から、必ずしも直ちに引き出せるとは限らず、プログラムの意味に開する様々な情報を含んでいる。
したがって、上記証明をそのまま流通させた場合、例えば証明を利用したリバースエンジニアリングなどを招くおそれを否定することができない。
証明携帯プログラム配信方式あるいは対話型証明携帯プログラム配信方式を拡張し、上記タイプ１の攻撃に対する優位性を保ちつつ、安全性証明の盗用及び悪用を防止する機能を追加した方式として、ゼロ知識証明携帯プログラム配信方式（例えば、非特許文献４参照）が提案されている。この非特許文献４に記載されているように、証明・検証プロトコルのゼロ知識化により、安全性証明の内容を秘匿しつつプログラムの安全性を利用者に納得させることができ、その結果、安全性証明の盗用・悪用を防ぐことが可能となる。
【特許文献１】ＵＳ Ｐａｔｅｎｔ ６,１２８,７７４
【特許文献２】特開２０００−７８１２６号公報
【非特許文献１】George C. Necula. Proof-carrying code. In Proceedings ofthe 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,pp.106-119,Paris,January 1997.ACM，ACM Press.
【非特許文献２】Yasuyuki Tsukada. Interactive and probabilistic proof of mobiele code safety. Automated Software Engineering. Vol.12,No2,pp.237-257,April 2005.
【非特許文献３】門田暁人，Clark Thomborson. ソフトウェアプロテクションの技術動向（前編）−ソフトウェア単体での耐タンパー化技術−．情報処理，Vol.46,No.4,pp.431-437,2005.
【非特許文献４】塚田恭章．対話型安全証明つきプログラム配信方式における証明の秘匿とその応用．情報処理学会論文誌，Vol.46,No.1,pp.236-246,2005.
【非特許文献５】門田暁人，高田義広，鳥居宏次. ループを含むプログラムを難読化する方法の提案．電子情報学会論文誌D-I,Vol.J80-D-I,No.7,pp.644-652,1997.
【非特許文献６】一杉裕志．ソフトウェア電子すかしの挿入法、攻撃法、評価法、実装法．夏のプログラミングシンポジウム報告集, pp.57-64.情報処理学会,July 1997.
【非特許文献７】門田暁人，松本健一，飯田元，井上克朗，鳥居宏次．Javaクラスファイルに対する電子透かし法．情報処理学会論文誌, Vol.41, No.11, pp.3001-3009, 2000.
【非特許文献８】Shafi Goldwasser, Silvio Micali, and Charies Rackoff．The Knowledge Complexity of Interactive Proof Systems, SIAM J. Computing, Vol. 18, No. 1, pp. 186-208 ，1989.
【非特許文献９】Adi Shamir. IP = PSPACE, Jpurnal of ACM, Vol.39, No.4, pp. 869-877，1992.
【非特許文献１０】Ronald Cramer and Ivan Damgard. Zero-knowledge proofs for finite field arithmetic or: Can zero-knowledge be for free? In Advances in Cryptology−Crypto'98,vol.1462 of lecture notes in Computer Science,pp.421-441.Springer-Verlag, Berlin,1998.
【発明の開示】
【発明が解決しようとする課題】
【０００８】
しかしながら、安全性証明の盗用・悪用防止に開し、既存のゼロ知識証明携帯プログラム配信方式は、秘匿できる情報の制約により実際的な効用に限界がある。このプログラムに添付して配信される安全性証明は、実際には証明本体と、プログラム及び証明本体を正しく開連づけるのに必要な不変条件（プログラムの各ポイントで成立すべき条件式）との２種類から構成されている。
【０００９】
ここで、既存のゼロ知識証明携帯プログラム配信方式が秘匿するのは証明本体に限られている。すなわち、不変条件は証明本体と異なり秘匿されないため、不変条件を利用した攻撃を防ぐことができない。
一般に不変条件はプログラムの実行時の振舞いに開する重要な情報を含み、その情報を用いた解析により、難読化（例えば、非特許文献５参照）や、透かしの挿入（例えば、非特許文献６及び７参照）などの様々な操作をプログラムに施すことができる。そこで，不変条件も証明とともに秘匿する新たな枠組みを示す必要があった。
上述した従来技術についての比較テーブルを図１９に示す。
【００１０】
本発明は、このような事情に鑑みてなされたもので、既存のゼロ知識証明携帯プログラム配信方式においては公開せざるを得なかった不変条件を秘匿し、不変条件と証明本体との両方を隠すことにより、不変条件と証明本体とに基づいたリバースエンジニアリングの危険性を削減し、配信プログラムの耐タンパ性を本質的に向上させる耐タンパ証明携帯プログラム配信システム及びその方法を提供することにある。
【課題を解決するための手段】
【００１１】
本発明の耐タンパ証明携帯プログラム配信方法は、開発者側が作成したプログラムｆを送信装置により利用者側に配信する際に、開発者側は前記プログラムｆが安全に実行可能であることを利用者側に示し、利用者側は受信装置により受信した前記プログラムｆを実行前に該プログラムｆが安全に実行可能であることを、開発者側の送信装置と対話的に通信しながら検証する耐タンパ証明携帯プログラム配信方法であり、開発者側が作成したプログラムｆが正しいことを示すために、プログラムｆと、プログラムｆを実行する際に、プログラム中の複数ポイントで成立すべき不変条件からなる不変条件列を生成する第１のステップと、前記不変条件列に対するダミーの不変条件を複数含む不変条件列候補集合を生成する第２のステップと、不変条件列候補集合に基づいて、プログラムｆの安全性を証明する命題論理式を生成する第３のステップと、前記命題論理式を算術化する第４のステップと、開発者側と利用者側とにおいて、ゼロ知識証明プロトコルに従った対話的通信を行い、前記算術化された量化命題論理式の計算結果が真であるか偽であるかを判定し、真である場合にプログラムｆを実行する第５のステップとを有することを特徴とする耐タンパ証明携帯プログラム配信方法。
【００１２】
本発明の耐タンパ証明携帯プログラム配信方法は、前記第４のステップにおいて、開発者側がゼロ知識証明プロトコルにより、一方向性準同型写像を用いたコミットメント関数を用いて、前記命題論理式の部分証明を、利用者側に送信することを特徴とする。
【００１３】
本発明の耐タンパ証明携帯プログラム配信システムは、開発者側が作成したプログラムｆを送信装置により利用者側に配信する際に、開発者側は前記プログラムｆが安全に実行可能であることを利用者側に示し、利用者側は受信装置により受信した前記プログラムｆを実行前に該プログラムｆが安全に実行可能であることを、開発者側の送信装置と対話的に通信しながら検証する耐タンパ証明携帯プログラム配信システムであり、開発者側が作成したプログラムｆが正しいことを示すために、プログラムｆと、プログラムｆを実行する際に、プログラム中の複数ポイントで成立すべき不変条件からなる不変条件列を生成するプログラム・不変条件列作成部と、前記不変条件列に対するダミーの不変条件を複数含む不変条件列候補集合を生成する不変条件列候補集合作成部と、不変条件列候補集合に基づいて、プログラムｆの安全性を証明する命題論理式を生成する安全性量化命題論理式生成部と、前記命題論理式を算術化する算術化部と、開発者側と利用者側とにおいて、ゼロ知識証明プロトコルに従った対話的通信を行い、前記算術化された量化命題論理式の計算結果が真であるか偽であるかを判定し、真である場合にプログラムｆを実行するゼロ知識証明プロトコル部とを有することを特徴とする。
【００１４】
本発明の耐タンパ証明携帯プログラム配信システムは、前ゼロ知識証明プロトコル部が、開発者側がゼロ知識証明プロトコルにより、一方向性準同型写像を用いたコミットメント関数を用いて、前記命題論理式の部分証明を利用者側に送信することを特徴とする。
【発明の効果】
【００１５】
以上説明したように、本発明によれば、証明本体ｐの秘匿だけでなく、既存方式においては公開せざるを得なかった不変条件列をも秘匿したまま、プログラムが正しく安全に動作することの数学的証明を効率的に検証する手段を与えており、これにより、悪性プログラムの高精度な実行前の検出及び駆除の処理を実現できる。
すなわち、本発明によれば、安全性証明の内容を秘匿し証明の盗用・悪用を防ぐ効率的なプロトコルを提供しており、これにより証明情報に基づくリバースエンジニアリングの防止が実現できる。
【００１６】
特に、本発明によれば、既存方式において、公開せざるを得なかった不変条件を秘匿し、不変条件及び証明本体の両方を利用者に対して隠すことにより、不変条件と証明本体とに基づくリバースエンジニアリングを防止し、配信プログラムの耐タンパ性を本質的に向上させている。
さらに、本発明によれば、不変条件と証明本体との所有者が、正規のプログラム開発者に限られるため、不変条件および証明本体の所有をプログラム著作権の保持とみなすことも可能になるという効果を併せ持つこととなる。
このように、本発明によれば、ネットワークを介したプログラム配信において、悪性プログラムによるホストヘの攻撃と、悪意のあるホストによるプログラムヘの攻撃との、双方を同時に防止することが可能なセキュリティ技術を提供することができる。
【発明を実施するための最良の形態】
【００１７】
＜本発明の概要＞
以下に、本発明によるプログラム配信方法の概要を説明する。
従来の定式化においては、プログラムの安全性は以下の（１）式に示すように定義されていた（例えば、非特許文献２参照）。
【００１８】
【数１】
【００１９】
すなわち、配信するプログラムｆと、以下の（２）式に示す不変条件の列（不変条件列）の組が安全性を満たしている（以下、集合Safeに含まれると表記する）とは、プログラムｆのすべての実行パスpathについて、以下に示す（３）式が成立することの数学的証明ｐが存在することとして定義される。
【００２０】
【数２】
【００２１】
【数３】
【００２２】
論理式である上記（３）式は、「前条件Preが成立する状況でプログラムｆをそのひとつの実行パスpathに沿って実行した場合、必ず後条件Postが成立しており、しかもプログラムｆの実行時には、利用者の要求する安全性が満たされる」ことを表わす論理式であり、プログラムｆと不変条件列を用いて計算される。ここで、上記前条件Preは「プログラムｆを実行する直前に成立すべき条件」を示し、上記後条件Postは「プログラムｆの実行した直後に成立すべき条件」を示している。
なお、プログラムｆの入出力仕様を規定する前条件Preおよび後条件Postも不変条件の一種であるが、本発明においては別の扱いとする。そして、上述した定義は以下に示す同値な定義式である（４）式へ容易に変形することができる。
【００２３】
【数４】
【００２４】
一般的に、（４）式における以下の（５）式の述語は、プログラムｆと不変条件列とについての多項式時間計算述語である。このため、この上記（４）式による定義は、集合Safeが計算量クラスco-NPに属していることを表しており、より正確に言うと、co-NP完全である（例えば、非特許文献２参照）。ここで、計算量クラスco-NPは、以下に示す（６）式に等しい。上述した説明の補足として、非決定性多項式時間限定アルゴリズムで計算可能な集合のクラスをNPと言い、上記co-NP完全とは、補集合がNPに属する集合のクラスco-NPの中において、最も計算するのが難しい集合のことを指している。
【００２５】
【数５】
【００２６】
【数６】
【００２７】
したがって、集合Safeに対するゼロ知識対話型証明プロトコル（例えば、非特許文献９，１０参照）を構成することが可能となり、不変条件列をアノテーションとして持つプログラムｆの安全性を、証明ｐそのものを提示することなく利用者に納得させることが可能となっている。例えば、以下に示すステップにより行われるゼロ知識証明携帯プログラム配信方法（例えば、非特許文献４参照）。すなわち、このゼロ知識証明携帯プログラム配信方法は、開発者側が作成したプログラムｆを送信装置により利用者側に配信する際に、開発者側は前記プログラムｆが安全に実行可能であることを利用者側に示し、利用者側は受信装置により受信した前記プログラムｆを実行前に該プログラムｆが安全に実行可能であることを、開発者側の送信装置と対話的に通信しながら検証する証明携帯プログラム配信方法である。
【００２８】
そして、上記証明携帯プログラム配信方法においては、開発者側が作成したプログラムｆが正しいことを示すために、プログラムｆと、プログラムｆを実行する直前に成立すべき条件である前条件Preと、プログラムｆの実行直後に成立すべき条件である後条件Postとから検証論理式｛Pre｝ｆ｛Post｝を検証論理式生成部により生成する第１のステップと、上記検証論理式が妥当であることを示すためにある論理体系Ｔ内で証明し、安全性証明ｐを、安全性証明作成部により作成する第２のステップと、開発者側が得られた安全性証明ｐをもとに利用者側との間でゼロ知識証明プロトコル部により対話的に通信を行い、送信したプログラムｆが、Safe＝｛ｆ｜Ｔにおける｛Pre｝ｆ｛Post｝の証明ｐが存在する｝によって定義される安全なプログラムの集合Safeに属することを利用者に確認させる第３のステップと、利用者側が、開発者側から送信されたプログラムｆが前記集合Safeに属することを確認した後に該プログラムｆを実行する第４のステップとにより、ゼロ知識証明の処理を行っている。
【００２９】
一方、本発明は、安全なプログラムの全体Safeを、以下の定義式である（７）式に示すように一般化することを最も主要な特徴としている。
【００３０】
【数７】
【００３１】
不変条件列を量化子∃によって束縛することにより、集合Safeの計算量はより複雑化して、（８）式に示すクラスに属することになる。
しかしながら、依然としてゼロ知識対話型証明プロトコルを構成可能な上限クラスPSPACE(決定性多項式領域限定アルゴリズムで計算可能な集合のクラスであり、クラスNP，co-NP，あるいは（８）式のクラスよりもはるかに大きいと考えられている)に抑えられているため、集合Safeに対するゼロ知識対話型証明プロトコルが非特許文献８，９，１０の方法（対話的・確率的手法に基づく効率的な証明検証技法）を応用することにより構成可能である。
【００３２】
【数８】
【００３３】
上述してきたように、本発明は、安全性の定式化における不変条件の扱い方に工夫を凝らすことにより、証明本体ｐの秘匿だけでなく、既存方式においては公開せざるを得なかった不変条件列をも秘匿したまま、プログラムｆの安全性を利用者に納得させることを可能にする、新しいプログラム配信方法を実現している。
【００３４】
＜耐タンパ証明携帯プログラム配信システムの構成＞
以下、本発明の一実施形態によるプログラム配信方法を実現する耐タンパ証明携帯プログラム配信システムを図面を参照して説明する。図１は同実施形態の構成例を示すブロック図である。
この図１の構成としては、説明のために、最も基本的な例題のひとつである、機械語プログラムのメモリ安全性・型安全性を対象としているが、プログラム言語や検証対象となる安全性は一般に多岐に渡るため、それらに応じて構成を適宜修正・拡張しても良い。
開発者（証明者）側装置１０は，プログラム・不変条件列・不変条件列侯補集合作成部１００，プログラム・不変条件列侯補集合送信部１０１，安全性量化命題論理式生成部１０２，算術化部１０３及びヒント（部分証明）作成・送信部１０４を有している。
【００３５】
一方、利用者（検証者）側装置２０は、プログラム入出力仕様作成・送信部２００，プログラム・不変条件列侯補集合受信部２０１，安全性量化命題論理式生成部２０２，算術化部２０３，ヒント（部分証明）受信・検証部２０４及び乱数生成・送信部２０５を有している。
上述した１１構成部各々のなかにおいて、プログラム入出力仕様作成・送信部２００と、プログラム・不変条件列・不変条件列候補集合作成部１００の２つは、他の９個の構成部がオンライン・リアルタイムで処理されるべきものであるのに対し、その前処理として実行を行う構成部である。
また、ヒント(部分証明)作成・送信部１０４,ヒント(部分証明)受信・検証部２０４及び乱数生成・送信部２０５各々は、ゼロ知識証明プロトコル部３０に設けられている。
【００３６】
この本発明におけるゼロ知識証明プロトコル部３０において、ヒント（部分証明）作成・送信部１０４は、ヒント（部分証明）受信・検証部２０４との間で対話型プロトコルを実行する。このとき、ヒント（部分証明）受信・検証部２０４は、乱数生成・送信部２０５により乱数を発生させ、該乱数によりヒント（部分証明）作成・送信部１０４から転送されるヒント情報を指定する。そして、ヒント（部分証明）受信・検証部２０４は、プログラムｆが安全に実行可能であることを確認した後、プログラムｆを実行する。
また、本発明の最も主要な構成は、ゼロ知識証明プロトコル部３０の前段における、プログラム・不変条件列・不変条件列侯補集合作成部１００，プログラム・不変条件列侯補集合送信部１０１，安全性量化命題論理式生成部１０２，算術化部１０３，プログラム入出力仕様作成・送信部２００，プログラム・不変条件列侯補集合受信部２０１，安全性量化命題論理式生成部２０２，算術化部２０３の各部である。
【００３７】
以下に、上述した本発明の主要な構成について説明する。
プログラム入出力仕様作成・送信部２００は、プログラムの利用者がプログラムの入出力仕様を規定するために作成及び入力した、プログラムを実行する直前および直後に成立すべき条件である前条件Ｐｒeおよび後条件Ｐｏｓｔを開発者（証明者）側装置に対して送信する。これにより、利用者は、自身の作成した上記前条件Ｐｒｅ及び後条件Ｐｏｓｔを公開しておく。例えば、利用者は、自然数の列の総和を求めるプログラムを利用したい場合、「入カレジスタは自然数のリスト型を持つ」という前条件Ｐｒｅと、「出力レジスタは自然数の型を持つ」という後条件Ｐｏｓｔを、プログラム入出力仕様作成・送信部２００により生成し、開発者（証明者）側装置１０へ送信し、開発者に対して事前に公開しておく。
【００３８】
さらに、プログラム入出力仕様作成・送信部２００は、プログラムを実行する際に、いかなる安全性を要求するかについての、利用者が入力する条件も、開発者（証明者）側装置１０に対して送信する。すなわち、利用者は、プログラムを実行する際に、いかなる安全性を要求するかについての、利用者が入力する条件も、開発者に対して事前に公開しているものとする。例えば、上記条件は、プログラム実行中に禁止されたメモリ領域へのアクセスが皆無であるという性質(メモリ安全性)に関する要求などである。
【００３９】
プログラム・不変条件列・不変条件列候補集合作成部１００は、開発者が作成した、利用者の規定した入出力仕様を満たす安全なプログラムｆが入力されると、これらの入出力仕様や安全性を満たすことを示す際、プログラム中における適切な複数ポイントで成立すべき、（２）式による条件式(不変条件)を抽出（発見）し、この発見した不変条件の列から不変条件列を作成する。
また、プログラム・不変条件列・不変条件列候補集合作成部１００は、後にこの不変条件列を秘匿したまま安全性を利用者に認識させるため、不変条件列を作成するのと同時に、ダミーの不変条件列を適宜複数個用意し、これらダミーの不変条件列を複数用いて不変条件列侯補集合を作成する。
すなわち、プログラム・不変条件列・不変条件列候補集合作成部１００は、以下に示す（９）式の論理式を満たすプログラムｆ及び不変条件列候補集合を、論理式成立の証拠とも見なせる（２）式の不変条件列とともに作成する。
【００４０】
【数９】
【００４１】
プログラム・不変条件列候補集合送信部１０１は、プログラム実行時の振る舞いに関する重要な情報を含んだ（２）式による不変条件列を秘匿したまま、プログラムｆと、作成した不変条件列候補集合とを利用者（検証者）側装置２０へ送信する。
プログラム・不変条件列候補集合受信部２０１は、プログラム・不変条件列候補集合送信部１０１から、プログラムｆと不変条件列候補集合とを受信する
【００４２】
安全性量化命題論理式生成部１０２及び２０２と、算術化部１０３及び２０３とは、開発者側（証明者）装置１０と利用者（検証者）側装置２０とで同じ機能の構成を用いる。 上記安全性量化命題論理式生成部１０２は、プログラムｆが安全であることを表す上記（９）式に示す論理式と同値な、以下の（１０）式に示す量化命題論理式（量化子を用いた命題論理式）を、不変条件列候補集合に基づき生成する。
【００４３】
【数１０】
【００４４】
ここで、上記（１０）式のような量化命題論理式は、以下の理由により容易に生成可能である。すなわち、（２）式に示す不変条件列を量化子∃（特称量化子）によって束縛した場合のメモリ安全・型安全な機械語プログラムの全体(つまり、（９）式に示す論理式を満たすプログラムｆの全体)は（８）式に示す計算量クラスに属する。
一方、真なる量化命題論理式の全体は、より計算量の大きいとされるPSPACE完全である。したがって、プログラムｆが安全か否かといった安全性検証の問題は、量化命題論理式の真偽判定問題に還元可能であり、この還元アルゴリズムを用いることにより、上記（１０）式に示す量化命題論理式は生成可能である．
【００４５】
算術化部１０３（２０３）は、上記（１０）式に示す量化命題論理式の算術化を行う。ここで、量化命題論理式を算術化することにより、この量化命題論理式の真偽判定を数式の値の零判定に置き換えることができる。実際に、命題変数Ｘを自然数変数Ｘに算術化し、同様に、論理結合子各々を算術化、すなわち論理結合子∨を「＋」に、論理結合子∧を×に、論理結合子¬Ｘを１−Ｘに、算術化し、また、量化子∃を和Σに、そして量化子∀（全称量化子）を積Πに変換することで算術化は完了する。これにより、上記（１０）式による量化命題論理式が真であることは、以下の（１１）式の計算結果が零でないことと同値となる。
【００４６】
【数１１】
【００４７】
ゼロ知識証明プロトコル部３０において、ヒント(部分証明)作成・送信部１０４，ヒント(部分証明)受信・検証部２０４，乱数生成・送信部２０５各々が、すでに述べたように開発者及び利用者間における対話的通信を行い、上記（１１）式が零とならないことを利用して、利用者に対してプログラムｆの安全性を納得させる。
一方、利用者もゼロ知識証明プロトコル部３０において、開発者と対話的通信を行い，上記（１１）式が確かに零でないこと、すなわち受信したプログラムｆが安全であることを確認した後に、このプログラムｆに対して処理を実行させる。
【００４８】
上記（８）式により示される計算クラスにおける計算量は決して小さくはないが、ゼロ知識証明プロトコル部３０は、非特許文献８及び９の対話型証明プロトコルの理論を応用することにより、確率的ではあるが極めて高い精度により、効率的に（１１）式が零でないことを証明・検証することができる。
また、プログラムの耐タンパ性は、（２）式による不変条件列を検出（発見）・作成する多項式時間アルゴリズムが存在しないこととして、数学的に表現される。
すなわち、安全なプログラムｆの全体が（８）式により示される計算クラスにおいて完全であることが示されれば、以下の（１２）式が成り立たない限り、上記多項式時間アルゴリズムは存在しない。
【００４９】
【数１２】
【００５０】
＜利用者側における前条件及び後条件の作成＞
次に、機械語プログラムのメモリ安全性及び型安全性を例にとり、本発明の実施方法について説明する。ここでは、Alphaアセンブリ言語で記述された機械語プログラム（プログラムｆ）を、利用者（検証者）側装置２０（Standard ML言語の型つき中間言語コンパイラ実行時システム）が受信し、この機械語プログラムをメモリ安全及び型安全に実行する一連の流れ（非特許文献１，２，４で展開されている）を用い、耐タンパ証明携帯プログラム配信システムの動作例を説明する。はじめに、利用者がプログラム入出力仕様作成・送信部２００にて行う、前条件Ｐｒｅ，後条件Ｐｏｓｔの作成と、開発者側に対する公開について説明する。
【００５１】
まず、安全性要求，前条件Ｐｒｅ及び後条件Ｐｏｓｔについて、以下に簡単に説明する。利用者（検証者）側装置２０は、代表的な関数型言語であるStandard ML言語の型つき中間言語コンパイラ実行時システムを搭載している（例えば、アプリケーションプログラムがインストールされている）と仮定する。この利用者（検証者）側装置２０は、中間言語コンパイラ実行時システムにおいて、Alphaアセンブリ言語で記述された機械語プログラムを、開発者側（証明者）装置１０から受信し、メモリ安全かつ型安全に実行しようとしていると仮定する．
この利用者（検証者）側装置２０は、その安全性要求やプログラムの前条件Ｐｒｅ及び後条件Ｐｏｓｔといった仕様を、型（例えば、データの種類または内容：整数型，実数型，文字型、アドレス型など）の概念を用いて規定する。例えば、式ｅが型τを持つことをｅ：τと記述し、本実施形態において利用される式と型とは以下に示す（１３）式のように定義される。
【００５２】
【数１３】
【００５３】
上記（１３）式において、ｎは３２ビットで表わされる自然数であり、各ｒ1はAlphaレジスタ，sel（e）はメモリ番地ｅの内容を指している。ここで、型intの値は３２ビットで表される自然数である。型τ1＊τ2の値は、型τ1と型τ2の値が格納された隣接するメモリ番地へのポインタである。また、型τ1＋τ2の値は隣接するメモリ番地へのポインタであり、最初の番地にはタグ（０または１）が格納されており、ダグが「０」ならば型τ1の値が、一方、ダグが「１」ならば型τ2の値が続きの番地に格納される。さらに、型addrの値は、安全に読み出し可能なメモリ番地を表わしている。
なお、加法および減法は厳密には２３２を法とするものであるが、説明を簡単とするため、ここでは法演算を省略して記述する。
【００５４】
そして、利用者は上述した型の概念を用い、利用者（検証者）側装置２０において、安全性要求を事前に規定する。本実施形態における安全性要求は、図２に示す公理からなる一階述語論理体系Ｔとして規定する。
また、利用者は、すでに述べたように、プログラムが実行される直前および直後に成立すべき条件を、それぞれ前条件Ｐｒｅと後条件Ｐｏｓｔとして規定し、事前に開発者側に対して公関しておかなければならない。
本実施形態における前条件Ｐｒｅおよび後条件Ｐｏｓｔは、上述した型を用いて、図３に示すように規定されているとする。
【００５５】
＜機械語プログラムの作成＞
本実施形態におけるプログラム・不変条件列・不変条件列候補集合作成部１００にて、開発者に作成されるプログラムの例として、Alphaアセンブリ言語で記述された簡単なプログラム（プログラムｆ）を図４に示す。このプログラムは、コンピュータのレジスタｒ1, ｒ2，ｒ3の値に応じて分岐した後、単純なループに入る処理を示している。
ここで、上記プログラムは、図３に示す前条件Ｐｒｅおよび後条件Ｐｏｓｔを入出力仕様として満たし、メモリ安全かつ型安全に実行されることを意図して作成されたものである。これらの前条件Ｐｒｅおよび後条件Ｐｏｓｔは、例えば補助的な命令であるINV命令（Invariant：不変条件）を用い、図４に示すプログラム中に表明されている。なお、不変条件列もINV命令を用いて表記（表明）されるが、この表記については後に詳述する。
ここで、実は、図４のプログラム例において、プログラムがメモリ安全かつ型安全であることと、以下に示す（１４）式に定義する量化命題論理式が偽であることが同値となるように作成されている。
【００５６】
【数１４】
【００５７】
そして、プログラム・不変条件列・不変条件列候補集合作成部１００は、命題変数Ｘiの真偽を、番地４（ｒi） (ダグが格納された番地０（ｒi）の続きの番地)が型intであるか、あるいは型intの組へのポインタであるかということにエンコードする。
さらに、プログラム・不変条件列・不変条件列候補集合作成部１００は、レジスタｒ（3＋i）に、上記番地に記憶された内容を読み込むことにより、真偽を、ｒ（3＋i）：intあるいはsel(r3+i):intの成立へと変換する。
【００５８】
＜不変条件およびプログラム安全性＞
すでに述べたように、プログラムｆ（機械語プログラム）が安全なプログラムの全体Safeに属すると言うことは、（９）式に示す論理式が成立することであると定義された。ここで、各pathによってインデックス付けされた部分式である（３）式の全体を特に検証論理式と呼ぶこととする。この検証論理式は、プログラム・不変条件列・不変条件列候補集合作成部１００内部に設けられたFloyd流の検証論理式生成器によって、プログラムｆ，前条件Ｐｒｅ，後条件Ｐｏｓｔ及び不変条件列から自動的に生成される。
【００５９】
上記検証論理式生成器における検証論理式の生成の規約を図５に示し、この図の規約を用いて図４のプログラムに対する検証論理式が実際に生成されていく様子を図６及び図７に示す。
この検証論理式の生成において、必須の情報として不変条件列がある。図４のプログラム中の前方へのジャンプ命令の行き先が必ずINV命令であるとの規約を置くことにより、検証論理式生成器は１パスで容易に検証論理式を生成することができる。
本実施形態における図４のプログラムにおいても、１０行目のラベルＬcが貼られた（マーキングされた）ポイントで常に成立すべき不変条件Ｉを明らかにしておく必要がある。本実施形態における不変条件Ｉを図８に示す。
図８に示す不変条件Ｉを用いることにより、最終的に得られる検証論理式は、図９に示すように、ＶＣ0⇒ＶＣ1を表す９個の論理式と、ＶＣ10⇒ＶＣ11を表わす２個の論理式をあわせた計１１個の論理式となる。ここで、「⇒」は「含意」を示す論理結合子であり、「Ｐ⇒Ｑ」が「ＰならばＱ」となる。
【００６０】
上述した図９に示す各検証論理式は、その妥当性の証拠を得るため、一階述語論理体系Ｔにおいて証明される。そして、検証論理式が全て証明された場合、すなわち、各pathについて（３）式が一階述語論理体系Ｔ内で証明された場合、Standard ML言語の型つき中間言語コンパイラ実行時システムにおいて、前条件Ｐｒｅが成立する状況においてプログラムｆを実行し、計算が終了すると必ず後条件Ｐｏｓｔが成立し、しかもプログラムｆの実行中に用いられる全ての値に対して適切な型がつくため、このプログラムｆの実行時のメモリアクセスが安全であることが保証される。
【００６１】
例えば、図４のプログラム例も、検証論理式が全て証明可能であり、メモリ安全かつ型安全であることが保証される。
また、図９の検証論理式が示唆するように、プログラム中に条件分岐命令がｎ回続いた場合、このｎの指数オーダの実行パスが存在することになる。ここで、個々の検証論理式の証明は、短く多項式時間で検証することが可能であるが、全ての検証論理式を証明するとなると証明は指数オーダのサイズとなる。
実際、図４のプログラムの安全性、すなわち検証論理式の証明可能性は、ＶＣ0⇒ＶＣ1に対応する部分が上記（１４）式が偽であることと同値である。
また、ＶＣ10⇒ＶＣ11に対応する部分が以下に示す（１５）式が真であることと同値である。
【００６２】
【数１５】
【００６３】
（１５）式が真であることは容易に確認できるが、（１４）式が偽であることの証明は本質的に難しい。
【００６４】
＜不変条件の秘匿＞
開発者（証明者）側装置１０において発見・計算された（２）式の不変条件列をそのまま利用者（検証者）側装置２０に送信することにより、プログラムｆの安全性を開発者及び利用者の双方において、安全性量化命題論理式生成部１０２（及び２０２）により容易に定義することができる。
しかしながら、本発明の技術思想においては、不変条件列に基づくリバースエンジニアリングを防止し、配信するプログラムの耐タンパ性を高めることを目的としているため、悪意を持っている可能性もある利用者に上記不変条件列を明示的に送信することは避ける必要がある。
【００６５】
そこで、開発者（証明者）側装置１０は、本来の（２）式に示す不変条件列にダミーの条件を適宜加えた不変条件列候補集合を、利用者（検証者）側装置２０に送信する。この不変条件列候補集合が十分大きい場合、利用者（検証者）側装置２０が、その不変条件列候補集合中から正解の不変条件を選択することが困難となる。
図４に示す本実施形態のプログラム例におけるダミーの不変条件を、図１０に示す不変条件Ｉ＊とする。すなわち、不変条件候補集合を｛Ｉ，Ｉ＊｝とする。ただし、ダミーであるためには、不変条件にはなり得ないこと、例えば以下の（１６）式に示す論理式を満たすことが望ましい。本実施形態におけるダミーの不変条件Ｉ＊はこれを満たしている。
【００６６】
【数１６】
【００６７】
また、不変条件Ｉに基づくリバースエンジニアリングを防止するためには、不変条件列候補集合は大きいほど都合がよい。
しかしながら、一般にプログラム中の各ポイントにおいて追加されるダミーの不変条件は、１つでよい。すなわち、本実施形態においては、プログラム中に不変条件が表明されるポイントは１つであるが、一般にｋ個の不変条件Ｉが表明されている場合、不変条件列候補集合のサイズは組合せにより２ｋとなるからである。
ダミーの不変条件Ｉ＊を用いたときの検証論理式の証明可能性は、ＶＣ0⇒ＶＣ1に対応する部分が以下に示す（１７）式が偽であることと同値である。
【００６８】
【数１７】
【００６９】
また、ＶＣ10⇒ＶＣ11に対応する部分が以下に示す（１８）式が真であることと同値である。
【００７０】
【数１８】
【００７１】
そして、プログラム・不変条件列候補集合送信部１０１は、機械語プログラム，不変条件列及び不変条件列候補集合を、安全性量化命題論理式生成部１０２に出力するとともに、プログラムｆ及び不変条件列候補集合を、プログラム・不変条件候補集合受信部２０１に対して送信する。
【００７２】
＜安全性の量化命題論理式への翻訳＞
上述したように、不変条件候補集合が｛Ｉ，Ｉ＊｝である場合、安全性量化命題論理式生成部１０２（及び２０２）は、プログラムｆが安全であることを表す（９）式に示される論理式を、以下に示す（１９）式の構成に変換する（書き換える）。本実施形態においては、この書き換えにより、安全性を（８）式の計算クラスから、（１２）式に示すco-NPに還元している。
【００７３】
【数１９】
【００７４】
そして、（１９）式の論理式は、以下に示す（２０）式が真であること、すなわち、以下に示す（２１）式が偽であることと同値となる。
【００７５】
【数２０】
【００７６】
【数２１】
【００７７】
＜量化命題論理式の算術化＞
次に、算術化部１０３（及び２０３）は、上記（２１）式の算術化を行うことにより、量化命題論理式の真偽判定を数式の値の零判定に置き換える。
実際の処理としては、命題変数Ｘを自然数変数Ｘに、∨を＋に、∧を×に、¬Ｘを１−Ｘに、そして量化子∃を和Σに変換することにより算術化は完了する。ここで、本実施形態における（２１）式に示す量化命題論理式が偽であることは、以下の（２２）式の計算値が零であることと同値である。
【００７８】
【数２２】
【００７９】
＜安全性のゼロ知識証明＞
次に、ゼロ知識証明プロトコル部３０における、上記（２２）式が零であることを証明するゼロ知識証明プロトコルの実行例を、図１１，１２，１３，１４，１５，１６，１７及び図１８を用いて説明する。
開発者（証明者）側装置１０と利用者（検証者）側装置２０とにおける開発者及び利用者の対話処理は実質的に６ラウンドからなっている。ここで、各ラウンドがひとつのΣ記号に対応している。
【００８０】
上記各ラウンド毎に、ひとつの数式が提示され,利用者はその値の正当性を開発者との対話を通じて検証することになる。なお、実際のプロトコルにおいては、セキュリティパラメータ(本実施形態では一例として数式の長さ）ｌに対応して決定される長さΟ（ｌ）の適当な素数ｑを法とした計算が行われるが、ここでは省略する。
開発者（証明者）側装置１０におけるヒント（部分証明）作成・送信部１０４は、各ラウンドで提示された数式からΣ記号をひとつ除去し、それを展開して得られた１変数多項式の係数をヒント情報として、利用者（検証者）側装置２０のヒント（部分証明）受信・検証部２０４へ送信する。例えば、ヒント（部分証明）作成・送信部１０４は、図１１の第１ラウンドの「情報１」を、ヒント（部分証明）受信・検証部２０４へ送信する。
【００８１】
次に、利用者側のヒント（部分証明）受信・検証部２０４は、各ラウンドごとに自動的に決まる検証タスクを実行する。例えば、ヒント（部分証明）受信・検証部２０４は、ヒント（部分証明）作成・送信部１０４から「情報１」を受信することにより、「タスク１」による検証処理を実行する。
具体的な例として、ヒント（部分証明）受信・検証部２０４は、受け取った多項式の０と１とにおけるそれぞれの値の和を計算し、それの計算結果が期待される値と等しいか否かの検証を行う。
そして、ヒント（部分証明）受信・検証部２０４は、この検証をパスすると（計算結果が期待される値と等しいことを検出すると）、ヒント情報の妥当性を検証する新しい、すなわち次のラウンド（例えば、第１ラウンドの次は第２ラウンド）に移行する。
【００８２】
次に、Σ記号のひとつ少ない新しい数式が提示され、開発者（証明者）側装置１０によるヒントの送付と、利用者（検証者）側装置２０による多項式の０と１とにおけるそれぞれの値の和を計算し、計算結果の値の検証が繰り返される。このゼロ知識証明プロトコルのプロセスは、Σ記号を含まない数式の自明な検証に帰着されるまで繰り返される。
ここで、不正な開発者が妥当でないヒントを送付した場合、この攻撃に対処するため、ヒント（部分証明）受信・検証部２０４は、開発者が各ラウンドにてΣ記号の一つ少ない数式を提示する際に、変数に代入する定数を、乱数生成・送信部２０５により生成させ、ヒント（部分証明）作成・送信部１０４へ送信する。
【００８３】
ただし、開発者（証明者）側装置１０がヒントとして、多項式の係数そのものを送付してしまうと、不変条件と証明本体とに開する情報が利用者に対して漏れてしまう。
そこで、開発者（証明者）側装置１０は、１変数多項式の係数そのものではなく、係数のコミットメントを送付することにより、プロトコルをゼロ知識化する。
すなわち、本実施形態においては、プログラム安全性の証明・検証プロトコルをゼロ知識化する際に、一方向性準同型写像を用いたコミットメント(秘密証拠供託)関数を用いる。
情報の内容自体を秘密に保ったまま、内容の事後変更を不可能とする十分な証拠を予め相手に渡しておくために、コミットメント（秘密証拠供託）関数commitを本プロトコルにおいて利用する。セキュリティパラメータｌと長さＯ（ｌ）の素数ｑに対し、証明者は秘密にしたい情報ａ∈ {０，１，…，ｑ−１}と乱数r∈｛０，１｝ｌをもとに証拠commit(a、 r)∈｛０，１｝ｌを計算して、利用者（検証者）側装置２０へ送信する（コミットメント・フェーズ）。
【００８４】
そして、証明者によるａとｒの開示を受けた検証者は、これらの情報に基づき先の証拠が確かにcommit(a、r)であることを計算し、情報ａが事後変更されていないことを確認する（開示フェーズ）。
このような秘密証拠供託の実現は、関数commitに課せられた次の３つの性質により保証される。
「秘匿性」：commit (a，r)の値から秘密情報ａに間する知識を得ることは計算論的に困難である性質、すなわち、異なるふたつの秘密情報に対するコミットメントの確率分布は多項式時間識別不可能である性質である。
「束縛性」：commit（a、r）の値から秘密情報ａが一意に決まる性質である。すなわち、秘密情報ａに対する証拠commit（a、r）を受信した後に、ａ及びｒの開示を受け、先に受信した証拠が計算値commit（a、r）に一致するか否かをもって、秘密がａであったことを検証する場合、秘密情報の事後変更は不可能である性質である。
「準同型性」：与えられたふたつのコミットメントＡ ＝commit（a、r）およびＢ ＝commit（ｂ、r）から、commit（ａ＋ｂ mod ｑ，ｔ）およびcommit（ａ−ｂ mod ｑ，ｕ）が多項式時間で計算可能である。各コミットメントは乗法群の要素であるため、これらをそれぞれＡＢおよびＡＢ−１と記す。この性質から直ちに、コミットメントＡ＝commit（a、r）が与えられれば、任意の定数ｃに対して、commit(ca mod ｑ，ｓ)が多項式時間計算可能となる。これをＡＣと記す。
【００８５】
図１８においては、簡単のため適当なｒに対するcommit（a，r）をＣ(a)と略記していいる。これにあわせ、コミットメント間の等号Ｃ＝Ｃ’を、ＣとＣ’があるａに対し集合{commit(a，r)｜r}の要素であることと定義する。Ｃ（ａ）は同値関係＝による各同値類{commit(a，r)｜r}の代表元とみなせる。
上述した３つの性質(秘匿性、束縛性、準同型性)をもつコミットメント関数を実際に構成することができる（例えば、非特許文献１０参照）。そして、そのコミットメント関数を用いることにより、利用者（検証者）側装置２０において、利用者は係数のコミットメントのみから、係数自体を知ることなく、目的とする式のコミットメントを計算することが可能となる。
【００８６】
なお、図１における各部の機能を実現するためのプログラムをコンピュータ読み取り可能な記録媒体に記録して、この記録媒体に記録されたプログラムをコンピュータシステムに読み込ませ、実行することにより開発者（検証者）側装置１０及び利用者（検証者）側装置２０における各処理を行ってもよい。なお、ここでいう「コンピュータシステム」とは、ＯＳや周辺機器等のハードウェアを含むものとする。また、「コンピュータシステム」は、ホームページ提供環境（あるいは表示環境）を備えたＷＷＷシステムも含むものとする。また、「コンピュータ読み取り可能な記録媒体」とは、フレキシブルディスク、光磁気ディスク、ＲＯＭ、ＣＤ−ＲＯＭ等の可搬媒体、コンピュータシステムに内蔵されるハードディスク等の記憶装置のことをいう。さらに「コンピュータ読み取り可能な記録媒体」とは、インターネット等のネットワークや電話回線等の通信回線を介してプログラムが送信された場合のサーバやクライアントとなるコンピュータシステム内部の揮発性メモリ（ＲＡＭ）のように、一定時間プログラムを保持しているものも含むものとする。
【００８７】
また、上記プログラムは、このプログラムを記憶装置等に格納したコンピュータシステムから、伝送媒体を介して、あるいは、伝送媒体中の伝送波により他のコンピュータシステムに伝送されてもよい。ここで、プログラムを伝送する「伝送媒体」は、インターネット等のネットワーク（通信網）や電話回線等の通信回線（通信線）のように情報を伝送する機能を有する媒体のことをいう。また、上記プログラムは、前述した機能の一部を実現するためのものであっても良い。さらに、前述した機能をコンピュータシステムにすでに記録されているプログラムとの組み合わせで実現できるもの、いわゆる差分ファイル（差分プログラム）であっても良い。
【図面の簡単な説明】
【００８８】
【図１】本発明の一実施形態による耐タンパ証明携帯プログラム配信システムの構成例を示すブロック図である。
【図２】一階述語論理体系Ｔの内容を示す図である。
【図３】規定された前条件Ｐｒｅおよび後条件Ｐｏｓｔを示す図である。
【図４】検証対象となるプログラムの一例を示す図である。
【図５】検証論理式生成器における検証論理式の生成の規約を示す図である。
【図６】図５に示した検証論理式生成器の規約を用いて図４に示したプログラムに対する検証論理式が生成される様子を示す説明図。
【図７】図５に示した検証論理式生成器の規約を用いて図４に示したプログラムに対する検証論理式が生成される様子を示す説明図。
【図８】本実施形態における不変条件Ｉを示す図である。
【図９】不変条件Ｉを用いることにより、最終的に得られる検証論理式を示す図である。
【図１０】図４に示すプログラムに対するダミーの不変条件Ｉ＊を示す図である。
【図１１】ゼロ知識証明プロトコル部３０におけるゼロ知識証明プロトコルの実行例を示す図である。
【図１２】ゼロ知識証明プロトコル部３０におけるゼロ知識証明プロトコルの実行例を示す図である。
【図１３】ゼロ知識証明プロトコル部３０におけるゼロ知識証明プロトコルの実行例を示す図である。
【図１４】ゼロ知識証明プロトコル部３０におけるゼロ知識証明プロトコルの実行例を示す図である。
【図１５】ゼロ知識証明プロトコル部３０におけるゼロ知識証明プロトコルの実行例を示す図である。
【図１６】ゼロ知識証明プロトコル部３０におけるゼロ知識証明プロトコルの実行例を示す図である。
【図１７】ゼロ知識証明プロトコル部３０におけるゼロ知識証明プロトコルの実行例を示す図である。
【図１８】ゼロ知識証明プロトコル部３０におけるゼロ知識証明プロトコルの実行例を示す図である。
【図１９】従来技術と本発明との特性を比較したテーブルを示す図である。
【符号の説明】
【００８９】
１０…開発者（証明者）側装置
２０…利用者（検証者）側装置
１００…プログラム・不変条件列・不変条件列候補集合作成部
２００…プログラム入出力仕様作成・送信部
１０１…プログラム・不変条件列・不変条件列候補集合送信部
２０１…プログラム・不変条件列・不変条件列候補集合受信部
１０２，２０２…安全性量化命題論理式生成部
１０３，２０３…算術化部
１０４…ヒント（部分証明）作成・送信部
２０４…ヒント（部分証明）受信・検証部
２０５…乱数生成・送信部
【技術分野】
【０００１】
本発明は、ネットワークを介したプログラム配信において悪性プログラムによるホストヘの攻撃と、悪意のあるホストによるプログラムヘの攻撃との、双方を同時に防ぐセキュリティ技術としての耐タンパ証明携帯プログラム配信システム及びその方法に関する。
【背景技術】
【０００２】
今日、プログラム化された高機能コンテンツがＷＷＷブラウザや携帯端末に日常的にダウンロードされ実行されている。
また、パケットやノードなどのネットワーク構成要素をプログラマブルとすることで拡張性や耐故障性を増したアクティブネットワークの研究も進んでいる。
プログラムが流通する時代を迎え、悪性プログラムから計算機を守る新しい技術への需要が高まってきている。
【０００３】
ここで、上述したようなネットワークを介したプログラム配信においては、タイプの異なる次の２種類の攻撃を考慮する必要がある。
・タイプ１悪性プログラム
ウィルス・バッファ溢れのバグを悪用するプログラムなどによるホストコンピュータヘの攻撃。
・タイプ２悪意のあるホストコンピュータによるプログラムヘの攻撃
配布されたプログラムの解析・改ざん・リバースエンジニアリングなど。
【０００４】
上述したタイプ１の攻撃を防ぐための技術としては、プログラムに開発者の電子署名を付与し検証する方式，パタンマッチによるウィルス検知・駆除方式，仮想機械のバイトコード検証方式などが既に実用化されている。しかしながら、これらの方式はいずれも悪性プログラムの検出精度に限界があることが知られている。
この問題を解決する次世代技術として、証明携帯プログラム配信方式(Proof-Carrying Code)（例えば、特許文献１及び非特許文献１を参照）が提案されている。この証明携帯プログラム配信方式は、プログラム本体にそれが正しく安全に動作すること(例えば、与えられた入力条件のもとでプログラムを実行した場合、結果が出力条件を満たし、実行時には禁止されたメモリ領域へのアクセスがまったくないこと）の詳細な数学的証明を添付し両者を同時に流通させ、証明に誤りのあるプログラムを悪性として実行前に検出・駆除する方式である。このように、証明を精査することにより厳密なプログラム検証を行うため、精度の高い検出・駆除が可能である．
【０００５】
しかしながら、上述した証明携帯プログラム配信方式には、証明サイズが指数開数的に爆発するという問題がある。
この証明携帯プログラム配信方式の問題を解決するために、簡単な対話的通信により証明の部分的検証を繰り返す方式、すなわち、対話型証明携帯プログラム配信方式（例えば、特許文献２及び非特許文献２を参照）が提案されている。
【０００６】
一方、上記タイプ２の攻撃を防ぐための要素技術としては、難読化・暗号化・多様化・電子透かしなどが既に提案されている（例えば、非特許文献３参照）。
また、すでに述べたタイプ１の攻撃に対し有望な技術である証明携帯プログラム配信方式、または対話型証明携帯プログラム配信方式は、その証明に誤りのあるプログラムの検出処理の特性上、タイプ２の攻撃の防止に対しては弱い。すなわち、悪性プログラムからホストを守るために安全性の証拠として添付する証明自体が、逆に悪意のあるホストに盗用・悪用されかねないという問題があるからである。
【０００７】
一般に、安全性の証明は、プログラム本体から、必ずしも直ちに引き出せるとは限らず、プログラムの意味に開する様々な情報を含んでいる。
したがって、上記証明をそのまま流通させた場合、例えば証明を利用したリバースエンジニアリングなどを招くおそれを否定することができない。
証明携帯プログラム配信方式あるいは対話型証明携帯プログラム配信方式を拡張し、上記タイプ１の攻撃に対する優位性を保ちつつ、安全性証明の盗用及び悪用を防止する機能を追加した方式として、ゼロ知識証明携帯プログラム配信方式（例えば、非特許文献４参照）が提案されている。この非特許文献４に記載されているように、証明・検証プロトコルのゼロ知識化により、安全性証明の内容を秘匿しつつプログラムの安全性を利用者に納得させることができ、その結果、安全性証明の盗用・悪用を防ぐことが可能となる。
【特許文献１】ＵＳ Ｐａｔｅｎｔ ６,１２８,７７４
【特許文献２】特開２０００−７８１２６号公報
【非特許文献１】George C. Necula. Proof-carrying code. In Proceedings ofthe 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,pp.106-119,Paris,January 1997.ACM，ACM Press.
【非特許文献２】Yasuyuki Tsukada. Interactive and probabilistic proof of mobiele code safety. Automated Software Engineering. Vol.12,No2,pp.237-257,April 2005.
【非特許文献３】門田暁人，Clark Thomborson. ソフトウェアプロテクションの技術動向（前編）−ソフトウェア単体での耐タンパー化技術−．情報処理，Vol.46,No.4,pp.431-437,2005.
【非特許文献４】塚田恭章．対話型安全証明つきプログラム配信方式における証明の秘匿とその応用．情報処理学会論文誌，Vol.46,No.1,pp.236-246,2005.
【非特許文献５】門田暁人，高田義広，鳥居宏次. ループを含むプログラムを難読化する方法の提案．電子情報学会論文誌D-I,Vol.J80-D-I,No.7,pp.644-652,1997.
【非特許文献６】一杉裕志．ソフトウェア電子すかしの挿入法、攻撃法、評価法、実装法．夏のプログラミングシンポジウム報告集, pp.57-64.情報処理学会,July 1997.
【非特許文献７】門田暁人，松本健一，飯田元，井上克朗，鳥居宏次．Javaクラスファイルに対する電子透かし法．情報処理学会論文誌, Vol.41, No.11, pp.3001-3009, 2000.
【非特許文献８】Shafi Goldwasser, Silvio Micali, and Charies Rackoff．The Knowledge Complexity of Interactive Proof Systems, SIAM J. Computing, Vol. 18, No. 1, pp. 186-208 ，1989.
【非特許文献９】Adi Shamir. IP = PSPACE, Jpurnal of ACM, Vol.39, No.4, pp. 869-877，1992.
【非特許文献１０】Ronald Cramer and Ivan Damgard. Zero-knowledge proofs for finite field arithmetic or: Can zero-knowledge be for free? In Advances in Cryptology−Crypto'98,vol.1462 of lecture notes in Computer Science,pp.421-441.Springer-Verlag, Berlin,1998.
【発明の開示】
【発明が解決しようとする課題】
【０００８】
しかしながら、安全性証明の盗用・悪用防止に開し、既存のゼロ知識証明携帯プログラム配信方式は、秘匿できる情報の制約により実際的な効用に限界がある。このプログラムに添付して配信される安全性証明は、実際には証明本体と、プログラム及び証明本体を正しく開連づけるのに必要な不変条件（プログラムの各ポイントで成立すべき条件式）との２種類から構成されている。
【０００９】
ここで、既存のゼロ知識証明携帯プログラム配信方式が秘匿するのは証明本体に限られている。すなわち、不変条件は証明本体と異なり秘匿されないため、不変条件を利用した攻撃を防ぐことができない。
一般に不変条件はプログラムの実行時の振舞いに開する重要な情報を含み、その情報を用いた解析により、難読化（例えば、非特許文献５参照）や、透かしの挿入（例えば、非特許文献６及び７参照）などの様々な操作をプログラムに施すことができる。そこで，不変条件も証明とともに秘匿する新たな枠組みを示す必要があった。
上述した従来技術についての比較テーブルを図１９に示す。
【００１０】
本発明は、このような事情に鑑みてなされたもので、既存のゼロ知識証明携帯プログラム配信方式においては公開せざるを得なかった不変条件を秘匿し、不変条件と証明本体との両方を隠すことにより、不変条件と証明本体とに基づいたリバースエンジニアリングの危険性を削減し、配信プログラムの耐タンパ性を本質的に向上させる耐タンパ証明携帯プログラム配信システム及びその方法を提供することにある。
【課題を解決するための手段】
【００１１】
本発明の耐タンパ証明携帯プログラム配信方法は、開発者側が作成したプログラムｆを送信装置により利用者側に配信する際に、開発者側は前記プログラムｆが安全に実行可能であることを利用者側に示し、利用者側は受信装置により受信した前記プログラムｆを実行前に該プログラムｆが安全に実行可能であることを、開発者側の送信装置と対話的に通信しながら検証する耐タンパ証明携帯プログラム配信方法であり、開発者側が作成したプログラムｆが正しいことを示すために、プログラムｆと、プログラムｆを実行する際に、プログラム中の複数ポイントで成立すべき不変条件からなる不変条件列を生成する第１のステップと、前記不変条件列に対するダミーの不変条件を複数含む不変条件列候補集合を生成する第２のステップと、不変条件列候補集合に基づいて、プログラムｆの安全性を証明する命題論理式を生成する第３のステップと、前記命題論理式を算術化する第４のステップと、開発者側と利用者側とにおいて、ゼロ知識証明プロトコルに従った対話的通信を行い、前記算術化された量化命題論理式の計算結果が真であるか偽であるかを判定し、真である場合にプログラムｆを実行する第５のステップとを有することを特徴とする耐タンパ証明携帯プログラム配信方法。
【００１２】
本発明の耐タンパ証明携帯プログラム配信方法は、前記第４のステップにおいて、開発者側がゼロ知識証明プロトコルにより、一方向性準同型写像を用いたコミットメント関数を用いて、前記命題論理式の部分証明を、利用者側に送信することを特徴とする。
【００１３】
本発明の耐タンパ証明携帯プログラム配信システムは、開発者側が作成したプログラムｆを送信装置により利用者側に配信する際に、開発者側は前記プログラムｆが安全に実行可能であることを利用者側に示し、利用者側は受信装置により受信した前記プログラムｆを実行前に該プログラムｆが安全に実行可能であることを、開発者側の送信装置と対話的に通信しながら検証する耐タンパ証明携帯プログラム配信システムであり、開発者側が作成したプログラムｆが正しいことを示すために、プログラムｆと、プログラムｆを実行する際に、プログラム中の複数ポイントで成立すべき不変条件からなる不変条件列を生成するプログラム・不変条件列作成部と、前記不変条件列に対するダミーの不変条件を複数含む不変条件列候補集合を生成する不変条件列候補集合作成部と、不変条件列候補集合に基づいて、プログラムｆの安全性を証明する命題論理式を生成する安全性量化命題論理式生成部と、前記命題論理式を算術化する算術化部と、開発者側と利用者側とにおいて、ゼロ知識証明プロトコルに従った対話的通信を行い、前記算術化された量化命題論理式の計算結果が真であるか偽であるかを判定し、真である場合にプログラムｆを実行するゼロ知識証明プロトコル部とを有することを特徴とする。
【００１４】
本発明の耐タンパ証明携帯プログラム配信システムは、前ゼロ知識証明プロトコル部が、開発者側がゼロ知識証明プロトコルにより、一方向性準同型写像を用いたコミットメント関数を用いて、前記命題論理式の部分証明を利用者側に送信することを特徴とする。
【発明の効果】
【００１５】
以上説明したように、本発明によれば、証明本体ｐの秘匿だけでなく、既存方式においては公開せざるを得なかった不変条件列をも秘匿したまま、プログラムが正しく安全に動作することの数学的証明を効率的に検証する手段を与えており、これにより、悪性プログラムの高精度な実行前の検出及び駆除の処理を実現できる。
すなわち、本発明によれば、安全性証明の内容を秘匿し証明の盗用・悪用を防ぐ効率的なプロトコルを提供しており、これにより証明情報に基づくリバースエンジニアリングの防止が実現できる。
【００１６】
特に、本発明によれば、既存方式において、公開せざるを得なかった不変条件を秘匿し、不変条件及び証明本体の両方を利用者に対して隠すことにより、不変条件と証明本体とに基づくリバースエンジニアリングを防止し、配信プログラムの耐タンパ性を本質的に向上させている。
さらに、本発明によれば、不変条件と証明本体との所有者が、正規のプログラム開発者に限られるため、不変条件および証明本体の所有をプログラム著作権の保持とみなすことも可能になるという効果を併せ持つこととなる。
このように、本発明によれば、ネットワークを介したプログラム配信において、悪性プログラムによるホストヘの攻撃と、悪意のあるホストによるプログラムヘの攻撃との、双方を同時に防止することが可能なセキュリティ技術を提供することができる。
【発明を実施するための最良の形態】
【００１７】
＜本発明の概要＞
以下に、本発明によるプログラム配信方法の概要を説明する。
従来の定式化においては、プログラムの安全性は以下の（１）式に示すように定義されていた（例えば、非特許文献２参照）。
【００１８】
【数１】
【００１９】
すなわち、配信するプログラムｆと、以下の（２）式に示す不変条件の列（不変条件列）の組が安全性を満たしている（以下、集合Safeに含まれると表記する）とは、プログラムｆのすべての実行パスpathについて、以下に示す（３）式が成立することの数学的証明ｐが存在することとして定義される。
【００２０】
【数２】
【００２１】
【数３】
【００２２】
論理式である上記（３）式は、「前条件Preが成立する状況でプログラムｆをそのひとつの実行パスpathに沿って実行した場合、必ず後条件Postが成立しており、しかもプログラムｆの実行時には、利用者の要求する安全性が満たされる」ことを表わす論理式であり、プログラムｆと不変条件列を用いて計算される。ここで、上記前条件Preは「プログラムｆを実行する直前に成立すべき条件」を示し、上記後条件Postは「プログラムｆの実行した直後に成立すべき条件」を示している。
なお、プログラムｆの入出力仕様を規定する前条件Preおよび後条件Postも不変条件の一種であるが、本発明においては別の扱いとする。そして、上述した定義は以下に示す同値な定義式である（４）式へ容易に変形することができる。
【００２３】
【数４】
【００２４】
一般的に、（４）式における以下の（５）式の述語は、プログラムｆと不変条件列とについての多項式時間計算述語である。このため、この上記（４）式による定義は、集合Safeが計算量クラスco-NPに属していることを表しており、より正確に言うと、co-NP完全である（例えば、非特許文献２参照）。ここで、計算量クラスco-NPは、以下に示す（６）式に等しい。上述した説明の補足として、非決定性多項式時間限定アルゴリズムで計算可能な集合のクラスをNPと言い、上記co-NP完全とは、補集合がNPに属する集合のクラスco-NPの中において、最も計算するのが難しい集合のことを指している。
【００２５】
【数５】
【００２６】
【数６】
【００２７】
したがって、集合Safeに対するゼロ知識対話型証明プロトコル（例えば、非特許文献９，１０参照）を構成することが可能となり、不変条件列をアノテーションとして持つプログラムｆの安全性を、証明ｐそのものを提示することなく利用者に納得させることが可能となっている。例えば、以下に示すステップにより行われるゼロ知識証明携帯プログラム配信方法（例えば、非特許文献４参照）。すなわち、このゼロ知識証明携帯プログラム配信方法は、開発者側が作成したプログラムｆを送信装置により利用者側に配信する際に、開発者側は前記プログラムｆが安全に実行可能であることを利用者側に示し、利用者側は受信装置により受信した前記プログラムｆを実行前に該プログラムｆが安全に実行可能であることを、開発者側の送信装置と対話的に通信しながら検証する証明携帯プログラム配信方法である。
【００２８】
そして、上記証明携帯プログラム配信方法においては、開発者側が作成したプログラムｆが正しいことを示すために、プログラムｆと、プログラムｆを実行する直前に成立すべき条件である前条件Preと、プログラムｆの実行直後に成立すべき条件である後条件Postとから検証論理式｛Pre｝ｆ｛Post｝を検証論理式生成部により生成する第１のステップと、上記検証論理式が妥当であることを示すためにある論理体系Ｔ内で証明し、安全性証明ｐを、安全性証明作成部により作成する第２のステップと、開発者側が得られた安全性証明ｐをもとに利用者側との間でゼロ知識証明プロトコル部により対話的に通信を行い、送信したプログラムｆが、Safe＝｛ｆ｜Ｔにおける｛Pre｝ｆ｛Post｝の証明ｐが存在する｝によって定義される安全なプログラムの集合Safeに属することを利用者に確認させる第３のステップと、利用者側が、開発者側から送信されたプログラムｆが前記集合Safeに属することを確認した後に該プログラムｆを実行する第４のステップとにより、ゼロ知識証明の処理を行っている。
【００２９】
一方、本発明は、安全なプログラムの全体Safeを、以下の定義式である（７）式に示すように一般化することを最も主要な特徴としている。
【００３０】
【数７】
【００３１】
不変条件列を量化子∃によって束縛することにより、集合Safeの計算量はより複雑化して、（８）式に示すクラスに属することになる。
しかしながら、依然としてゼロ知識対話型証明プロトコルを構成可能な上限クラスPSPACE(決定性多項式領域限定アルゴリズムで計算可能な集合のクラスであり、クラスNP，co-NP，あるいは（８）式のクラスよりもはるかに大きいと考えられている)に抑えられているため、集合Safeに対するゼロ知識対話型証明プロトコルが非特許文献８，９，１０の方法（対話的・確率的手法に基づく効率的な証明検証技法）を応用することにより構成可能である。
【００３２】
【数８】
【００３３】
上述してきたように、本発明は、安全性の定式化における不変条件の扱い方に工夫を凝らすことにより、証明本体ｐの秘匿だけでなく、既存方式においては公開せざるを得なかった不変条件列をも秘匿したまま、プログラムｆの安全性を利用者に納得させることを可能にする、新しいプログラム配信方法を実現している。
【００３４】
＜耐タンパ証明携帯プログラム配信システムの構成＞
以下、本発明の一実施形態によるプログラム配信方法を実現する耐タンパ証明携帯プログラム配信システムを図面を参照して説明する。図１は同実施形態の構成例を示すブロック図である。
この図１の構成としては、説明のために、最も基本的な例題のひとつである、機械語プログラムのメモリ安全性・型安全性を対象としているが、プログラム言語や検証対象となる安全性は一般に多岐に渡るため、それらに応じて構成を適宜修正・拡張しても良い。
開発者（証明者）側装置１０は，プログラム・不変条件列・不変条件列侯補集合作成部１００，プログラム・不変条件列侯補集合送信部１０１，安全性量化命題論理式生成部１０２，算術化部１０３及びヒント（部分証明）作成・送信部１０４を有している。
【００３５】
一方、利用者（検証者）側装置２０は、プログラム入出力仕様作成・送信部２００，プログラム・不変条件列侯補集合受信部２０１，安全性量化命題論理式生成部２０２，算術化部２０３，ヒント（部分証明）受信・検証部２０４及び乱数生成・送信部２０５を有している。
上述した１１構成部各々のなかにおいて、プログラム入出力仕様作成・送信部２００と、プログラム・不変条件列・不変条件列候補集合作成部１００の２つは、他の９個の構成部がオンライン・リアルタイムで処理されるべきものであるのに対し、その前処理として実行を行う構成部である。
また、ヒント(部分証明)作成・送信部１０４,ヒント(部分証明)受信・検証部２０４及び乱数生成・送信部２０５各々は、ゼロ知識証明プロトコル部３０に設けられている。
【００３６】
この本発明におけるゼロ知識証明プロトコル部３０において、ヒント（部分証明）作成・送信部１０４は、ヒント（部分証明）受信・検証部２０４との間で対話型プロトコルを実行する。このとき、ヒント（部分証明）受信・検証部２０４は、乱数生成・送信部２０５により乱数を発生させ、該乱数によりヒント（部分証明）作成・送信部１０４から転送されるヒント情報を指定する。そして、ヒント（部分証明）受信・検証部２０４は、プログラムｆが安全に実行可能であることを確認した後、プログラムｆを実行する。
また、本発明の最も主要な構成は、ゼロ知識証明プロトコル部３０の前段における、プログラム・不変条件列・不変条件列侯補集合作成部１００，プログラム・不変条件列侯補集合送信部１０１，安全性量化命題論理式生成部１０２，算術化部１０３，プログラム入出力仕様作成・送信部２００，プログラム・不変条件列侯補集合受信部２０１，安全性量化命題論理式生成部２０２，算術化部２０３の各部である。
【００３７】
以下に、上述した本発明の主要な構成について説明する。
プログラム入出力仕様作成・送信部２００は、プログラムの利用者がプログラムの入出力仕様を規定するために作成及び入力した、プログラムを実行する直前および直後に成立すべき条件である前条件Ｐｒeおよび後条件Ｐｏｓｔを開発者（証明者）側装置に対して送信する。これにより、利用者は、自身の作成した上記前条件Ｐｒｅ及び後条件Ｐｏｓｔを公開しておく。例えば、利用者は、自然数の列の総和を求めるプログラムを利用したい場合、「入カレジスタは自然数のリスト型を持つ」という前条件Ｐｒｅと、「出力レジスタは自然数の型を持つ」という後条件Ｐｏｓｔを、プログラム入出力仕様作成・送信部２００により生成し、開発者（証明者）側装置１０へ送信し、開発者に対して事前に公開しておく。
【００３８】
さらに、プログラム入出力仕様作成・送信部２００は、プログラムを実行する際に、いかなる安全性を要求するかについての、利用者が入力する条件も、開発者（証明者）側装置１０に対して送信する。すなわち、利用者は、プログラムを実行する際に、いかなる安全性を要求するかについての、利用者が入力する条件も、開発者に対して事前に公開しているものとする。例えば、上記条件は、プログラム実行中に禁止されたメモリ領域へのアクセスが皆無であるという性質(メモリ安全性)に関する要求などである。
【００３９】
プログラム・不変条件列・不変条件列候補集合作成部１００は、開発者が作成した、利用者の規定した入出力仕様を満たす安全なプログラムｆが入力されると、これらの入出力仕様や安全性を満たすことを示す際、プログラム中における適切な複数ポイントで成立すべき、（２）式による条件式(不変条件)を抽出（発見）し、この発見した不変条件の列から不変条件列を作成する。
また、プログラム・不変条件列・不変条件列候補集合作成部１００は、後にこの不変条件列を秘匿したまま安全性を利用者に認識させるため、不変条件列を作成するのと同時に、ダミーの不変条件列を適宜複数個用意し、これらダミーの不変条件列を複数用いて不変条件列侯補集合を作成する。
すなわち、プログラム・不変条件列・不変条件列候補集合作成部１００は、以下に示す（９）式の論理式を満たすプログラムｆ及び不変条件列候補集合を、論理式成立の証拠とも見なせる（２）式の不変条件列とともに作成する。
【００４０】
【数９】
【００４１】
プログラム・不変条件列候補集合送信部１０１は、プログラム実行時の振る舞いに関する重要な情報を含んだ（２）式による不変条件列を秘匿したまま、プログラムｆと、作成した不変条件列候補集合とを利用者（検証者）側装置２０へ送信する。
プログラム・不変条件列候補集合受信部２０１は、プログラム・不変条件列候補集合送信部１０１から、プログラムｆと不変条件列候補集合とを受信する
【００４２】
安全性量化命題論理式生成部１０２及び２０２と、算術化部１０３及び２０３とは、開発者側（証明者）装置１０と利用者（検証者）側装置２０とで同じ機能の構成を用いる。 上記安全性量化命題論理式生成部１０２は、プログラムｆが安全であることを表す上記（９）式に示す論理式と同値な、以下の（１０）式に示す量化命題論理式（量化子を用いた命題論理式）を、不変条件列候補集合に基づき生成する。
【００４３】
【数１０】
【００４４】
ここで、上記（１０）式のような量化命題論理式は、以下の理由により容易に生成可能である。すなわち、（２）式に示す不変条件列を量化子∃（特称量化子）によって束縛した場合のメモリ安全・型安全な機械語プログラムの全体(つまり、（９）式に示す論理式を満たすプログラムｆの全体)は（８）式に示す計算量クラスに属する。
一方、真なる量化命題論理式の全体は、より計算量の大きいとされるPSPACE完全である。したがって、プログラムｆが安全か否かといった安全性検証の問題は、量化命題論理式の真偽判定問題に還元可能であり、この還元アルゴリズムを用いることにより、上記（１０）式に示す量化命題論理式は生成可能である．
【００４５】
算術化部１０３（２０３）は、上記（１０）式に示す量化命題論理式の算術化を行う。ここで、量化命題論理式を算術化することにより、この量化命題論理式の真偽判定を数式の値の零判定に置き換えることができる。実際に、命題変数Ｘを自然数変数Ｘに算術化し、同様に、論理結合子各々を算術化、すなわち論理結合子∨を「＋」に、論理結合子∧を×に、論理結合子¬Ｘを１−Ｘに、算術化し、また、量化子∃を和Σに、そして量化子∀（全称量化子）を積Πに変換することで算術化は完了する。これにより、上記（１０）式による量化命題論理式が真であることは、以下の（１１）式の計算結果が零でないことと同値となる。
【００４６】
【数１１】
【００４７】
ゼロ知識証明プロトコル部３０において、ヒント(部分証明)作成・送信部１０４，ヒント(部分証明)受信・検証部２０４，乱数生成・送信部２０５各々が、すでに述べたように開発者及び利用者間における対話的通信を行い、上記（１１）式が零とならないことを利用して、利用者に対してプログラムｆの安全性を納得させる。
一方、利用者もゼロ知識証明プロトコル部３０において、開発者と対話的通信を行い，上記（１１）式が確かに零でないこと、すなわち受信したプログラムｆが安全であることを確認した後に、このプログラムｆに対して処理を実行させる。
【００４８】
上記（８）式により示される計算クラスにおける計算量は決して小さくはないが、ゼロ知識証明プロトコル部３０は、非特許文献８及び９の対話型証明プロトコルの理論を応用することにより、確率的ではあるが極めて高い精度により、効率的に（１１）式が零でないことを証明・検証することができる。
また、プログラムの耐タンパ性は、（２）式による不変条件列を検出（発見）・作成する多項式時間アルゴリズムが存在しないこととして、数学的に表現される。
すなわち、安全なプログラムｆの全体が（８）式により示される計算クラスにおいて完全であることが示されれば、以下の（１２）式が成り立たない限り、上記多項式時間アルゴリズムは存在しない。
【００４９】
【数１２】
【００５０】
＜利用者側における前条件及び後条件の作成＞
次に、機械語プログラムのメモリ安全性及び型安全性を例にとり、本発明の実施方法について説明する。ここでは、Alphaアセンブリ言語で記述された機械語プログラム（プログラムｆ）を、利用者（検証者）側装置２０（Standard ML言語の型つき中間言語コンパイラ実行時システム）が受信し、この機械語プログラムをメモリ安全及び型安全に実行する一連の流れ（非特許文献１，２，４で展開されている）を用い、耐タンパ証明携帯プログラム配信システムの動作例を説明する。はじめに、利用者がプログラム入出力仕様作成・送信部２００にて行う、前条件Ｐｒｅ，後条件Ｐｏｓｔの作成と、開発者側に対する公開について説明する。
【００５１】
まず、安全性要求，前条件Ｐｒｅ及び後条件Ｐｏｓｔについて、以下に簡単に説明する。利用者（検証者）側装置２０は、代表的な関数型言語であるStandard ML言語の型つき中間言語コンパイラ実行時システムを搭載している（例えば、アプリケーションプログラムがインストールされている）と仮定する。この利用者（検証者）側装置２０は、中間言語コンパイラ実行時システムにおいて、Alphaアセンブリ言語で記述された機械語プログラムを、開発者側（証明者）装置１０から受信し、メモリ安全かつ型安全に実行しようとしていると仮定する．
この利用者（検証者）側装置２０は、その安全性要求やプログラムの前条件Ｐｒｅ及び後条件Ｐｏｓｔといった仕様を、型（例えば、データの種類または内容：整数型，実数型，文字型、アドレス型など）の概念を用いて規定する。例えば、式ｅが型τを持つことをｅ：τと記述し、本実施形態において利用される式と型とは以下に示す（１３）式のように定義される。
【００５２】
【数１３】
【００５３】
上記（１３）式において、ｎは３２ビットで表わされる自然数であり、各ｒ1はAlphaレジスタ，sel（e）はメモリ番地ｅの内容を指している。ここで、型intの値は３２ビットで表される自然数である。型τ1＊τ2の値は、型τ1と型τ2の値が格納された隣接するメモリ番地へのポインタである。また、型τ1＋τ2の値は隣接するメモリ番地へのポインタであり、最初の番地にはタグ（０または１）が格納されており、ダグが「０」ならば型τ1の値が、一方、ダグが「１」ならば型τ2の値が続きの番地に格納される。さらに、型addrの値は、安全に読み出し可能なメモリ番地を表わしている。
なお、加法および減法は厳密には２３２を法とするものであるが、説明を簡単とするため、ここでは法演算を省略して記述する。
【００５４】
そして、利用者は上述した型の概念を用い、利用者（検証者）側装置２０において、安全性要求を事前に規定する。本実施形態における安全性要求は、図２に示す公理からなる一階述語論理体系Ｔとして規定する。
また、利用者は、すでに述べたように、プログラムが実行される直前および直後に成立すべき条件を、それぞれ前条件Ｐｒｅと後条件Ｐｏｓｔとして規定し、事前に開発者側に対して公関しておかなければならない。
本実施形態における前条件Ｐｒｅおよび後条件Ｐｏｓｔは、上述した型を用いて、図３に示すように規定されているとする。
【００５５】
＜機械語プログラムの作成＞
本実施形態におけるプログラム・不変条件列・不変条件列候補集合作成部１００にて、開発者に作成されるプログラムの例として、Alphaアセンブリ言語で記述された簡単なプログラム（プログラムｆ）を図４に示す。このプログラムは、コンピュータのレジスタｒ1, ｒ2，ｒ3の値に応じて分岐した後、単純なループに入る処理を示している。
ここで、上記プログラムは、図３に示す前条件Ｐｒｅおよび後条件Ｐｏｓｔを入出力仕様として満たし、メモリ安全かつ型安全に実行されることを意図して作成されたものである。これらの前条件Ｐｒｅおよび後条件Ｐｏｓｔは、例えば補助的な命令であるINV命令（Invariant：不変条件）を用い、図４に示すプログラム中に表明されている。なお、不変条件列もINV命令を用いて表記（表明）されるが、この表記については後に詳述する。
ここで、実は、図４のプログラム例において、プログラムがメモリ安全かつ型安全であることと、以下に示す（１４）式に定義する量化命題論理式が偽であることが同値となるように作成されている。
【００５６】
【数１４】
【００５７】
そして、プログラム・不変条件列・不変条件列候補集合作成部１００は、命題変数Ｘiの真偽を、番地４（ｒi） (ダグが格納された番地０（ｒi）の続きの番地)が型intであるか、あるいは型intの組へのポインタであるかということにエンコードする。
さらに、プログラム・不変条件列・不変条件列候補集合作成部１００は、レジスタｒ（3＋i）に、上記番地に記憶された内容を読み込むことにより、真偽を、ｒ（3＋i）：intあるいはsel(r3+i):intの成立へと変換する。
【００５８】
＜不変条件およびプログラム安全性＞
すでに述べたように、プログラムｆ（機械語プログラム）が安全なプログラムの全体Safeに属すると言うことは、（９）式に示す論理式が成立することであると定義された。ここで、各pathによってインデックス付けされた部分式である（３）式の全体を特に検証論理式と呼ぶこととする。この検証論理式は、プログラム・不変条件列・不変条件列候補集合作成部１００内部に設けられたFloyd流の検証論理式生成器によって、プログラムｆ，前条件Ｐｒｅ，後条件Ｐｏｓｔ及び不変条件列から自動的に生成される。
【００５９】
上記検証論理式生成器における検証論理式の生成の規約を図５に示し、この図の規約を用いて図４のプログラムに対する検証論理式が実際に生成されていく様子を図６及び図７に示す。
この検証論理式の生成において、必須の情報として不変条件列がある。図４のプログラム中の前方へのジャンプ命令の行き先が必ずINV命令であるとの規約を置くことにより、検証論理式生成器は１パスで容易に検証論理式を生成することができる。
本実施形態における図４のプログラムにおいても、１０行目のラベルＬcが貼られた（マーキングされた）ポイントで常に成立すべき不変条件Ｉを明らかにしておく必要がある。本実施形態における不変条件Ｉを図８に示す。
図８に示す不変条件Ｉを用いることにより、最終的に得られる検証論理式は、図９に示すように、ＶＣ0⇒ＶＣ1を表す９個の論理式と、ＶＣ10⇒ＶＣ11を表わす２個の論理式をあわせた計１１個の論理式となる。ここで、「⇒」は「含意」を示す論理結合子であり、「Ｐ⇒Ｑ」が「ＰならばＱ」となる。
【００６０】
上述した図９に示す各検証論理式は、その妥当性の証拠を得るため、一階述語論理体系Ｔにおいて証明される。そして、検証論理式が全て証明された場合、すなわち、各pathについて（３）式が一階述語論理体系Ｔ内で証明された場合、Standard ML言語の型つき中間言語コンパイラ実行時システムにおいて、前条件Ｐｒｅが成立する状況においてプログラムｆを実行し、計算が終了すると必ず後条件Ｐｏｓｔが成立し、しかもプログラムｆの実行中に用いられる全ての値に対して適切な型がつくため、このプログラムｆの実行時のメモリアクセスが安全であることが保証される。
【００６１】
例えば、図４のプログラム例も、検証論理式が全て証明可能であり、メモリ安全かつ型安全であることが保証される。
また、図９の検証論理式が示唆するように、プログラム中に条件分岐命令がｎ回続いた場合、このｎの指数オーダの実行パスが存在することになる。ここで、個々の検証論理式の証明は、短く多項式時間で検証することが可能であるが、全ての検証論理式を証明するとなると証明は指数オーダのサイズとなる。
実際、図４のプログラムの安全性、すなわち検証論理式の証明可能性は、ＶＣ0⇒ＶＣ1に対応する部分が上記（１４）式が偽であることと同値である。
また、ＶＣ10⇒ＶＣ11に対応する部分が以下に示す（１５）式が真であることと同値である。
【００６２】
【数１５】
【００６３】
（１５）式が真であることは容易に確認できるが、（１４）式が偽であることの証明は本質的に難しい。
【００６４】
＜不変条件の秘匿＞
開発者（証明者）側装置１０において発見・計算された（２）式の不変条件列をそのまま利用者（検証者）側装置２０に送信することにより、プログラムｆの安全性を開発者及び利用者の双方において、安全性量化命題論理式生成部１０２（及び２０２）により容易に定義することができる。
しかしながら、本発明の技術思想においては、不変条件列に基づくリバースエンジニアリングを防止し、配信するプログラムの耐タンパ性を高めることを目的としているため、悪意を持っている可能性もある利用者に上記不変条件列を明示的に送信することは避ける必要がある。
【００６５】
そこで、開発者（証明者）側装置１０は、本来の（２）式に示す不変条件列にダミーの条件を適宜加えた不変条件列候補集合を、利用者（検証者）側装置２０に送信する。この不変条件列候補集合が十分大きい場合、利用者（検証者）側装置２０が、その不変条件列候補集合中から正解の不変条件を選択することが困難となる。
図４に示す本実施形態のプログラム例におけるダミーの不変条件を、図１０に示す不変条件Ｉ＊とする。すなわち、不変条件候補集合を｛Ｉ，Ｉ＊｝とする。ただし、ダミーであるためには、不変条件にはなり得ないこと、例えば以下の（１６）式に示す論理式を満たすことが望ましい。本実施形態におけるダミーの不変条件Ｉ＊はこれを満たしている。
【００６６】
【数１６】
【００６７】
また、不変条件Ｉに基づくリバースエンジニアリングを防止するためには、不変条件列候補集合は大きいほど都合がよい。
しかしながら、一般にプログラム中の各ポイントにおいて追加されるダミーの不変条件は、１つでよい。すなわち、本実施形態においては、プログラム中に不変条件が表明されるポイントは１つであるが、一般にｋ個の不変条件Ｉが表明されている場合、不変条件列候補集合のサイズは組合せにより２ｋとなるからである。
ダミーの不変条件Ｉ＊を用いたときの検証論理式の証明可能性は、ＶＣ0⇒ＶＣ1に対応する部分が以下に示す（１７）式が偽であることと同値である。
【００６８】
【数１７】
【００６９】
また、ＶＣ10⇒ＶＣ11に対応する部分が以下に示す（１８）式が真であることと同値である。
【００７０】
【数１８】
【００７１】
そして、プログラム・不変条件列候補集合送信部１０１は、機械語プログラム，不変条件列及び不変条件列候補集合を、安全性量化命題論理式生成部１０２に出力するとともに、プログラムｆ及び不変条件列候補集合を、プログラム・不変条件候補集合受信部２０１に対して送信する。
【００７２】
＜安全性の量化命題論理式への翻訳＞
上述したように、不変条件候補集合が｛Ｉ，Ｉ＊｝である場合、安全性量化命題論理式生成部１０２（及び２０２）は、プログラムｆが安全であることを表す（９）式に示される論理式を、以下に示す（１９）式の構成に変換する（書き換える）。本実施形態においては、この書き換えにより、安全性を（８）式の計算クラスから、（１２）式に示すco-NPに還元している。
【００７３】
【数１９】
【００７４】
そして、（１９）式の論理式は、以下に示す（２０）式が真であること、すなわち、以下に示す（２１）式が偽であることと同値となる。
【００７５】
【数２０】
【００７６】
【数２１】
【００７７】
＜量化命題論理式の算術化＞
次に、算術化部１０３（及び２０３）は、上記（２１）式の算術化を行うことにより、量化命題論理式の真偽判定を数式の値の零判定に置き換える。
実際の処理としては、命題変数Ｘを自然数変数Ｘに、∨を＋に、∧を×に、¬Ｘを１−Ｘに、そして量化子∃を和Σに変換することにより算術化は完了する。ここで、本実施形態における（２１）式に示す量化命題論理式が偽であることは、以下の（２２）式の計算値が零であることと同値である。
【００７８】
【数２２】
【００７９】
＜安全性のゼロ知識証明＞
次に、ゼロ知識証明プロトコル部３０における、上記（２２）式が零であることを証明するゼロ知識証明プロトコルの実行例を、図１１，１２，１３，１４，１５，１６，１７及び図１８を用いて説明する。
開発者（証明者）側装置１０と利用者（検証者）側装置２０とにおける開発者及び利用者の対話処理は実質的に６ラウンドからなっている。ここで、各ラウンドがひとつのΣ記号に対応している。
【００８０】
上記各ラウンド毎に、ひとつの数式が提示され,利用者はその値の正当性を開発者との対話を通じて検証することになる。なお、実際のプロトコルにおいては、セキュリティパラメータ(本実施形態では一例として数式の長さ）ｌに対応して決定される長さΟ（ｌ）の適当な素数ｑを法とした計算が行われるが、ここでは省略する。
開発者（証明者）側装置１０におけるヒント（部分証明）作成・送信部１０４は、各ラウンドで提示された数式からΣ記号をひとつ除去し、それを展開して得られた１変数多項式の係数をヒント情報として、利用者（検証者）側装置２０のヒント（部分証明）受信・検証部２０４へ送信する。例えば、ヒント（部分証明）作成・送信部１０４は、図１１の第１ラウンドの「情報１」を、ヒント（部分証明）受信・検証部２０４へ送信する。
【００８１】
次に、利用者側のヒント（部分証明）受信・検証部２０４は、各ラウンドごとに自動的に決まる検証タスクを実行する。例えば、ヒント（部分証明）受信・検証部２０４は、ヒント（部分証明）作成・送信部１０４から「情報１」を受信することにより、「タスク１」による検証処理を実行する。
具体的な例として、ヒント（部分証明）受信・検証部２０４は、受け取った多項式の０と１とにおけるそれぞれの値の和を計算し、それの計算結果が期待される値と等しいか否かの検証を行う。
そして、ヒント（部分証明）受信・検証部２０４は、この検証をパスすると（計算結果が期待される値と等しいことを検出すると）、ヒント情報の妥当性を検証する新しい、すなわち次のラウンド（例えば、第１ラウンドの次は第２ラウンド）に移行する。
【００８２】
次に、Σ記号のひとつ少ない新しい数式が提示され、開発者（証明者）側装置１０によるヒントの送付と、利用者（検証者）側装置２０による多項式の０と１とにおけるそれぞれの値の和を計算し、計算結果の値の検証が繰り返される。このゼロ知識証明プロトコルのプロセスは、Σ記号を含まない数式の自明な検証に帰着されるまで繰り返される。
ここで、不正な開発者が妥当でないヒントを送付した場合、この攻撃に対処するため、ヒント（部分証明）受信・検証部２０４は、開発者が各ラウンドにてΣ記号の一つ少ない数式を提示する際に、変数に代入する定数を、乱数生成・送信部２０５により生成させ、ヒント（部分証明）作成・送信部１０４へ送信する。
【００８３】
ただし、開発者（証明者）側装置１０がヒントとして、多項式の係数そのものを送付してしまうと、不変条件と証明本体とに開する情報が利用者に対して漏れてしまう。
そこで、開発者（証明者）側装置１０は、１変数多項式の係数そのものではなく、係数のコミットメントを送付することにより、プロトコルをゼロ知識化する。
すなわち、本実施形態においては、プログラム安全性の証明・検証プロトコルをゼロ知識化する際に、一方向性準同型写像を用いたコミットメント(秘密証拠供託)関数を用いる。
情報の内容自体を秘密に保ったまま、内容の事後変更を不可能とする十分な証拠を予め相手に渡しておくために、コミットメント（秘密証拠供託）関数commitを本プロトコルにおいて利用する。セキュリティパラメータｌと長さＯ（ｌ）の素数ｑに対し、証明者は秘密にしたい情報ａ∈ {０，１，…，ｑ−１}と乱数r∈｛０，１｝ｌをもとに証拠commit(a、 r)∈｛０，１｝ｌを計算して、利用者（検証者）側装置２０へ送信する（コミットメント・フェーズ）。
【００８４】
そして、証明者によるａとｒの開示を受けた検証者は、これらの情報に基づき先の証拠が確かにcommit(a、r)であることを計算し、情報ａが事後変更されていないことを確認する（開示フェーズ）。
このような秘密証拠供託の実現は、関数commitに課せられた次の３つの性質により保証される。
「秘匿性」：commit (a，r)の値から秘密情報ａに間する知識を得ることは計算論的に困難である性質、すなわち、異なるふたつの秘密情報に対するコミットメントの確率分布は多項式時間識別不可能である性質である。
「束縛性」：commit（a、r）の値から秘密情報ａが一意に決まる性質である。すなわち、秘密情報ａに対する証拠commit（a、r）を受信した後に、ａ及びｒの開示を受け、先に受信した証拠が計算値commit（a、r）に一致するか否かをもって、秘密がａであったことを検証する場合、秘密情報の事後変更は不可能である性質である。
「準同型性」：与えられたふたつのコミットメントＡ ＝commit（a、r）およびＢ ＝commit（ｂ、r）から、commit（ａ＋ｂ mod ｑ，ｔ）およびcommit（ａ−ｂ mod ｑ，ｕ）が多項式時間で計算可能である。各コミットメントは乗法群の要素であるため、これらをそれぞれＡＢおよびＡＢ−１と記す。この性質から直ちに、コミットメントＡ＝commit（a、r）が与えられれば、任意の定数ｃに対して、commit(ca mod ｑ，ｓ)が多項式時間計算可能となる。これをＡＣと記す。
【００８５】
図１８においては、簡単のため適当なｒに対するcommit（a，r）をＣ(a)と略記していいる。これにあわせ、コミットメント間の等号Ｃ＝Ｃ’を、ＣとＣ’があるａに対し集合{commit(a，r)｜r}の要素であることと定義する。Ｃ（ａ）は同値関係＝による各同値類{commit(a，r)｜r}の代表元とみなせる。
上述した３つの性質(秘匿性、束縛性、準同型性)をもつコミットメント関数を実際に構成することができる（例えば、非特許文献１０参照）。そして、そのコミットメント関数を用いることにより、利用者（検証者）側装置２０において、利用者は係数のコミットメントのみから、係数自体を知ることなく、目的とする式のコミットメントを計算することが可能となる。
【００８６】
なお、図１における各部の機能を実現するためのプログラムをコンピュータ読み取り可能な記録媒体に記録して、この記録媒体に記録されたプログラムをコンピュータシステムに読み込ませ、実行することにより開発者（検証者）側装置１０及び利用者（検証者）側装置２０における各処理を行ってもよい。なお、ここでいう「コンピュータシステム」とは、ＯＳや周辺機器等のハードウェアを含むものとする。また、「コンピュータシステム」は、ホームページ提供環境（あるいは表示環境）を備えたＷＷＷシステムも含むものとする。また、「コンピュータ読み取り可能な記録媒体」とは、フレキシブルディスク、光磁気ディスク、ＲＯＭ、ＣＤ−ＲＯＭ等の可搬媒体、コンピュータシステムに内蔵されるハードディスク等の記憶装置のことをいう。さらに「コンピュータ読み取り可能な記録媒体」とは、インターネット等のネットワークや電話回線等の通信回線を介してプログラムが送信された場合のサーバやクライアントとなるコンピュータシステム内部の揮発性メモリ（ＲＡＭ）のように、一定時間プログラムを保持しているものも含むものとする。
【００８７】
また、上記プログラムは、このプログラムを記憶装置等に格納したコンピュータシステムから、伝送媒体を介して、あるいは、伝送媒体中の伝送波により他のコンピュータシステムに伝送されてもよい。ここで、プログラムを伝送する「伝送媒体」は、インターネット等のネットワーク（通信網）や電話回線等の通信回線（通信線）のように情報を伝送する機能を有する媒体のことをいう。また、上記プログラムは、前述した機能の一部を実現するためのものであっても良い。さらに、前述した機能をコンピュータシステムにすでに記録されているプログラムとの組み合わせで実現できるもの、いわゆる差分ファイル（差分プログラム）であっても良い。
【図面の簡単な説明】
【００８８】
【図１】本発明の一実施形態による耐タンパ証明携帯プログラム配信システムの構成例を示すブロック図である。
【図２】一階述語論理体系Ｔの内容を示す図である。
【図３】規定された前条件Ｐｒｅおよび後条件Ｐｏｓｔを示す図である。
【図４】検証対象となるプログラムの一例を示す図である。
【図５】検証論理式生成器における検証論理式の生成の規約を示す図である。
【図６】図５に示した検証論理式生成器の規約を用いて図４に示したプログラムに対する検証論理式が生成される様子を示す説明図。
【図７】図５に示した検証論理式生成器の規約を用いて図４に示したプログラムに対する検証論理式が生成される様子を示す説明図。
【図８】本実施形態における不変条件Ｉを示す図である。
【図９】不変条件Ｉを用いることにより、最終的に得られる検証論理式を示す図である。
【図１０】図４に示すプログラムに対するダミーの不変条件Ｉ＊を示す図である。
【図１１】ゼロ知識証明プロトコル部３０におけるゼロ知識証明プロトコルの実行例を示す図である。
【図１２】ゼロ知識証明プロトコル部３０におけるゼロ知識証明プロトコルの実行例を示す図である。
【図１３】ゼロ知識証明プロトコル部３０におけるゼロ知識証明プロトコルの実行例を示す図である。
【図１４】ゼロ知識証明プロトコル部３０におけるゼロ知識証明プロトコルの実行例を示す図である。
【図１５】ゼロ知識証明プロトコル部３０におけるゼロ知識証明プロトコルの実行例を示す図である。
【図１６】ゼロ知識証明プロトコル部３０におけるゼロ知識証明プロトコルの実行例を示す図である。
【図１７】ゼロ知識証明プロトコル部３０におけるゼロ知識証明プロトコルの実行例を示す図である。
【図１８】ゼロ知識証明プロトコル部３０におけるゼロ知識証明プロトコルの実行例を示す図である。
【図１９】従来技術と本発明との特性を比較したテーブルを示す図である。
【符号の説明】
【００８９】
１０…開発者（証明者）側装置
２０…利用者（検証者）側装置
１００…プログラム・不変条件列・不変条件列候補集合作成部
２００…プログラム入出力仕様作成・送信部
１０１…プログラム・不変条件列・不変条件列候補集合送信部
２０１…プログラム・不変条件列・不変条件列候補集合受信部
１０２，２０２…安全性量化命題論理式生成部
１０３，２０３…算術化部
１０４…ヒント（部分証明）作成・送信部
２０４…ヒント（部分証明）受信・検証部
２０５…乱数生成・送信部
【特許請求の範囲】
【請求項１】
開発者側が作成したプログラムｆを送信装置により利用者側に配信する際に、開発者側は前記プログラムｆが安全に実行可能であることを利用者側に示し、利用者側は受信装置により受信した前記プログラムｆを実行前に該プログラムｆが安全に実行可能であることを、開発者側の送信装置と対話的に通信しながら検証する耐タンパ証明携帯プログラム配信方法であって、
開発者側が作成したプログラムｆが正しいことを示すために、プログラムｆと、プログラムｆを実行する際に、プログラム中の複数ポイントで成立すべき不変条件からなる不変条件列を生成する第１のステップと、
前記不変条件列に対するダミーの不変条件を複数含む不変条件列候補集合を生成する第２のステップと、
不変条件列候補集合に基づいて、プログラムｆの安全性を証明する命題論理式を生成する第３のステップと、
前記命題論理式を算術化する第４のステップと、
開発者側と利用者側とにおいて、ゼロ知識証明プロトコルに従った対話的通信を行い、前記算術化された量化命題論理式の計算結果が真であるか偽であるかを判定し、真である場合にプログラムｆを実行する第５のステップと
を有することを特徴とする耐タンパ証明携帯プログラム配信方法。
【請求項２】
前記第４のステップにおいて、開発者側がゼロ知識証明プロトコルにより、一方向性準同型写像を用いたコミットメント関数を用いて、前記命題論理式の部分証明を、利用者側に送信することを特徴とする請求項１に記載の耐タンパ証明携帯プログラム配信方法。
【請求項３】
開発者側が作成したプログラムｆを送信装置により利用者側に配信する際に、開発者側は前記プログラムｆが安全に実行可能であることを利用者側に示し、利用者側は受信装置により受信した前記プログラムｆを実行前に該プログラムｆが安全に実行可能であることを、開発者側の送信装置と対話的に通信しながら検証する耐タンパ証明携帯プログラム配信システムであって、
開発者側が作成したプログラムｆが正しいことを示すために、プログラムｆと、プログラムｆを実行する際に、プログラム中の複数ポイントで成立すべき不変条件からなる不変条件列を生成するプログラム・不変条件列作成部と、
前記不変条件列に対するダミーの不変条件を複数含む不変条件列候補集合を生成する不変条件列候補集合作成部と、
不変条件列候補集合に基づいて、プログラムｆの安全性を証明する命題論理式を生成する安全性量化命題論理式生成部と、
前記命題論理式を算術化する算術化部と、
開発者側と利用者側とにおいて、ゼロ知識証明プロトコルに従った対話的通信を行い、前記算術化された量化命題論理式の計算結果が真であるか偽であるかを判定し、真である場合にプログラムｆを実行するゼロ知識証明プロトコル部と
を有することを特徴とする耐タンパ証明携帯プログラム配信システム。
【請求項４】
前ゼロ知識証明プロトコル部が、開発者側がゼロ知識証明プロトコルにより、一方向性準同型写像を用いたコミットメント関数を用いて、前記命題論理式の部分証明を利用者側に送信することを特徴とする請求項３に記載の耐タンパ証明携帯プログラム配信システム。
【請求項１】
開発者側が作成したプログラムｆを送信装置により利用者側に配信する際に、開発者側は前記プログラムｆが安全に実行可能であることを利用者側に示し、利用者側は受信装置により受信した前記プログラムｆを実行前に該プログラムｆが安全に実行可能であることを、開発者側の送信装置と対話的に通信しながら検証する耐タンパ証明携帯プログラム配信方法であって、
開発者側が作成したプログラムｆが正しいことを示すために、プログラムｆと、プログラムｆを実行する際に、プログラム中の複数ポイントで成立すべき不変条件からなる不変条件列を生成する第１のステップと、
前記不変条件列に対するダミーの不変条件を複数含む不変条件列候補集合を生成する第２のステップと、
不変条件列候補集合に基づいて、プログラムｆの安全性を証明する命題論理式を生成する第３のステップと、
前記命題論理式を算術化する第４のステップと、
開発者側と利用者側とにおいて、ゼロ知識証明プロトコルに従った対話的通信を行い、前記算術化された量化命題論理式の計算結果が真であるか偽であるかを判定し、真である場合にプログラムｆを実行する第５のステップと
を有することを特徴とする耐タンパ証明携帯プログラム配信方法。
【請求項２】
前記第４のステップにおいて、開発者側がゼロ知識証明プロトコルにより、一方向性準同型写像を用いたコミットメント関数を用いて、前記命題論理式の部分証明を、利用者側に送信することを特徴とする請求項１に記載の耐タンパ証明携帯プログラム配信方法。
【請求項３】
開発者側が作成したプログラムｆを送信装置により利用者側に配信する際に、開発者側は前記プログラムｆが安全に実行可能であることを利用者側に示し、利用者側は受信装置により受信した前記プログラムｆを実行前に該プログラムｆが安全に実行可能であることを、開発者側の送信装置と対話的に通信しながら検証する耐タンパ証明携帯プログラム配信システムであって、
開発者側が作成したプログラムｆが正しいことを示すために、プログラムｆと、プログラムｆを実行する際に、プログラム中の複数ポイントで成立すべき不変条件からなる不変条件列を生成するプログラム・不変条件列作成部と、
前記不変条件列に対するダミーの不変条件を複数含む不変条件列候補集合を生成する不変条件列候補集合作成部と、
不変条件列候補集合に基づいて、プログラムｆの安全性を証明する命題論理式を生成する安全性量化命題論理式生成部と、
前記命題論理式を算術化する算術化部と、
開発者側と利用者側とにおいて、ゼロ知識証明プロトコルに従った対話的通信を行い、前記算術化された量化命題論理式の計算結果が真であるか偽であるかを判定し、真である場合にプログラムｆを実行するゼロ知識証明プロトコル部と
を有することを特徴とする耐タンパ証明携帯プログラム配信システム。
【請求項４】
前ゼロ知識証明プロトコル部が、開発者側がゼロ知識証明プロトコルにより、一方向性準同型写像を用いたコミットメント関数を用いて、前記命題論理式の部分証明を利用者側に送信することを特徴とする請求項３に記載の耐タンパ証明携帯プログラム配信システム。
【図１】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７】
【図８】
【図９】
【図１０】
【図１１】
【図１２】
【図１３】
【図１４】
【図１５】
【図１６】
【図１７】
【図１８】
【図１９】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７】
【図８】
【図９】
【図１０】
【図１１】
【図１２】
【図１３】
【図１４】
【図１５】
【図１６】
【図１７】
【図１８】
【図１９】
【公開番号】特開２００７−１５７０２１（Ｐ２００７−１５７０２１Ａ）
【公開日】平成１９年６月２１日（２００７．６．２１）
【国際特許分類】
【出願番号】特願２００５−３５４４３７（Ｐ２００５−３５４４３７）
【出願日】平成１７年１２月８日（２００５．１２．８）
【出願人】（０００００４２２６）日本電信電話株式会社 (13,992)
【Ｆターム（参考）】
【公開日】平成１９年６月２１日（２００７．６．２１）
【国際特許分類】
【出願日】平成１７年１２月８日（２００５．１２．８）
【出願人】（０００００４２２６）日本電信電話株式会社 (13,992)
【Ｆターム（参考）】
[ Back to top ]