Synthesis of Sound and Precise Leakage Contracts for Open-Source RISC-V Processors

• URL: http://arxiv.org/abs/2509.06509v1
• Date: Mon, 08 Sep 2025 10:14:52 GMT
• Title: Synthesis of Sound and Precise Leakage Contracts for Open-Source RISC-V Processors
• Authors: Zilong Wang, Gideon Mohr, Klaus von Gleissenthall, Jan Reineke, Marco Guarnieri,
• Abstract summary: Leakage contracts aim to capture the information that processors may leak via microarchitectural side channels.<n>LeaSyn is the first tool for automatically synthesizing leakage contracts that are both sound and precise for processor designs at register-transfer level.<n>Our experiments indicate that LeaSyn's contracts are sound and more precise (i.e., represent the actual leaks in the target processor more faithfully) than contracts constructed by existing approaches.
• Score: 10.160855270787962
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Leakage contracts have been proposed as a new security abstraction at the instruction set architecture level. Leakage contracts aim to capture the information that processors may leak via microarchitectural side channels. Recently, the first tools have emerged to verify whether a processor satisfies a given contract. However, coming up with a contract that is both sound and precise for a given processor is challenging, time-consuming, and error-prone, as it requires in-depth knowledge of the timing side channels introduced by microarchitectural optimizations. In this paper, we address this challenge by proposing LeaSyn, the first tool for automatically synthesizing leakage contracts that are both sound and precise for processor designs at register-transfer level. Starting from a user-provided contract template that captures the space of possible contracts, LeaSyn automatically constructs a contract, alternating between contract synthesis, which ensures precision based on an empirical characterization of the processor's leaks, and contract verification, which ensures soundness. Using LeaSyn, we automatically synthesize contracts for six open-source RISC-V CPUs for a variety of contract templates. Our experiments indicate that LeaSyn's contracts are sound and more precise (i.e., represent the actual leaks in the target processor more faithfully) than contracts constructed by existing approaches.

Related papers

• Wireless TokenCom: RL-Based Tokenizer Agreement for Multi-User Wireless Token Communications [59.84545048095092]
  Token Communications (TokenCom) has recently emerged as an effective new paradigm, where tokens are the unified units of communications computations.<n>We investigate a multi-user downlink wireless TokenCom scenario, where the base station transmits multiple users.
  arXiv  Detail & Related papers  (2026-02-12T19:00:33Z)
• Contract2Plan: Verified Contract-Grounded Retrieval-Augmented Optimization for BOM-Aware Procurement and Multi-Echelon Inventory Planning [0.0]
  We introduce Contract2Plan, a verified GenAI-to-optimizer pipeline that inserts a solver-based compliance gate before plans are emitted.<n>The system retrieves clause evidence with provenance, extracts a typed constraint schema with evidence spans, compiles constraints into a BOM-aware MILP, and verifies grounding, eligibility, consistency, and feasibility.
  arXiv  Detail & Related papers  (2026-01-07T01:38:05Z)
• One Signature, Multiple Payments: Demystifying and Detecting Signature Replay Vulnerabilities in Smart Contracts [56.94148977064169]
  lacking checks on signature usage conditions can lead to repeated verifications, increasing the risk of permission abuse and threatening contract assets.<n>We define this issue as the Signature Replay Vulnerability (SRV)<n>From 1,419 audit reports across 37 blockchain security companies, we identified 108 with detailed SRV descriptions and classified five types of SRVs.
  arXiv  Detail & Related papers  (2025-11-12T09:17:13Z)
• Coverage-Guided Pre-Silicon Fuzzing of Open-Source Processors based on Leakage Contracts [1.2413165648298643]
  Hardware-software leakage contracts have emerged as a formalism for specifying side-channel security guarantees of modern processors.<n>Current verification approaches struggle to scale to industrial-sized designs.<n>We introduce a novel and scalable approach: coverage-guided hardware-software contract fuzzing.
  arXiv  Detail & Related papers  (2025-11-11T16:46:35Z)
