論文の概要: Zero-Knowledge Model Checking

• arxiv url: http://arxiv.org/abs/2605.00487v1
• Date: Fri, 01 May 2026 07:53:51 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-04 17:43:28.897976
• Title: Zero-Knowledge Model Checking
• Title（参考訳）: ゼロ知識モデル検査
• Authors: Pascal Berrang, Mirco Giacobbe, Jacob Swales, Xiao Yang,
• Abstract要約: 我々は,ソフトウェアシステムが機能的正当性の時間的仕様を満たすことを,システム自体を明らかにすることなく正式に検証する技術を導入する。 提案手法は,システムに対する正当性の形式的証明を得るためのモデルチェックに対する帰納的アプローチと,その正当性の仕様に準拠していることを外部の検証者(秘密保持者)に納得させるゼロ知識証明とを組み合わせる。
• 参考スコア（独自算出の注目度）: 8.04509170587377
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We introduce a technology to formally verify that a software system satisfies a temporal specification of functional correctness, without revealing the system itself. Our method combines a deductive approach to model checking to obtain a formal certificate of correctness for the system, with zero-knowledge proofs to convince an external verifier that the system -- kept secret -- complies with its specification of correctness -- made public. We consider proof certificates represented as ranking functions, and introduce both an explicit-state and a symbolic scheme for model checking in zero knowledge. Our explicit-state scheme assumes systems represented as transition graphs. We use polynomial commitments to convince the verifier that the public proof certificates correspond to the secret transition relation. Our symbolic scheme assumes systems specified as linear guarded commands and uses piecewise-linear ranking functions. We apply Farkas' lemma to obtain a witness for the validity of the ranking function with public and secret components, and employ sigma protocols for matrix multiplication and range proofs to convince the verifier of the witness's existence. We built a prototype to demonstrate the practical efficacy of our two schemes on linear temporal logic verification examples. Our technology enables formal verification in domains where both the safety and the confidentiality of the system under analysis are critical.
• Abstract（参考訳）: 我々は,ソフトウェアシステムが機能的正当性の時間的仕様を満たすことを,システム自体を明らかにすることなく正式に検証する技術を導入する。 提案手法は,システムに対する正当性の形式的証明を得るためのモデルチェックに対する帰納的アプローチと,その正当性の仕様に準拠していることを外部の検証者(秘密保持者)に納得させるゼロ知識証明とを組み合わせる。 ランキング関数として表される証明証明書を考察し,ゼロ知識におけるモデルチェックのための明示的状態と記号的スキームの両方を導入する。 我々の明示状態スキームは、遷移グラフとして表されるシステムを想定している。 我々は,公証書が秘密遷移関係に対応することを検証者に納得させるために,多項式コミットメントを用いる。 我々のシンボリックスキームは、線形ガードコマンドとして指定されたシステムを想定し、一方向線形ランキング関数を使用する。 我々はFarkasの補題を公開および秘密成分によるランキング関数の有効性の証人獲得に応用し、行列乗算と範囲証明のシグマプロトコルを用いて証人の存在を証明した。 我々は,線形時間論理検証の例において,2つのスキームの実用的有効性を示すプロトタイプを構築した。 我々の技術は、分析対象システムの安全性と機密性の両方が重要である領域での正式な検証を可能にする。

関連論文リスト

• Formal Evidence Generation for Assurance Cases for Robotic Software Models [1.8145248907978841]
  保証ケースは、証拠によって支持される構造化された議論を提供する。 この証拠の生成と維持は、労働集約的で、エラーを起こし、システムが進化するにつれて一貫性を維持するのが困難である。 本稿では,保証ワークフローに形式検証を組み込むことにより,AC証拠を体系的に生成するモデルに基づく手法を提案する。
  論文  参考訳（メタデータ） (2026-02-03T14:01:30Z)
• Neural Model Checking [10.376573742987917]
  時間論理をモデル化するための機械学習手法を導入し,ハードウェアの形式的検証に適用する。 我々の新しいアプローチは、ニューラルネットワークを線形時間論理の形式証明証明として用いることによって、機械学習と記号推論を組み合わせる。 提案手法は,SystemVerilogで記述された標準的なハードウェア設計において,最先端の学術的,商業的なモデルチェッカーよりも優れていることを示す。
  論文  参考訳（メタデータ） (2024-10-31T10:17:04Z)
• Bisimulation Learning [55.859538562698496]
  我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。 提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
  論文  参考訳（メタデータ） (2024-05-24T17:11:27Z)
• Formal Methods for Autonomous Systems [21.989467515686858]
  形式的手法は安全クリティカルシステムの正当性を確立する上で重要な役割を果たしてきた。 形式的なメソッドの主なビルディングブロックはモデルと仕様です。 様々な定式化の下で, 正しい構成合成を考察する。
  論文  参考訳（メタデータ） (2023-11-02T14:18:43Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。 コントローラと証明書を形式的に合成する自動化手法を提案する。 我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
  論文  参考訳（メタデータ） (2023-09-12T09:37:26Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  安全クリティカル制御システムのためのモデルベース強化学習では,システム特性を正式に認定することが重要である。 本稿では,強化学習と形式検証を共同で行う枠組みを提案する。
  論文  参考訳（メタデータ） (2022-01-28T16:53:56Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。