Guarded Equivalence Predicates for Scalable Formal Hardware Information-Flow Verification

• URL: http://arxiv.org/abs/2606.22063v1
• Date: Sat, 20 Jun 2026 14:25:13 GMT
• Title: Guarded Equivalence Predicates for Scalable Formal Hardware Information-Flow Verification
• Abstract summary: Self-composition reduces information-flow verification to safety checking over two circuit copies.<n>Recent PDR-based techniques exploit this duplicated structure through copy symmetry and global cross-copy equivalence predicates.<n>We introduce guarded equivalence predicates to expose these relations to PDR.
• Score: 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.

Related papers

• Zero-Knowledge Predicate Proofs Between AI Agents: A Measured, Cross-Protocol Gateway and the Source-Integrity Gap [0.0]
  Multi-agent AI platforms move quickly from staging to production, but the way agents establish trust remains rudimentary.<n>We take provable data minimisation between agents from proposal to running system.<n>A 32-bit threshold predicate proves in 6.2 ms and verifies in 1.0 ms with a 608-byte Bulletproofs proof.
  arXiv  Detail & Related papers  (2026-08-30T23:16:17Z)
• Chiral Analysis of Smart Contracts: Detecting Vulnerabilities from Relational Inconsistencies Across Business Paths [1.5217170480235822]
  This paper introduces chiral analysis, a relational model that treats paired business paths as implicit specifications for each other.<n>We implement this idea in ChiralDetector, a Solidity prototype that extracts business paths.<n>ChiralDetector reduced 3,217 statically ranked path pairs to 1,643 semantic candidates, produced 101 deduplicated finding groups, and retained 44 strict-validator positives that manually collapsed to 13 unique issues.
  arXiv  Detail & Related papers  (2026-07-20T14:17:00Z)
• PerceptionRubrics: Calibrating Multimodal Evaluation to Human Perception [75.70273182182397]
  PerceptionRubrics is a rubric-based evaluation framework.<n>It addresses the gap between saturated benchmark scores and real-world brittleness.<n>It pairs 1,038 information-dense images with over 10,000 instance-specific rubrics.
  arXiv  Detail & Related papers  (2026-06-26T17:59:15Z)
• Hybrid Robustness Verification for Spatio-Temporal Neural Networks [19.026662893450425]
  Existing verification methods rely on overly conservative approximations or incur prohibitive computational costs.<n>In practice, adversarial perturbations exhibit structured spatial and temporal correlations, constrained to lower-dimensional, semantically meaningful subspaces.<n>We study robustness verification 3D CNNs processing video inputs, targeting applications in action recognition (UCF-101), autonomous driving (Udacity), medical imaging (MedMNIST)
  arXiv  Detail & Related papers  (2026-06-08T17:06:51Z)
• Monitoring Data-aware Temporal Properties (Extended Version) [56.386411908764494]
  We consider anticipatory monitoring of linear-time properties enriched with an arbitrary SMT theory over finite traces.<n>Anticipatory monitoring in this setting is highly challenging, as the monitoring state depends on both the trace prefix seen so far and all its possible finite continuations.<n>We present and formally prove the correctness of a novel foundational framework for monitoring properties in an expressive fragment offMT.
  arXiv  Detail & Related papers  (2026-05-14T10:23:11Z)
• Neural Information Causality [0.0]
  We develop a framework called neural information causality (Neural-IC)<n>We show that Neural-IC is an operational diagnostic for query leakage, precision leakage, and episode-specific memory.<n>We also provide an exact one-bit classical RAC benchmark, showing explicitly that the relevant quantum enhancement is not total information beyond the bottleneck.
  arXiv  Detail & Related papers  (2026-05-10T04:25:11Z)
• Evaluating Prompt Injection Defenses for Educational LLM Tutors: Security-Usability-Latency Trade-offs [51.56484100374058]
  guardrail design entails explicit trade-offs among adversarial robustness, benign-task usability, and response latency.<n>We evaluate a domain-specific multi-layer safeguard pipeline combining deterministic pattern filters, structural validation, contextual sandboxing, and session-level behavioral checks.<n>Results expose operational trade-offs: NeMo reaches 0 percent bypass at 16.22 percent FPR and roughly 1.5s latency, while Prompt Guard yields 38.48 percent bypass with 3.60 percent FPR.
  arXiv  Detail & Related papers  (2026-03-29T18:52:01Z)
• Towards Verifiable AI with Lightweight Cryptographic Proofs of Inference [3.3323431541048385]
  We present a verification framework and protocol that replaces full proofs with a lightweight, sampling-based approach.<n>We formalize the conditions under which trace separation between functionally dissimilar models can be leveraged to argue the security of verifiable inference protocols.<n>Our approach reduces proving times by several orders of magnitude compared to state-of-the-art cryptographic proof systems.
  arXiv  Detail & Related papers  (2026-03-19T15:24:27Z)
• The Inevitability of Side-Channel Leakage in Encrypted Traffic [18.365496056967917]
  We show that in efficiency-prioritized systems, leakage is inevitable when at least one application pair is distinguishable.<n>This establishes the first rigorous information-theoretic foundation for encrypted traffic side channels.
  arXiv  Detail & Related papers  (2026-02-15T08:55:19Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• zkStruDul: Programming zkSNARKs with Structural Duality [0.2449909275410287]
  zkStruDul is a language that unifies input transformations and predicate definitions into a single combined abstraction.<n>We provide a source-level semantics and prove its behavior is identical to the projected semantics, allowing straightforward standard reasoning.
  arXiv  Detail & Related papers  (2025-11-13T18:06:21Z)
• SIM-CoT: Supervised Implicit Chain-of-Thought [108.30049193668083]
  Implicit Chain-of-Thought (CoT) methods offer a token-efficient alternative to explicit CoT reasoning in Large Language Models.<n>We identify a core latent instability issue when scaling the computational budget of implicit CoT.<n>We propose SIM-CoT, a plug-and-play training module that introduces step-level supervision to stabilize and enrich the latent reasoning space.
  arXiv  Detail & Related papers  (2025-09-24T17:01:32Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  Large language models (LLMs) are increasingly integrated into real-world personalized applications.<n>The valuable and often proprietary nature of the knowledge bases used in RAG introduces the risk of unauthorized usage by adversaries.<n>Existing methods that can be generalized as watermarking techniques to protect these knowledge bases typically involve poisoning or backdoor attacks.<n>We propose name for harmless' copyright protection of knowledge bases.
  arXiv  Detail & Related papers  (2025-02-10T09:15:56Z)
• Localizing Factual Inconsistencies in Attributable Text Generation [74.11403803488643]
  We introduce QASemConsistency, a new formalism for localizing factual inconsistencies in attributable text generation.<n>We show that QASemConsistency yields factual consistency scores that correlate well with human judgments.
  arXiv  Detail & Related papers  (2024-10-09T22:53:48Z)
• Semi-DETR: Semi-Supervised Object Detection with Detection Transformers [105.45018934087076]
  We analyze the DETR-based framework on semi-supervised object detection (SSOD) We present Semi-DETR, the first transformer-based end-to-end semi-supervised object detector. Our method outperforms all state-of-the-art methods by clear margins.
  arXiv  Detail & Related papers  (2023-07-16T16:32:14Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.