論文の概要: Guarded Equivalence Predicates for Scalable Formal Hardware Information-Flow Verification
- arxiv url: http://arxiv.org/abs/2606.22063v1
- Date: Sat, 20 Jun 2026 14:25:13 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-25 23:00:57.719735
- Title: Guarded Equivalence Predicates for Scalable Formal Hardware Information-Flow Verification
- Title（参考訳）: スケーラブルなハードウェア情報フロー検証のためのガード付き等価式
- Authors: Liangtao Dai, Yimin Gao, Melika Morsali, Mircea R. Stan,
- Abstract要約: 自己構成は、情報フロー検証を2つの回路コピー上の安全性チェックに還元する。
近年のPDRに基づく手法では、複写対称性と大域的クロスコピー等価式を用いて、この重複構造を利用する。
我々はこれらの関係をPDRに公開するために、ガード付き等価述語を導入する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Formal hardware information-flow verification is a principled way to rule out secret-dependent functional or timing observations, but scaling such proofs remains difficult. Self-composition reduces information-flow verification to safety checking over two circuit copies, creating relational proof obligations that are hard for a generic PDR engine to discover from bit-level logic alone. Recent PDR-based techniques exploit this duplicated structure through copy symmetry and global cross-copy equivalence predicates. These predicates are effective when corresponding internal signals agree throughout the reachable state space, but they do not capture equalities that are relevant only in a specific control context. We observe that such contextual relations arise naturally in hardware IFV proofs: an internal signal pair may need to agree only within a control phase, transaction window, loop state, or protocol region. We introduce guarded equivalence predicates to expose these relations to PDR. Rather than treating a proposed contextual equality as an assumption, the verifier submits the corresponding mismatch condition as an auxiliary blocking obligation. Guards are proposed from relational counterexamples-to-induction using CTI-local extraction and state-split search; only candidates proved unreachable by the backend affect the proof. Across 12 IFV benchmarks and two PDR backends, guarded predicates convert two contextual baseline timeouts into completed proofs within 34.2--89.5s under an 1800s limit, while reducing proof time by up to 10.8x on additional benchmarks.
- Abstract（参考訳）: 形式的ハードウェア情報フロー検証は、秘密に依存した機能やタイミングの観測を除外する原則的な方法であるが、そのような証明のスケールは依然として困難である。
自己合成は、情報フロー検証を2つの回路コピー上の安全性チェックに還元し、一般的なPDRエンジンがビットレベル論理のみから発見することが難しいリレーショナル証明義務を作成する。
近年のPDRに基づく手法では、複写対称性と大域的クロスコピー等価式を用いて、この重複構造を利用する。
これらの述語は、対応する内部信号が到達可能な状態空間全体で一致した場合に有効であるが、特定の制御コンテキストにのみ関係する等式をキャプチャしない。
内部信号ペアは制御フェーズ,トランザクションウィンドウ,ループ状態,プロトコル領域内でのみ一致する必要がある。
我々はこれらの関係をPDRに公開するために、ガード付き等価述語を導入する。
検証者は、提案された文脈等式を仮定として扱うのではなく、補助的ブロッキング義務として対応するミスマッチ条件を提出する。
CTI局所抽出とステートスプリット探索を併用したリレーショナル・カウンター・サンプル・ツー・インダクション(英語版)からガードが提案されている。
12のIFVベンチマークと2つのPDRバックエンドにおいて、ガード付き述語は2つの文脈ベースラインタイムアウトを1800sの制限下で34.2-89.5s以内の証明に変換し、追加ベンチマークでは10.8倍の証明時間を短縮した。
関連論文リスト
- Hybrid Robustness Verification for Spatio-Temporal Neural Networks [19.026662893450425]
既存の検証方法は、過度に保守的な近似や不正な計算コストに依存している。
実際には、対向摂動は、低次元、意味論的に意味のある部分空間に制約された、構造化された空間的および時間的相関を示す。
動作認識(UCF-101)、自律運転(Udacity)、医用画像(MedMNIST)の用途を対象として、3次元CNNによる映像入力のロバスト性検証を行う。
論文 参考訳（メタデータ） (2026-06-08T17:06:51Z) - Neural Information Causality [0.0]
我々はニューラル情報因果性(Neural-IC)と呼ばれる枠組みを開発する。
本稿では,Neural-ICがクエリリーク,精度リーク,エピソード固有メモリの操作診断であることを示す。
また、1ビットの古典的RACベンチマークも提供し、関連する量子エンハンスメントがボトルネックを超える完全な情報ではないことを示す。
論文 参考訳（メタデータ） (2026-05-10T04:25:11Z) - Evaluating Prompt Injection Defenses for Educational LLM Tutors: Security-Usability-Latency Trade-offs [51.56484100374058]
ガードレールの設計には、敵の堅牢性、良質なタスクのユーザビリティ、応答レイテンシの明確なトレードオフが伴う。
決定論的パターンフィルタ,構造検証,コンテキストサンドボックス,セッションレベルの動作チェックを組み合わせた,ドメイン固有のマルチレイヤセーフガードパイプラインの評価を行った。
NeMoは16.22パーセントのFPRと1.5パーセントのレイテンシで0パーセントのバイパスに達し、Prompt Guardは38.48パーセントのFPRと3.60パーセントのバイパスを実現している。
論文 参考訳（メタデータ） (2026-03-29T18:52:01Z) - Towards Verifiable AI with Lightweight Cryptographic Proofs of Inference [3.3323431541048385]
完全証明を軽量なサンプリングベースアプローチで置き換える検証フレームワークとプロトコルを提案する。
我々は,機能的に異なるモデル間のトレース分離を活用可能な条件を定式化し,検証可能な推論プロトコルの安全性について議論する。
我々の手法は、最先端の暗号証明システムと比較して、証明時間を桁違いに削減する。
論文 参考訳（メタデータ） (2026-03-19T15:24:27Z) - The Inevitability of Side-Channel Leakage in Encrypted Traffic [18.365496056967917]
効率優先のシステムでは、少なくとも1つのアプリケーションペアが識別可能である場合、リークは避けられないことを示す。
これにより、暗号化されたトラフィックサイドチャネルのための厳密な情報理論の基礎が確立される。
論文 参考訳（メタデータ） (2026-02-15T08:55:19Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - zkStruDul: Programming zkSNARKs with Structural Duality [0.2449909275410287]
zkStruDulは、入力変換を統一し、定義を単一の複合抽象化に述語する言語である。
我々は、ソースレベルのセマンティクスを提供し、その振る舞いが予測されたセマンティクスと同一であることを証明する。
論文 参考訳（メタデータ） (2025-11-13T18:06:21Z) - SIM-CoT: Supervised Implicit Chain-of-Thought [108.30049193668083]
Implicit Chain-of-Thought(CoT)メソッドは、大規模言語モデルにおける明示的なCoT推論に代わるトークン効率の代替手段を提供する。
暗黙的なCoTの計算予算をスケールする際の中核的な不安定性問題を特定する。
そこで我々はSIM-CoTを提案する。SIM-CoTは,遅延推論空間を安定化・拡張するためのステップレベルの監視を実現するモジュールである。
論文 参考訳（メタデータ） (2025-09-24T17:01:32Z) - Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
大規模言語モデル(LLM)は、現実のパーソナライズされたアプリケーションにますます統合されている。
RAGで使用される知識基盤の貴重かつしばしばプロプライエタリな性質は、敵による不正使用のリスクをもたらす。
これらの知識基盤を保護するための透かし技術として一般化できる既存の方法は、一般的に毒やバックドア攻撃を含む。
我々は、無害な」知識基盤の著作権保護の名称を提案する。
論文 参考訳（メタデータ） (2025-02-10T09:15:56Z) - Localizing Factual Inconsistencies in Attributable Text Generation [74.11403803488643]
本稿では,帰属可能なテキスト生成における事実の不整合をローカライズするための新しい形式であるQASemConsistencyを紹介する。
QASemConsistencyは、人間の判断とよく相関する事実整合性スコアを得られることを示す。
論文 参考訳（メタデータ） (2024-10-09T22:53:48Z) - Semi-DETR: Semi-Supervised Object Detection with Detection Transformers [105.45018934087076]
半教師付き物体検出(SSOD)におけるDETRに基づくフレームワークの解析
本報告では,第1次変圧器を用いたエンド・ツー・エンド半教師対象検出器であるSemi-DETRについて述べる。
我々の手法は、最先端の手法をクリアマージンで上回る。
論文 参考訳（メタデータ） (2023-07-16T16:32:14Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。