Pith. sign in

REVIEW 4 major objections 5 minor 57 references

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

T0 review · 4 major / 5 minor · reviewed 2026-08-04 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read LeaSyn automatically synthesizes leakage contracts that are both sound and precise for RISC-V processors, directly from register-transfer-level designs.

desk verdict A real step forward in leakage-contract synthesis, with a couple of addressable warts: a precision-formula typo and an honest but under-specified dependence on template completeness. read the letter →

arxiv 2509.06509 v1 pith:7FR4F5YC submitted 2025-09-08 cs.CR

Zilong Wang , Gideon Mohr , Klaus von Gleissenthall , Jan Reineke , Marco Guarnieri This is my paper · ORCID
classification cs.CR
keywords sidechannelsleakagecontractsRISC-Vregister-transferlevelcontractsynthesistimingleakshardwareverification
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

LeaSyn aims to close the gap between two existing kinds of leakage-contract synthesis for RISC-V processors: one that produces precise contracts but cannot guarantee soundness, and one that produces sound but very imprecise contracts. Starting from an RTL design and a user-supplied contract template, LeaSyn alternates between an ILP-based synthesis step that picks the most precise contract consistent with empirical tests and a bounded verification step that hunts for leaks the tests missed, then finishes with an unbounded verification that proves the final contract sound. The paper reports that this pipeline synthesized sound contracts for six open-source RISC-V cores in under 48 hours each, with precision above 0.99 for all but one core where the template cannot capture the cache's actual leakage. If the method works as claimed, it removes a major manual step in hardware side-channel assurance: programmers get a processor-specific, machine-checked description of what timing information the CPU exposes.

What carries the argument

The load-bearing object is the contract template: a finite set of contract atoms, each an applicability predicate over architectural states and a leakage function that maps a state to an observation. Any subset of atoms is a candidate contract. The paper introduces two notions that make template-based synthesis tractable: strongly-distinguishing atoms and xor-distinguishing pairs, which together fully characterize when any contract distinguishes a test case (Proposition 1). This characterization feeds an ILP whose objective minimizes false positives while forcing all empirically attacker-distinguishable tests to be contract-distinguishable. A stuttering product circuit built from two copies

What would settle it

Take a processor with a known timing leak that is absent from the supplied template, for example a cache whose timing depends on whether two consecutive accesses hit the same line when the template only exposes addresses. Running LeaSyn should fail to produce a sound contract, or should return a contract with low precision, as the Ibex-cache experiment already shows. More directly, one could take a synthesized contract and search by black-box differential testing on random program pairs for a pair of executions with identical contract traces but different retirement times; finding one would fa

Watch

Extended reading notes

Core claim

The central claim is that LeaSyn is the first tool to automatically synthesize leakage contracts that are both sound and precise from register-transfer-level processor designs. Soundness means any two executions an attacker can tell apart by observing instruction retirement must produce different contract traces; precision means the contract over-approximates actual leakage as little as possible. The paper formalizes contracts as subsets of a user-provided template of atoms, each an applicability predicate paired with a leakage function. LeaSyn first characterizes leakage empirically on generated test cases, solves an integer-linear program to pick a minimal atom set that distinguishes all a

Load-bearing premise

LeaSyn's soundness guarantee holds only if the user-supplied contract template already contains an atom capable of expressing every leak the processor actually has; if some leak has no matching atom, no contract in the search space is sound.

Editorial extensions

