Granite: A Modular Methodology for Foundational Verification of Hardware-Software Leakage Contracts

• URL: http://arxiv.org/abs/2607.27480v1
• Date: Wed, 29 Jul 2026 21:44:57 GMT
• Title: Granite: A Modular Methodology for Foundational Verification of Hardware-Software Leakage Contracts
• Abstract summary: Granite is a methodology for modular verification of both functional correctness and nonleakage of RTL processors against ISA contracts.<n>We prove that the cycle-by-cycle timing of a pipelined RISC design--with speculation, precise interrupts, and I/O--is determined solely by observables specified in an ISA leakage contract.
• Score: 2.76228438275135
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Granite is a methodology for modular verification of both functional correctness and nonleakage of RTL processors against ISA contracts. We prove that the cycle-by-cycle timing of a pipelined RISC design--with speculation, precise interrupts, and I/O--is determined solely by observables specified in an ISA leakage contract. For programs that keep observables independent of secrets (i.e., following the cryptographic-constant-time discipline), this result rules out information leakage through known and unknown timing side channels. Granite's specifications only constrain functional correctness and information-flow dependencies: not how many cycles an instruction takes, at which instruction an interrupt is handled, or the exact latencies of submodules such as multipliers and memory. Granite's central technique is leakage-aware refinement via determinism, which establishes correctness and confidentiality together as trace equivalence with respect to a family of cycle-level, deterministic spec machines. Secret-independent nondeterminism is handled by existentially parameterizing specs with untrusted, deterministic functions acting only on public data. Submodules are proved against their own leakage-aware specs, and these proofs compose into the whole-design guarantee--which therefore holds over a space of secure implementations. We believe this work is the first to achieve modular and foundational connection between instruction-set-level leakage contracts and microarchitecture-specific cycle-by-cycle execution with wire-level observations. Our proofs compose with a certified static analysis that recognizes cryptographic-constant-time code to derive a single Rocq theorem about the cycle-by-cycle confidentiality of a hardware-and-software cryptographic implementation--eliminating every intermediate specification, including the ISA contract itself, from the trusted computing base.

Related papers

• TELLER: Non-intrusive Cross-Layer Root-Cause Analysis for LLM Inference [47.62941623025392]
  We present TELLER, a non-intrusive and Log-aware LLM inference Root-cause analysis framework.<n>TELLER collects NVTX/CUPTI traces and service logs without modifying model binaries.<n>It reconstructs per-request call-chain trees and aligns log lines with corresponding execution steps.<n>On top of these representations, TELLER combines numeric candidate localization with a multimodal root-cause model.
  arXiv  Detail & Related papers  (2026-08-03T09:39:11Z)
• CLOSER-Bench: Evaluating Budgeted Cross-Stage Design Closure for Hardware Agents [5.604484678527336]
  CLOSER-Bench is a controlled evaluation protocol for budgeted cross-stage design closure.<n>It pairs spec-to-RTL, RTL-to-GDS, and spec-to-GDS tasks, records every simulator, synthesis, STA, and place-and-route invocation.<n>It measures final quality, anytime progress, tool cost, and cross-stage recovery.
  arXiv  Detail & Related papers  (2026-07-18T04:28:47Z)
• LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean [9.293322518056357]
  We present an approach that combines type-based reasoning with trace-based reasoning, enabling modular verification of stateful and unbounded protocols.<n>We implement this framework as the LeanDY library for the Lean proof assistant, building on and extending the design of DY*.<n>We formalize SegWit-style blockchain primitives in LeanDY and demonstrate its expressiveness by carrying out an in-depth formalization of payment channels.
  arXiv  Detail & Related papers  (2026-07-03T15:12:30Z)
• AnchorMoE: Interpretable Time Series Classification via Anchor-Routed MoE [51.994752158953084]
  AnchorMoE is an interpretable-by-construction classification framework.<n>It encodes multi-view representations of local patches and routes them to specialized experts.<n>Experiments on real-world and synthetic benchmarks demonstrate that AnchorMoE achieves highly competitive classification performance.
  arXiv  Detail & Related papers  (2026-06-02T13:30:54Z)
• The Path Matters: Learning a Token-Commitment Policy for Diffusion Language Models [52.93186090124315]
  We argue that token commitment can be learned as a reusable trace-state policy.<n>We introduce TraceLock, a lightweight plug-in controller that instantiates this policy for a frozen diffusion language model.
  arXiv  Detail & Related papers  (2026-05-23T18:23:46Z)
• Certified Circuits: Stability Guarantees for Mechanistic Circuits [80.30622018787835]
  Certified Circuits provides provable stability guarantees for circuit discovery.<n>On ImageNet and OOD datasets, certified circuits achieve up to 91% higher accuracy.
  arXiv  Detail & Related papers  (2026-02-26T13:07:31Z)
• Symfrog-512: High-Capacity Sponge-Based AEAD Cipher (1024-bit State) [0.0]
  This submission includes a complete reference implementation together with deterministic test vectors and a reproducible benchmark suite.<n>The AEAD construction is fully specified, including domain separation, rate and capacity choices, tag generation, and the exact file format used by the reference CLI.<n>Reported performance numbers are produced by the built in benchmark tool under documented hardware and compiler settings.
  arXiv  Detail & Related papers  (2026-02-19T23:39:54Z)
• Unsupervised Conformal Inference: Bootstrapping and Alignment to Control LLM Uncertainty [49.19257648205146]
  We propose an unsupervised conformal inference framework for generation.<n>Our gates achieve close-to-nominal coverage and provide tighter, more stable thresholds than split UCP.<n>The result is a label-free, API-compatible gate for test-time filtering.
  arXiv  Detail & Related papers  (2025-09-26T23:40:47Z)
• 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)
• HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
  Confidential computing enables the protection of confidential code and data in a co-tenanted cloud deployment using specialized hardware isolation units called Trusted Execution Environments (TEEs) TEEs offer low-level C/C++-based toolchains that are susceptible to inherent memory safety vulnerabilities and lack language constructs to monitor explicit and implicit information-flow leaks. We address the above with HasTEE+, a domain-specific language (cla) embedded in Haskell that enables programming TEEs in a high-level language with strong type-safety.
  arXiv  Detail & Related papers  (2024-01-17T00:56:23Z)
• A Scalable Formal Verification Methodology for Data-Oblivious Hardware [3.518548208712866]
  We propose a novel methodology to formally verify data-oblivious behavior in hardware using standard property checking techniques. We show that proving this inductive property is sufficient to exhaustively verify data-obliviousness at the microarchitectural level. One case study uncovered a data-dependent timing violation in the extensively verified and highly secure IBEX RISC-V core.
  arXiv  Detail & Related papers  (2023-08-15T13:19:17Z)
• Short Blocklength Wiretap Channel Codes via Deep Learning: Design and Performance Evaluation [5.203329540700176]
  We design short blocklength codes for the Gaussian wiretap channel under information-theoretic security guarantees. We handle the reliability constraint via an autoencoder, and handle the secrecy constraint with hash functions. For blocklengths smaller than or equal to 16, we evaluate through simulations the probability of error at the legitimate receiver.
  arXiv  Detail & Related papers  (2022-06-07T17:52:46Z)

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.