論文の概要: Proving Circuit Functional Equivalence in Zero Knowledge

• arxiv url: http://arxiv.org/abs/2601.11173v1
• Date: Fri, 16 Jan 2026 10:43:30 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-19 20:21:50.452487
• Title: Proving Circuit Functional Equivalence in Zero Knowledge
• Title（参考訳）: ゼロ知識における回路機能等価性の証明
• Authors: Sirui Shen, Zunchen Huang, Chenglu Jin,
• Abstract要約: ハードウェア形式検証のための最初のプライバシ保護フレームワークであるZK-CECを提案する。 正式な検証とゼロ知識証明(ZKP)を組み合わせることで、ZK-CECはIPの正当性とセキュリティを正式に検証する基盤を確立する。 ZK- CECは、AES S-Boxのような実用的な設計を実用時間内に検証することに成功した。
• 参考スコア（独自算出の注目度）: 4.301822791698451
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The modern integrated circuit ecosystem is increasingly reliant on third-party intellectual property integration, which introduces security risks, including hardware Trojans and security vulnerabilities. Addressing the resulting trust deadlock between IP vendors and system integrators without exposing proprietary designs requires novel privacy-preserving verification techniques. However, existing privacy-preserving hardware verification methods are all simulation-based and fail to offer formal guarantees. In this paper, we propose ZK-CEC, the first privacy-preserving framework for hardware formal verification. By combining formal verification and zero-knowledge proof (ZKP), ZK-CEC establishes a foundation for formally verifying IP correctness and security without compromising the confidentiality of the designs. We observe that existing zero-knowledge protocols for formal verification are designed to prove statements of public formulas. However, in a privacy-preserving verification context where the formula is secret, these protocols cannot prevent a malicious prover from forging the formula, thereby compromising the soundness of the verification. To address these gaps, we first propose a blueprint for proving the unsatisfiability of a secret design against a public constraint, which is widely applicable to proving properties in software, hardware, and cyber-physical systems. Based on the proposed blueprint, we construct ZK-CEC, which enables a prover to convince the verifier that a secret IP's functionality aligns perfectly with the public specification in zero knowledge, revealing only the length and width of the proof. We implement ZK-CEC and evaluate its performance across various circuits, including arithmetic units and cryptographic components. Experimental results show that ZK-CEC successfully verifies practical designs, such as the AES S-Box, within practical time limits.
• Abstract（参考訳）: 現代の集積回路エコシステムは、ハードウェアトロイの木馬やセキュリティ脆弱性を含むセキュリティリスクをもたらす、サードパーティの知的財産統合にますます依存している。 プロプライエタリな設計を公開することなく、IPベンダーとシステムインテグレータ間の信頼のデッドロックに対処するには、新しいプライバシ保護検証技術が必要である。 しかし、既存のプライバシ保護ハードウェア検証手法はすべてシミュレーションベースであり、正式な保証を提供していない。 本稿では,ZK-CECを提案する。 ZK-CECは、正式な検証とゼロ知識証明(ZKP)を組み合わせることで、設計の秘密性を損なうことなく、IPの正当性とセキュリティを正式に検証する基盤を確立する。 公式検証のための既存のゼロ知識プロトコルは、公定公式のステートメントを証明するために設計されている。 しかし、これらのプロトコルは、公式が秘密であるプライバシー保護検証コンテキストにおいて、悪意のある証明者が公式を偽造することを防げず、検証の健全性を損なう。 これらのギャップに対処するために、我々はまず、ソフトウェア、ハードウェア、サイバー物理システムの特性の証明に広く適用可能な、公開制約に対する秘密設計の不満足性を証明するための青写真を提案する。 提案した青写真に基づいて,ZK-CECを構築することで,秘密IPの機能をゼロ知識で公開仕様と完全に整合し,証明の長さと幅だけを明らかにする。 我々は、ZK-CECを実装し、演算ユニットや暗号コンポーネントを含む様々な回路上での性能を評価する。 実験結果から,ZK-CECは,AES S-Boxのような実用的設計を実用的時間内に検証することに成功した。