If this is right

  • A user who can write or reuse a template no longer needs to reverse-engineer timing leaks manually; the tool returns a machine-checked contract from RTL.
  • Software-level constant-time reasoning can be tied to a specific processor: programs can be checked against the synthesized contract instead of against a generic, overly conservative policy.
  • The alternating loop is guaranteed to terminate because each bounded counterexample rules out at least one candidate contract, so the search is finite.
  • The precision measurements indicate that contracts synthesized by LeaSyn distinguish far fewer attacker-indistinguishable executions than contracts from prior sound synthesis approaches, so fewer secure programs would be rejected as leaky.
  • The bounded-verification step with a dynamic instruction bound can serve as a fast pre-filter before expensive unbounded verification, reducing total synthesis time.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Because the guarantee in Proposition 6 is relative to the test cases explored during synthesis, the claimed precision is an empirical property of those tests, not a mathematical optimum over all possible programs; different test sets could yield different optimal contracts.
  • The single-line-cache case suggests the main practical bottleneck is template expressiveness: richer atoms encoding something like 'same address as the immediately preceding access' could probably restore high precision for cores with small caches.
  • The same synthesis loop could in principle be applied to other attacker models and instruction sets, since the formal model is not RISC-V-specific; the RISC-V formal interface is only the implementation substrate.
  • If templates were extended with atoms that expose sequences of instructions or speculation-related events, the method might generalize to speculative-leak contracts, though the paper explicitly leaves that to future work.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper presents LeaSyn, a tool and methodology for synthesizing leakage contracts for RISC-V processors directly from RTL. The user provides a contract template consisting of atoms; LeaSyn simulates generated test cases to characterize attacker-visible and contract-distinguishable behavior, uses an ILP to pick the most precise subset of atoms, alternates synthesis with bounded model checking to discover missed leaks, and finally invokes the LeaVe verifier for an unbounded soundness check. The authors evaluate on six open-source RISC-V cores and report contracts that are more precise than those from prior tools (LeaVe, Mohr et al., ConjunCT, VeloCT, RTL2MμPATH). The formal development includes propositions connecting the ILP constraints to distinguishability, the bounded verification to a bounded soundness guarantee, and the final Phase 3 to soundness of the synthesized contract.

Significance. If the results hold, this is a useful step toward automating a labor-intensive hardware-security task: deriving sound and precise ISA-level leakage contracts. The paper's strengths are its explicit formal model, the combination of empirical characterization with bounded and unbounded verification, the open-source implementation, and a broad evaluation over multiple core families with comparisons to several prior approaches. The central insight—using strongly-distinguishing atoms and xor-distinguishing pairs to characterize template distinguishability—is clean and well suited to the ILP formulation. The significance is somewhat qualified by the dependence on user-provided templates and on manually supplied invariants for the final unbounded verification, both acknowledged in the paper but relevant to the "automatic" claim.

major comments (4)
  1. [§6.1 (Evaluating precision)] The definition of precision as "FP/(TP+FP)" contradicts every reported value. With that formula, a perfect contract would have precision 0 and the Ibex-cache result 0.579 would be better than 0.999. Table 1, Table 2, Table 3, and Figure 2(b) are all consistent with the standard definition precision = TP/(TP+FP). This is a load-bearing error for the RQ1/RQ4 conclusions and must be corrected in the formula and in any accompanying prose.
  2. [§4.4, §5, §6.1] The unbounded soundness guarantee is not obtained by LeaSyn alone: Phase 3 relies on the LeaVe verifier with user-supplied relational invariants, and the evaluation explicitly re-uses manually constructed invariants from Wang et al. [50]. The paper presents LeaSyn as "automatically synthesizing" sound contracts, but for a new core a user may need to hand-craft these invariants. The manuscript should state this dependency in the main contributions and clarify which parts of the pipeline are automatic and which require expert input.
  3. [§4.3 and §7] The soundness of any output contract is conditional on the user-provided template being expressive enough to capture all leaks of the target. Section 7 acknowledges this, and RQ3 shows templates I, R, M alone admit no sound contract. However, the paper does not specify what LeaSyn does when the ILP in Eq. (1) becomes infeasible or when Phase 2b keeps producing counterexamples that no subset of T can distinguish. Since the termination argument in §4.3 only says each iteration rules out at least one contract, the behavior in the no-sound-contract case should be described explicitly, including the diagnostic returned to the user.
  4. [Proposition 6] The theorem states that the synthesized contract "distinguishes as few attacker-distinguishable test cases as possible," but the ILP objective in §4.2 minimizes false positives among attacker-indistinguishable test cases, and the surrounding text in §1 and §4.2 uses "attacker-indistinguishable." As written, Proposition 6 is either a typo or a different, unproved claim. Please correct the wording so the formal guarantee matches the synthesis objective.