• Trace: Securing Smart Contract Repository Against Access Control Vulnerability [58.02691083789239]
  GitHub hosts numerous smart contract repositories containing source code, documentation, and configuration files.<n>Third-party developers often reference, reuse, or fork code from these repositories during custom development.<n>Existing tools for detecting smart contract vulnerabilities are limited in their ability to handle complex repositories.
  arXiv  Detail & Related papers  (2025-10-22T05:18:28Z)
• Exploring Microstructural Dynamics in Cryptocurrency Limit Order Books: Better Inputs Matter More Than Stacking Another Hidden Layer [9.2463347238923]
  We aim to examine whether adding extra hidden layers or parameters to "blackbox ish" neural networks genuinely enhances short term price forecasting.<n>We benchmark a spectrum of models from interpretable baselines, logistic regression, XGBoost to deep architectures (DeepLOB, Conv1D+LSTM) on BTC/USDT LOB snapshots sampled at 100 ms to multi second intervals using publicly available Bybit data.
  arXiv  Detail & Related papers  (2025-06-06T05:43:30Z)
• Specification Mining for Smart Contracts with Trace Slicing and Predicate Abstraction [10.723903783651537]
  We propose a specification mining approach to infer contract specifications from past transaction histories.<n>Our approach derives high-level behavioral automata of function invocations, accompanied by program invariants statistically inferred from the transaction histories.<n>Experiments show that SMCON mines reasonably accurate specifications that can be used to enhance symbolic analysis of smart contracts achieving higher code coverage and up to 56% speedup.
  arXiv  Detail & Related papers  (2024-03-20T03:39:51Z)
• Synthesizing Hardware-Software Leakage Contracts for RISC-V Open-Source Processors [6.061386291375516]
  We propose a semi-automatic methodology for synthesizing hardware-software leakage contracts for open-source microarchitectures. We have instantiated this methodology for the RISC-V ISA and applied it to the Ibex and CVA6 open-source processors.
  arXiv  Detail & Related papers  (2024-01-17T17:54:53Z)
• 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)
• Gradual Verification for Smart Contracts [0.4543820534430522]
  Algos facilitate secure resource transactions through smart contracts, yet these digital agreements are prone to vulnerabilities. Traditional verification techniques fall short in providing comprehensive security assurances. This paper introduces an incremental approach: gradual verification.
  arXiv  Detail & Related papers  (2023-11-22T12:42:26Z)
• ConReader: Exploring Implicit Relations in Contracts for Contract Clause Extraction [84.0634340572349]
  We study automatic Contract Clause Extraction (CCE) by modeling implicit relations in legal contracts. In this work, we first comprehensively analyze the complexity issues of contracts and distill out three implicit relations commonly found in contracts. We propose a novel framework ConReader to exploit the above three relations for better contract understanding and improving CCE.
  arXiv  Detail & Related papers  (2022-10-17T02:15:18Z)
• Data post-processing for the one-way heterodyne protocol under composable finite-size security [62.997667081978825]
  We study the performance of a practical continuous-variable (CV) quantum key distribution protocol. We focus on the Gaussian-modulated coherent-state protocol with heterodyne detection in a high signal-to-noise ratio regime. This allows us to study the performance for practical implementations of the protocol and optimize the parameters connected to the steps above.
  arXiv  Detail & Related papers  (2022-05-20T12:37:09Z)
• Detecting Logical Relation In Contract Clauses [94.85352502638081]
  We develop an approach to automate the extraction of logical relations between clauses in a contract. The resulting approach should help contract authors detecting potential logical conflicts between clauses.
  arXiv  Detail & Related papers  (2021-11-02T19:26:32Z)
• Composably secure data processing for Gaussian-modulated continuous variable quantum key distribution [58.720142291102135]
  Continuous-variable quantum key distribution (QKD) employs the quadratures of a bosonic mode to establish a secret key between two remote parties. We consider a protocol with homodyne detection in the general setting of composable finite-size security. In particular, we analyze the high signal-to-noise regime which requires the use of high-rate (non-binary) low-density parity check codes.
  arXiv  Detail & Related papers  (2021-03-30T18:02:55Z)

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.