関連論文リスト

• Securing Generative AI in Healthcare: A Zero-Trust Architecture Powered by Confidential Computing on Google Cloud [0.0]
  Confidential Zero-Trust Framework (CZF) は、Zero-Trust ArchitectureとConfidential Computingのハードウェア強化データアイソレーションを組み合わせたセキュリティパラダイムである。 CZFは、ハードウェアベースのTrusted Execution Environment内で使用中にデータが暗号化される詳細なアーキテクチャを提供する。
  論文  参考訳（メタデータ） (2025-11-14T19:56:52Z)
• CSI-IBBS: Identity-Based Blind Signature using CSIDH [0.0]
  CSIDHフレームワークを用いた最上位ゼロ知識検証器を用いたアイデンティティベースブラインド署名方式を提案する。 本稿では,標準暗号モデルにおいて導入されたプロトコルのセキュリティを分析し,プライバシと検証の正当性を保護する上での有効性を実証する。 この研究は、ポスト量子時代のセキュアでスケーラブルな暗号システムの構築を促進する。
  論文  参考訳（メタデータ） (2025-09-07T16:31:16Z)
• Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks (extended version) [1.5997757408973357]
  音響アニメーションを生成するIsabelle形式を用いたNeedham-Schroederプロトコルをモデル化する。 以上の結果から,すべてのシナリオにおいて信頼性が保たれていることが示唆された。 我々は、透かしとジャミングを統合したPLSベースのDiffie-Hellmanプロトコルを提案している。
  論文  参考訳（メタデータ） (2025-08-26T20:59:16Z)
• Structural Vulnerability in Y00 Protocols [0.0]
  本稿では,古典的暗号手法を強化するために提案された量子ノイズベースのストリーム暗号であるY00プロトコルを批判的に分析する。 測定結果から秘密情報を漏洩させる構造的脆弱性を明らかにする。
  論文  参考訳（メタデータ） (2024-12-10T08:29:44Z)
• Balancing Confidentiality and Transparency for Blockchain-based Process-Aware Information Systems [43.253676241213626]
  機密性と透明性を維持するために,ブロックチェーンベースのPAISアーキテクチャを提案する。 スマートコントラクトは公開インタラクションを制定、強制、保存し、属性ベースの暗号化技術は機密情報へのアクセス許可を指定するために採用されている。 システム的脅威モデル解析によりソリューションの安全性を評価し,その実用性を評価する。
  論文  参考訳（メタデータ） (2024-12-07T20:18:36Z)
• ACRIC: Securing Legacy Communication Networks via Authenticated Cyclic Redundancy Integrity Check [98.34702864029796]
  安全クリティカルな業界における最近のセキュリティインシデントは、適切なメッセージ認証の欠如により、攻撃者が悪意のあるコマンドを注入したり、システムの振る舞いを変更することができることを明らかにした。 これらの欠点は、サイバーセキュリティを強化するために圧力をかける必要性を強調する新しい規制を引き起こしている。 我々は,レガシ産業通信をセキュアにするためのメッセージ認証ソリューションであるACRICを紹介する。
  論文  参考訳（メタデータ） (2024-11-21T18:26:05Z)
• Coding-Based Hybrid Post-Quantum Cryptosystem for Non-Uniform Information [53.85237314348328]
  我々は、新しいハイブリッドユニバーサルネットワーク符号化暗号(NU-HUNCC)を導入する。 NU-HUNCCは,リンクのサブセットにアクセス可能な盗聴者に対して,個別に情報理論的に保護されていることを示す。
  論文  参考訳（メタデータ） (2024-02-13T12:12:39Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。 本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。 実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
  論文  参考訳（メタデータ） (2024-01-19T14:52:04Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  完全同型暗号方式として, 完全同型暗号方式を初めて構築する。 我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
  論文  参考訳（メタデータ） (2022-03-03T10:07:32Z)

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

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