minor comments (5)
  1. [§4.3] The retirement predicate is denoted φ in §3.1 and ψ in §4.3 and Appendix C; please unify the notation.
  2. [§6.1] The precision metric should be defined with enough context to distinguish TP and FP (e.g., TP = contract- and attacker-distinguishable, FP = contract-distinguishable but attacker-indistinguishable). The current sentence is also unclear about whether the validation set is balanced or whether TP+FP is always nonzero.
  3. [§2.4] In the example, Ctr2 is written both as { (div, "Reg[RS2]") } and then later as { (div, "Reg[RS2]=0?") } in the same section; this is confusing even though the template has changed. Consider renaming the contracts across template revisions.
  4. [§6.2 (RQ4)] The table labels "same-programs" and "different-programs" are used inconsistently with a hyphen and as separate words; please make them consistent.
  5. [§A.2] In the proof of Proposition 2, Lemmas 1–3 are stated after Lemma 1 references them; reordering or forward-referencing would improve readability.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the synthesis objective is explicitly scoped to explored test cases, soundness is checked by an independent unbounded verifier, and the template dependence is an acknowledged limitation rather than a circular step.

full rationale

LeaSyn's derivation chain separates three distinct activities. (1) Empirical characterization (§4.1) simulates test cases to obtain attacker distinguishability and template distinguishability; this is input data, not an output claim. (2) ILP synthesis (§4.2) selects atoms to satisfy Eq. (1) while minimizing false positives; Proposition 3 is a correctness statement about that optimization, and Proposition 6 explicitly limits the precision guarantee to 'test cases explored during the synthesis process', so it does not pass off a fitted objective as an external prediction. (3) Soundness is not claimed by construction: the paper alternates with bounded BMC (§4.3) and then invokes the LeaVe unbounded verifier (§4.4), relying on Wang et al. [50, Theorem 2]. That citation is to a separately published, peer-reviewed tool and theorem by the same research group; it is load-bearing but it is independent prior evidence, not an output of this paper, and the paper does not fit parameters to make that theorem true. The main limitation—that soundness and precision depend on the user-supplied template containing atoms able to express the processor's leaks—is stated explicitly in Section 7 ('Our approach critically relies on user-provided contract atoms...') and is demonstrated in RQ3, where isolated I, R, and M templates admit no sound contract. This is a search-space limitation, not a self-referential definition: the tool can fail or return less precise contracts when the template is inadequate, and the paper says so. No equation is defined in terms of the result it claims to prove, and no prior-work citation is used to forbid alternative choices. The comparison contracts from prior work are either taken from the respective papers or reconstructed with disclosed templates; this affects fairness, not circularity. Overall, the central claim is independently checkable: the synthesized contract is tested on held-out validation sets, and the unbounded verification is an external proof obligation.

Assumptions & free parameters 1 free parameters · 5 assumptions · 0 invented entities

The core contribution is algorithmic; the main external inputs are the contract template (user-defined) and the unbounded verifier LeaVe with manual invariants. No physical entities are invented. The bounds k, b, i are user-chosen but do not affect the final soundness guarantee.

free parameters (1)
  • BMC bound k, attacker bound b, instruction bound i = k=51, b=12, i=1 for most Ibex runs; e.g., DarkRISCV-2: k=15, b=10, i=1
    User-provided verification bounds for Phase 2b; they affect which counterexamples are found and runtime, but the final soundness guarantee rests on Phase 3 unbounded verification. They are chosen by hand, not fitted to data.
assumptions (5)
  • domain assumption Architectures and microarchitectures are deterministic state machines; ISA compliance connects architectural and microarchitectural traces via a retirement predicate (Section 3.1).
    The whole reduction from contract satisfaction to microarchitectural contract satisfaction from [50] depends on deterministic transition functions and the retirement predicate.
  • domain assumption The attacker model is a deterministic function Atk mapping each microarchitectural state to an observation; the considered attacker observes retirement timing (Section 3.3, Section 6.1).
    Attacker distinguishability is defined by inequality of Atk traces; soundness is relative to this specific attacker.
  • ad hoc to paper Contract templates satisfy mutual exclusivity of applicability predicates for atoms sharing a leakage function and disjoint images of different leakage functions (Section 3.2).
    These conditions are required for Proposition 1, which characterizes contract distinguishability; they restrict the space of templates.
  • domain assumption LeaVe unbounded verification is sound and the manually constructed invariants from [50] are sufficient for the six cores (Section 4.4, Section 6.1).
    The final soundness conclusion for the evaluated contracts rests on an external tool from the authors' prior work, not re-proven here.
  • domain assumption The synthesis loop terminates because the template is finite and each counterexample rules out at least one contract (Section 7, 'Termination of the synthesis loop').
    No formal bound on iterations is given; the argument assumes every counterexample is representable as a contract-distinguishable test case within the template.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Synthesis of Sound and Precise Leakage Contracts for Open-Source RISC-V Processors." pith.science (2026). https://pith.science/paper/7FR4F5YC

@misc{pith2026250906509,
  author       = {Pith},
  title        = {Pith review of: Synthesis of Sound and Precise Leakage Contracts for Open-Source RISC-V Processors},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/7FR4F5YC}},
  note         = {Machine review of arXiv:2509.06509}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2509.06509 by the authors.

Figure 1
Figure 1. Overview of LeaSyn synthesis approach Synthesis methodology: We propose a methodology (§4) to syn￾thesize sound and precise contracts given an RTL processor design. Our methodology starts from (a) the RTL design of the target proces￾sor, and (b) a user-provided contract template that consists of a set of contract atoms, each capturing a potential instruction-level leak. Crucially, the template defines the search spa… view at source ↗
Figure 2
Figure 2. Impact of the number of test cases on contract [PITH_FULL_IMAGE:figures/full_fig_p011_2.png] view at source ↗
Figure 3
Figure 3. Impact of template expressiveness on precision [PITH_FULL_IMAGE:figures/full_fig_p012_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Encoding of the bounded contract satisfaction property in Verilog [PITH_FULL_IMAGE:figures/full_fig_p018_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

57 extracted references · 57 canonical work pages

  1. [50]

    Zilong Wang, Gideon Mohr, Klaus von Gleissenthall, Jan Reineke, and Marco Guarnieri. 2023. Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts. InProceedings of the 30th ACM Conference on Computer and Communications Security (CCS). ACM

    work page 2023

  2. [1]

    [n. d.]. DarkRISCV processor. https://github.com/darklife/darkriscv

    work page

  3. [2]

    [n. d.]. Google OR-Tools. https://github.com/google/or-tools

    work page

  4. [3]

    [n. d.]. Ibex: An embedded 32 bit RISC-V CPU core. https://github.com/lowRISC/ ibex

    work page

  5. [4]

    [n. d.]. Ibex RISC-V Core – Mult./Divider Block. https://ibex-core.readthedocs. io/en/latest/03_reference/instruction_decode_execute.html#mult-div

    work page

  6. [5]

    [n. d.]. Icarus Verilog. https://github.com/steveicarus/iverilog

    work page

  7. [6]

    [n. d.]. RISC-V Formal Verification Framework. https://github.com/ SymbioticEDA/riscv-formal

    work page

  8. [7]

    [n. d.]. RISC-V Sodor processor. https://github.com/ucb-bar/riscv-sodor

    work page

Show all 57 references
  1. [8]

    d.].LeaSynimplementation

    [n. d.].LeaSynimplementation. https://github.com/zilongwang123/LeaSyn

  2. [9]

    [n. d.]. Yices 2 SMT Solver. https://yices.csl.sri.com

  3. [10]

    [n. d.]. Yosys Open SYnthesis Suite. https://github.com/YosysHQ/yosys

  4. [11]

    Onur Aciiçmez. 2007. Yet another MicroArchitectural Attack: Exploiting I-Cache. InProceedings of the 2007 ACM Workshop on Computer Security Architecture (CSA W). ACM

    2007

  5. [12]

    Alejandro Cabrera Aldaya, Billy Bob Brumley, Sohaib ul Hassan, Cesar Pereida García, and Nicola Tuveri. 2019. Port Contention for Fun and Profit. InProceedings of the 40th IEEE Symposium on Security and Privacy (S&P). IEEE

    2019

  6. [13]

    José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, and Michael Emmi. 2016. Verifying Constant-Time Implementations. InProceedings of the 25th USENIX Security Symposium (USENIX Security). USENIX Association

    2016

  7. [14]

    Gilles Barthe, Marcel Böhme, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Marco Guarnieri, David Mateos Romero, Peter Schwabe, David Wu, and Yuval Yarom. 2024. Testing Side-channel Security of Cryptographic Implementations against Future Microarchitectures. InPro...

    2024

  8. [15]

    D’Argenio, and Tamara Rezk

    Gilles Barthe, Pedro R. D’Argenio, and Tamara Rezk. 2011. Secure information flow by self-composition.Math. Struct. Comput. Sci.21, 6 (2011), 1207–1252

    2011

  9. [16]

    Roderick Bloem, Barbara Gigerl, Marc Gourjon, Vedad Hadzic, Stefan Mangard, and Robert Primas. 2022. Power Contracts: Provably Complete Power Leakage Models for Processors. InProceedings of the 29th ACM Conference on Computer and Communication Security (CCS). ACM

    2022

  10. [17]

    Claudio Canella, Daniel Genkin, Lukas Giner, Daniel Gruss, Moritz Lipp, Ma- rina Minkin, Daniel Moghimi, Frank Piessens, Michael Schwarz, Berk Sunar, Jo Van Bulck, and Yuval Yarom. 2019. Fallout: Leaking Data on Meltdown-resistant CPUs. InProceedings of the 26th ACM Conference...

    2019

  11. [18]

    Katharina Ceesay-Seitz, Flavien Solt, and Kaveh Razavi. 2024. 𝜇-CFI: Formal Verification of Microarchitectural Control-flow Integrity. InProceedings of the 31st ACM Conference on Computer and Communication Security (CCS). ACM. Synthesis of Sound and Precise Leakage Contracts f...

    2024

  12. [19]

    Lesly-Ann Daniel, Sébastien Bardin, and Tamara Rezk. 2020. Binsec/rel: Efficient relational symbolic execution for constant-time at binary-level. InProceedings of the 41st IEEE Symposium on Security and Privacy (S&P). IEEE

    2020

  13. [20]

    Alvise de Faveri Tron, Raphael Isemann, Hany Ragab, Cristiano Giuffrida, Klaus von Gleissenthall, and Herbert Bos. 2025. Phantom Trails: Practical Pre-Silicon Discovery of Transient Data Leaks. InProceedings of the 34th USENIX Security Symposium (USENIX Security). USENIX Association

    2025

  14. [21]

    Fletcher

    Sushant Dinesh, Madhusudan Parthasarathy, and Christopher W. Fletcher. 2024. ConjunCT: Learning Inductive Invariants to Prove Unbounded Instruction Safety Against Microarchitectural Timing Attacks. InProceedings of the 45th IEEE Sym- posium on Security and Privacy (S&P). IEEE

    2024

  15. [22]

    Fletcher

    Sushant Dinesh, Yongye Zhu, and Christopher W. Fletcher. 2025. H-Houdini: Scalable Invariant Learning. InProceedings of the 30th ACM International Confer- ence on Architectural Support for Programming Languages and Operating Systems (ASPLOS). ACM

    2025

  16. [23]

    Goran Doychev, Boris Köpf, Laurent Mauborgne, and Jan Reineke. 2015. CacheAu- dit: A Tool for the Static Analysis of Cache Side Channels.ACM Trans. Inf. Syst. Secur.18, 1 (2015)

    2015

  17. [24]

    Xaver Fabian, Marco Patrignani, and Marco Guarnieri. 2022. Automatic Detection of Speculative Execution Combinations. InProceedings of the 29th ACM SIGSAC Conference on Computer and Communications Security (CCS). ACM

    2022

  18. [25]

    Xaver Fabian, Marco Patrignani, Marco Guarnieri, and Michael Backes. 2025. Do You Even Lift? Strengthening Compiler Security Guarantees against Spectre Attacks.Proc. ACM Program. Lang.9, POPL (Jan. 2025)

    2025

  19. [26]

    Alameldeen, Marco Guarnieri, Mark Silberstein, Oleksii Oleksenko, and Gu- ruraj Saileshwar

    Bo Fu, Leo Tenenbaum, David Adler, Assaf Klein, Arpit Gogia, Alaa R. Alameldeen, Marco Guarnieri, Mark Silberstein, Oleksii Oleksenko, and Gu- ruraj Saileshwar. 2025. AMuLeT: Automated Design-Time Testing of Secure Speculation Countermeasures. InProceedings of the 30th ACM Int...

    2025

  20. [27]

    Lukas Gerlach, Daniel Weber, Ruiyi Zhang, and Michael Schwarz. 2023. A Secu- rity RISC: Microarchitectural Attacks on Hardware RISC-V CPUs. InProceedings of the 44th IEEE Symposium on Security and Privacy (S&P). IEEE

    2023

  21. [28]

    Moein Ghaniyoun, Kristin Barber, Yinqian Zhang, and Radu Teodorescu. 2021. IntroSpectre: a pre-silicon framework for discovery and analysis of transient exe- cution vulnerabilities. InProceedings of the 48th Annual International Symposium on Computer Architecture (ISCA). IEEE

    2021

  22. [29]

    Morales, Jan Reineke, and Andrés Sánchez

    Marco Guarnieri, Boris Köpf, José F. Morales, Jan Reineke, and Andrés Sánchez. 2020.Spectector: Principled detection of speculative information flows. In Proceedings of the 41st IEEE Symposium on Security and Privacy (S&P). IEEE

    2020

  23. [30]

    Marco Guarnieri, Boris Köpf, Jan Reineke, and Pepe Vila. 2021. Hardware- software contracts for secure speculation. InProceedings of the 42nd IEEE Sym- posium on Security and Privacy (S&P). IEEE

    2021

  24. [31]

    Jana Hofmann, Emanuele Vannacci, Cédric Fournet, Boris Köpf, and Oleksii Oleksenko. 2023. Speculation at fault: modeling and testing microarchitectural leakage of CPU exceptions. InProceedings of the 32nd USENIX Security Symposium (USENIX Security). USENIX Association

    2023

  25. [32]

    Mulligan, Nikos Nikoleris, Gustavo Petri, and Caroline Trippel

    Yao Hsiao, Dominic P. Mulligan, Nikos Nikoleris, Gustavo Petri, and Caroline Trippel. 2021. Synthesizing Formal Models of Hardware from RTL for Efficient Verification of Memory Model Implementations. InProceedings of the 54th Annual IEEE/ACM International Symposium on Microarc...

    2021

  26. [33]

    Mulligan, Gustavo Petri, Christopher W

    Yao Hsiao, Nikos Nikoleris, Artem Khyzha, Dominic P. Mulligan, Gustavo Petri, Christopher W. Fletcher, and Caroline Trippel. 2024. RTL2M 𝜇PATH: Multi- 𝜇PATH Synthesis with Applications to Hardware Security Verification. InPro- ceedings of the 2024 57th IEEE/ACM International S...

    2024

  27. [34]

    Jaewon Hur, Suhwan Song, Sunwoo Kim, and Byoungyoung Lee. 2022. Spec- Doctor: Differential Fuzz Testing to Find Transient Execution Vulnerabilities. In Proceedings of the 29th ACM SIGSAC Conference on Computer and Communications Security (CCS). ACM

    2022

  28. [35]

    Kocher, J

    P. Kocher, J. Horn, A. Fogh, D. Genkin, D. Gruss, W. Haas, M. Hamburg, M. Lipp, S. Mangard, T. Prescher, M. Schwarz, and Y. Yarom. 2019. Spectre Attacks: Exploiting Speculative Execution. InProceedings of the 41st IEEE Symposium on Security and Privacy (S&P). IEEE

    2019

  29. [36]

    Fangfei Liu, Yuval Yarom, Qian Ge, Gernot Heiser, and Ruby B. Lee. 2015. Last- Level Cache Side-Channel Attacks are Practical. InProceedings of the 36th IEEE Symposium on Security and Privacy (S&P). IEEE

    2015

  30. [37]

    Giorgi Maisuradze and Christian Rossow. 2018. Ret2Spec: Speculative Execution Using Return Stack Buffers. InProceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (CCS). ACM

    2018

  31. [38]

    Gideon Mohr, Marco Guarnieri, and Jan Reineke. 2024. Synthesizing Hardware- Software Leakage Contracts for RISC-V Open-Source Processors. InProceedings of the 27th Design, Automation and Test in Europe Conference and Exhibition (DATE). ACM/IEEE

    2024

  32. [39]

    Hamed Nemati, Pablo Buiras, Andreas Lindner, Roberto Guanciale, and Swen Jacobs. 2020. Validation of Abstract Side-Channel Models for Computer Archi- tectures. InProceedings of the 32nd International Conference on Computer Aided Verification (CA V). Springer

    2020

  33. [40]

    Oleksii Oleksenko, Christof Fetzer, Boris Köpf, and Mark Silberstein. 2022. Revi- zor: Testing Black-Box CPUs against Speculation Contracts. InProceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS). ACM

    2022

  34. [41]

    Oleksii Oleksenko, Marco Guarnieri, Boris Köpf, and Mark Silberstein. 2023. Hide and Seek with Spectres: Efficient discovery of speculative information leaks with random testing. InProceedings of the 44th IEEE Symposium on Security and Privacy (S&P). IEEE

    2023

  35. [42]

    Marco Patrignani and Marco Guarnieri. 2021. Exorcising Spectres with Secure Compilers. InProceedings of the 28th ACM Conference on Computer and Commu- nications Security (CCS). ACM

    2021

  36. [43]

    Antoon Purnal, Marton Bognar, Frank Piessens, and Ingrid Verbauwhede. 2023. ShowTime: Amplifying Arbitrary CPU Timing Side Channels. InProceedings of the 18th ACM Asia Conference on Computer and Communications Security (ASIA CCS). ACM

    2023

  37. [44]

    Thomas Ristenpart, Eran Tromer, Hovav Shacham, and Stefan Savage. 2009. Hey, you, get off of my cloud: exploring information leakage in third-party compute clouds. InProceedings of the 16th ACM SIGSAC Conference on Computer and Communications Security (CCS). ACM

    2009

  38. [45]

    Michael Schwarz, Moritz Lipp, Daniel Moghimi, Jo Van Bulck, Julian Steck- lina, Thomas Prescher, and Daniel Gruss. 2019. ZombieLoad: Cross-Privilege- Boundary Data Sampling. InProceedings of the 26th ACM Conference on Computer and Communication Security (CCS). ACM

    2019

  39. [46]

    Julian Stecklina and Thomas Prescher. 2018. LazyFP: Leaking FPU Register State using Microarchitectural Side-Channels.CoRRabs/1806.07480 (2018)

    2018 arXiv

  40. [47]

    Qinhan Tan, Yuheng Yang, Thomas Bourgeat, Sharad Malik, and Mengjia Yan

  41. [48]

    Yukiyasu Tsunoo, Teruo Saito, Tomoyasu Suzaki, Maki Shigeri, and Hiroshi Miyauchi. 2003. Cryptanalysis of DES Implemented on Computers with Cache. InProceedings of the 5th International Workshop on Cryptographic Hardware and Embedded Systems (CHES). Springer

    2003

  42. [49]

    Stephan van Schaik, Alyssa Milburn, Sebastian Österlund, Pietro Frigo, Giorgi Maisuradze, Kaveh Razavi, Herbert Bos, and Cristiano Giuffrida. 2019. RIDL: Rogue In-flight Data Load. InProceedings of the 40th IEEE Symposium on Security and Privacy (S&P). IEEE

    2019

  43. [51]

    Patterson, and Krste Asanović

    Andrew Waterman, Yunsup Lee, David A. Patterson, and Krste Asanović. 2014. The RISC-V Instruction Set Manual, Volume I: User-Level ISA, Version 2.0. Tech- nical Report UCB/EECS-2014-54. EECS Department, University of California, Berkeley

    2014

  44. [52]

    Daniel Weber, Ahmad Ibrahim, Hamed Nemati, Michael Schwarz, and Christian Rossow. 2021. Osiris: Automated Discovery of Microarchitectural Side Channels. InProceedings of the 30th USENIX Security Symposium (USENIX Security). USENIX Association

    2021

  45. [53]

    Hans Winderix, Marton Bognar, Lesly-Ann Daniel, and Frank Piessens. 2024. Libra: Architectural Support For Principled, Secure And Efficient Balanced Exe- cution On High-End Processors. InProceedings of the 31st ACM Conference on Computer and Communications Security (CCS). ACM

    2024

  46. [54]

    Hans Winderix, Marton Bognar, Job Noorman, Lesly-Ann Daniel, and Frank Piessens. 2024. Architectural Mimicry: Innovative Instructions to Efficiently Address Control-Flow Leakage in Data-Oblivious Programs. InProceedings of the 43rd IEEE Symposium on Security and Privacy (S&P). IEEE

    2024

  47. [55]

    Yuval Yarom and Katrina Falkner. 2014. Flush+Reload: A High Resolution, Low Noise, L3 Cache Side-channel Attack. InProceedings of the 23rd USENIX Security Symposium (USENIX Security). USENIX Association

    2014

  48. [56]

    Yuval Yarom, Daniel Genkin, and Nadia Heninger. 2017. CacheBleed: a timing attack on OpenSSL constant-time RSA.J. Cryptogr. Eng.7, 2 (2017). Zilong Wang, Gideon Mohr, Klaus von Gleissenthall, Jan Reineke, and Marco Guarnieri A Proofs A.1 Proof of Proposition 1 Proposition 1.Le...

    2017

  49. [2025]

    In Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)

    RTL Verification for Secure Speculation Using Contract Shadow Logic. In Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS). ACM

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.