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

Adam Chlipala; Andres Erbsen; Stella Lau

REVIEW 3 major objections 4 minor 49 references

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

T0 review · 3 major / 4 minor · reviewed 2026-08-01 · deepseek-v4-flash

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

Pith's one-line read Granite claims that cycle-by-cycle timing of a verified pipelined RISC core provably depends only on the observables a hand-written ISA leakage contract declassifies, and that a constant-time Salsa20 binary running on the core leaks nothing

desk verdict A serious, machine-checked advance in RTL leakage verification; the real caveats are the unverified pretty-printer and the hand-chosen policy, not the refinement story. read the letter →

arxiv 2607.27480 v1 pith:5JXUTPKC submitted 2026-07-29 cs.CR

Stella Lau , Andres Erbsen , Adam Chlipala This is my paper · ORCID

classification cs.CR

keywords timingsidechannelsnoninterferenceleakagecontractsRTLverificationrefinementconstant-timeprogrammingRISC-Vformal

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

Granite argues that the timing side-channel problem for processors can be closed by a single, auditable, instruction-set-level leakage contract, provided the contract's nondeterminism is determinized rather than abstracted. The paper's central claim is that a pipelined RISC implementation—with speculation, precise interrupts, and MMIO—is functionally correct and non-leaking exactly when it is trace-equivalent to a cycle-accurate specification machine parameterized by three untrusted black boxes: a secret-independent driver, an unconstrained witness, and a leakage transformer. Composing this with a certified static analysis of constant-time code yields a machine-checked theorem that a Salsa20 binary's cycle-by-cycle MMIO observations are identical for any two secrets, with the ISA contract itself removed from the trusted computing base. A sympathetic reader should care because this is the first modular, foundational connection between ISA-level leakage contracts and wire-level cycle-accurate RTL—making timing leaks a proof obligation rather than an empirical hunt.

What carries the argument

The central device is leakage-aware refinement via determinism: a one-instruction-at-a-time ISA machine with a leakage function is lowered to a cycle-accurate Mealy machine and then determinized by existentially parameterizing it with three untrusted functions—a driver that resolves secret-independent choices (when to step, when to take an interrupt, when to issue I/O) from public data, a witness that supplies unspecified possibly-secret outputs, and a leakage transformer that maps declassified leakage events to adversary observations. The proof obligation is a single trace-equivalence statement between implementation and the parameterized spec machine, established by a cycle-by-cycle bisimu

What would settle it

Run the pretty-printed SystemVerilog on an FPGA or simulator with two secret inputs that agree on every declassified event (branch conditions, load/store addresses, multiplier zero flags, instruction bytes, and writes to interrupt-configuration CSRs) but differ in some other register or memory value, and check whether the cycle-by-cycle MMIO ready/valid traces diverge; any divergence would falsify the end-to-end noninterference theorem.

Watch

Extended reading notes

Core claim

On Granite's terms: correctness and confidentiality are not separate properties but two faces of one trace-equivalence fact. An implementation satisfies a leakage-aware ISA contract when there exist a leakage transformer, a secret-independent driver, and an unconstrained witness such that for every cycle count and every public/secret input pair, the implementation's output trace equals the trace of the deterministic cycle-accurate specification built from the trusted ISA machine and those parameters. The paper reports this proof for a four-stage pipelined RISC-V core with branch prediction, precise exceptions and interrupts, and a ready/valid MMIO interface, and then extends it through a Qua

Load-bearing premise

The hand-written leakage contract must list every architectural event that can influence cycle-level timing; a secret-dependent effect missing from the list would not be ruled out by the proof.

Editorial extensions

If this is right

Any timing difference visible at the digital I/O boundary of the verified core is a function only of the declassified leakage; unknown future timing attacks of the same class are ruled out without enumerating them.
The RTL implementation and the existential parameters are removed from the trusted computing base; only the cycle-level ISA contract, memory model, external-world model, the proof kernel, and the pretty-printer remain trusted.
The methodology composes with software-level constant-time proofs, so the hardware-software contract is an intermediate specification rather than a trust anchor.
The same ISA contract admits multiple microarchitectures (such as the four-stage pipelined core and a three-stage multicycle core) without changes to the contract.
Submodule contracts capture both correctness and leakage independently, allowing designers to swap implementations or reason about early-stage designs and defenses without redoing the top-level proof.

Reading between the lines

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

The driver/witness/leakage-transformer decomposition suggests a template for other declassification policies: any policy expressible as a public-trace function can be verified with the same shadow-core recipe, though policies that declassify richer data (for example, exponent values) would need a more informative shadow machine.
Because the guarantee is trace-equivalence against a cycle-accurate spec, the same machinery could in principle verify non-timing microarchitectural side channels by changing only the observation function—but power or EM observations would require a different observation boundary and likely a different leakage transformer, which the framework leaves unconstrained.
A practical negative test for transferability: apply the same contract to a different RISC-V core with a subtle secret-dependent stall not listed in the policy; the proof should fail to construct the shadow machine, providing evidence that the policy is incomplete.
The reliance on a deterministic HDL fragment and a single clock domain means multi-clock and asynchronous designs would require new machinery; one could probe whether the one-method-at-a-time semantics extends to synchronous clock-domain-crossing interfaces with handshake-based crossing points.

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.

Desk Editor's Note

read the letter

Granite is worth your time if you care about whether constant-time guarantees can be made to survive contact with real microarchitecture. The central move is to determinize the ISA-level specification with existential parameters — an untrusted secret-independent driver for resolution of nondeterminism and an untrusted witness for secret-dependent unspecified outputs — then prove trace equivalence between implementation and spec. The witness can depend on secrets because it only affects outputs the adversary is not allowed to observe. That sounds like a small trick, but it is the right one: it lets the proof go through without either underspecifying (allowing secret-dependent choice) or overspecifying (ruling out legitimately variable latencies).

The modularity story is also genuine. Submodules get their own leakage contracts, with a substitution principle, so the whole-processor proof goes through once. The case study — a four-stage pipelined RISC core with speculation, precise interrupts, and I/O, plus a Salsa20 binary through a certified static analysis — is exactly the kind of integration the field needs. I also give them credit for honesty: they report that the proof forced them to add CSR-write leakage to the contract. That is evidence the methodology catches policy omissions, not that the policy was rigged.

The weak spots are real but disclosed. The Quartz-to-SystemVerilog pretty-printer is in the TCB, so the synthesizable RTL claim is not machine-checked; and the abstract memory model is trusted, so data-dependent memory timing is out of scope. Those temper the "single Rocq theorem" slogan but don't undercut the contribution. The leakage policy is hand-written — the guarantee is relative to it — but the trace-equivalence proof does certify that the verified design has no timing dependence outside that policy. That is the best one can do without a formal theory of what the policy ought to be.

I'd send this to peer review. The artifacts need to be checked — the Rocq development is the one thing I couldn't inspect from the text — and the TCB discussion should be sharpened, but the methodology is coherent and the result is new. It deserves a serious referee.

Referee Report

3 major / 4 minor

Summary. The paper presents Granite, a methodology formalized in Rocq for verifying both functional correctness and nonleakage of processor RTL against ISA-level leakage contracts. The central construction is 'leakage-aware refinement via determinism': the authors lower a one-instruction-at-a-time ISA with a leakage function into a cycle-accurate deterministic specification machine parameterized by an untrusted secret-independent driver, an untrusted witness, and a leakage transformer. An implementation satisfies the contract if there exist instantiations of these parameters under which the implementation and specification traces are equivalent, thereby discharging both correctness and confidentiality as a single trace-equivalence obligation. The methodology is demonstrated on a four-stage pipelined RISC-V core with branch prediction, precise interrupts, MMIO, and a zero-skip multiplier, and composed with a certified static analysis to obtain a noninterference theorem for a Salsa20 binary. The authors are explicit that the Quartz-to-SystemVerilog pretty-printer and the abstract memory specification remain in the trusted computing base.

Significance. If the claims are accepted at face value, this is a substantial advance: it is the first modular, machine-checked connection between ISA-level leakage contracts and cycle-level microarchitectural behavior, supporting nondeterminism without the usual refinement-based leak-explanation problem. The case study is nontrivial—it includes speculation, precise interrupts, and I/O—and the paper's explicit TCB accounting is a strength. The modular substitution principle and the reuse of functional-correctness proof structure for confidentiality are valuable contributions. However, the headline 'foundational verification of hardware-software leakage contracts' is conditional on two trusted components: the Quartz-to-SystemVerilog pretty-printer and the abstract memory model. The policy-completeness concern raised in the stress-test note is real but less decisive: the machine-checked trace-equivalence proof does certify nonleakage relative to the stated declassification policy, but the policy itself is hand-written and was found incomplete during the authors' own verification. Overall, the central derivation appears sound, but the scope of the claims needs significant tightening.

major comments (3)

[§7.2 and Abstract] The end-to-end theorem is proved for the Quartz/Gallina model, not for the generated SystemVerilog: the 200-line syntax-mapping function is explicitly in the TCB. Therefore the abstract's claim of 'a single Rocq theorem about cycle-by-cycle confidentiality of a hardware-and-software cryptographic implementation—eliminating every intermediate specification' is technically true only up to the pretty-printer. The synthesizable RTL artifact is not covered by the machine-checked theorem. This is disclosed, but it is load-bearing for the paper's 'synthesizable RTL' and 'foundational' claims. The authors should either verify the translation (e.g., by connecting to an RTL equivalence checker) or explicitly scope the main theorem to the Quartz model and present the RTL claim as conditional on translation correctness.
[§5.2.2 and §8.1] The abstract memory specification is trusted: the end-to-end noninterference theorem assumes that memory response time depends only on public information (addresses). No concrete memory implementation is verified against this specification. Consequently, a memory with secret-dependent latency—e.g., DRAM row conflicts or refresh timing that depends on stored values—would invalidate the practical guarantee while leaving every Rocq statement true. The paper should either verify a concrete memory against the abstract spec or state prominently in the abstract/introduction that the guarantee excludes memory implementations not satisfying the abstract memory model.
[§3.2 and §6] The leakage contract's declassification policy is hand-written and not proven complete. The authors' own experience in §6—the proof could not be completed without adding leakage of writes to mie/mtvec—demonstrates that the policy can omit timing-relevant architectural events. Thus the abstract's claim of 'conclusively rules out information leakage through known and unknown timing side channels' overstates the result: it rules out channels expressible in the contract's declassification events, but not channels omitted by the policy. To support the stronger claim, the paper would need a policy-completeness argument (e.g., a formal enumeration of all microarchitectural events that can influence cycle-level timing, mapped to leak events), or the claims should be weakened to 'no leakage beyond the declassified events specified by the contract.'

minor comments (4)

[Figure 2] The starred nodes and the 'Focus' label in the proof-structure diagram are not explained; please clarify what the asterisks indicate or remove them.
[Definitions 1 and 2] The two definitions use different step counts (n for the ISA trace, m for the microarchitectural trace) without explicit comment. State clearly that these are independent and that the quantifier order matters.
[Figure 8] The Beq-Spin rule uses 'interruptsDisabled(st)' but there is no corresponding discussion of how interrupts are modeled in the static analysis; clarify whether interrupts are assumed disabled for the entire analyzed program or only for the spin loop.
[References] The text refers to 'RISCV-COQ' in §3.2; please ensure that the citations [8,15] are presented consistently with their actual titles and venues.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the central security chain is a machine-checked trace-equivalence argument whose existential parameters are discharged by shadow-machine constructions, and the disclosed TCB gaps are soundness conditions rather than circular reductions.

full rationale

Granite's load-bearing derivation is Definition 2 (trace equivalence between the implementation and a determinized Cycle-ISA machine under existential driver/witness/leakage-transformer parameters) and Theorem 2 (noninterference for statically safe programs). Nothing in this chain reduces to its own conclusion: the existential parameters are discharged in §4.5 and §6 by explicitly constructed shadow copies, and the simulation invariants—public pipeline state, leakage-equivalence of multiplier/memory request histories, visibility-point/driver synchronization—are proved by single-cycle induction rather than assumed. The security property is relational (equality of observations for all pairs of secrets), and the shadow machine is a proof device, not a fitted value; the theorem does not become true by definition. The self-cited lineage ([9], [13], [15], [28]) contributes techniques and definitions that are re-proved or independently machine-checked; the 'leakage transformer' used in Definition 2 is formally defined there and its existence is proved, not imported as an unverified uniqueness claim. The disclosed trust gaps—the 200-line Quartz-to-SystemVerilog pretty-printer (§7.2) and the trusted abstract memory spec (§5.2.2)—are honest limitations on the end-to-end RTL statement, but they are TCB/soundness concerns that could invalidate practical guarantees if the translation or memory model were wrong; they do not make any proved theorem equivalent to an input. The §6 CSR-leakage clause that 'the proof could not be completed without' is evidence of a genuine policy gap discovered by verification, not of fitting the conclusion into the assumptions. Overall, the derivation is self-contained and no circular step is present.

Assumptions & free parameters 2 free parameters · 6 assumptions · 0 invented entities

All guarantees are conditional on the Rocq kernel, the hand-authored Cycle-ISA contract, the trusted abstract memory spec, the unverified Quartz-to-SystemVerilog pretty-printer, the leakage/declassification policy, and the stated threat model. No new physical entities are posited; the driver, witness, and shadow core are proof artifacts rather than physical mechanisms. The processor and static-analysis proofs are intended to be machine-checked, but the artifact is not inspectable in this submission.

free parameters (2)

Leakage contract declassification policy = branch conds; load/store addrs; Mul zero bits; instr bytes; mie/mtvec CSR writes
Hand-chosen by the authors; defines what counts as public for the nonleakage theorem. The mie/mtvec clause was added only after the proof failed (§6), so the guarantee is relative to this policy.
Static-analysis symbolic abstraction = Public n / Secret tags; program memory public, data memory secret
The analysis is sound but not complete and is validated on one Salsa20 binary; the end-to-end theorem inherits the adequacy of this abstraction for the case study.

assumptions (6)

domain assumption Rocq kernel soundness and equivalence of the shallow Gallina/Quartz fragment to the intended circuit semantics
The proof chain assumes the Rocq kernel. The Quartz-to-SystemVerilog pretty-printer is not verified against formal SystemVerilog semantics and is left in the TCB (§7.2, §8.1).
domain assumption The abstract memory spec models the real memory subsystem
Stated in §5.2.2: 'This work does not tackle verifying memory hierarchies, and so, the spec of memory is trusted.' A memory model that omits secret-dependent timing would break the end-to-end claim.
domain assumption Threat model: adversary observes only cycle-by-cycle digital I/O; power, EM, within-cycle timing, and physical access are excluded
Stated in §3.2 and Limitations. The 'rule out timing side channels' claim holds only within this observational model.
domain assumption The hand-written leakage contract exactly characterizes which architectural events can influence cycle timing
If a secret-dependent effect is missing from the policy, the theorem does not rule it out. §6 shows the policy had to be extended with CSR-write leakage before the proof could be completed.
domain assumption Deterministic HDL fragment, single clock domain, single hardware thread, read-only instruction memory
Limitations: proofs rely on determinism of the HDL fragment; multi-clock, multicore, and self-modifying-code behaviors are out of scope.
domain assumption The Quartz-to-SystemVerilog syntax-mapping function is semantically correct
Explicit TCB entry in §7.2 and §8.1: the 200-line pretty-printer is not verified against a formal SystemVerilog semantics.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Granite: A Modular Methodology for Foundational Verification of Hardware-Software Leakage Contracts." pith.science (2026). https://pith.science/paper/5JXUTPKC

@misc{pith2026260727480,
  author       = {Pith},
  title        = {Pith review of: Granite: A Modular Methodology for Foundational Verification of Hardware-Software Leakage Contracts},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/5JXUTPKC}},
  note         = {Machine review of arXiv:2607.27480}
}

read the original 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.

Figures

Figures reproduced from arXiv: 2607.27480 by the authors.

**Figure 2.** Layered, end-to-end proof structure. A program is deemed constant-time by a static analysis proven sound against a software-style ISA contract. Observations are the timing of externally observable behaviours (e.g. MMIO output). An equivalence proof lowers the software-style ISA contract to a hardware-style ISA contract that uses hardware-optimized, combinational decode and execute logic shared across instructions… view at source ↗

**Figure 3.** Implementation (left) and specification (right) of a pipelined, zero-skip multiplier. Functional cor [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗

Figures from the paper (5 more)

**Figure 4.** Figure 4: An implementation satisfies a leakage-aware ISA contract—and hence is both functionally correct [PITH_FULL_IMAGE:figures/full_fig_p011_4.png]

**Figure 5.** Figure 5: The Cycle−ISA state machine. The driver directs the machine to take steps and decides when an interrupt is taken. The machine outputs declassified leakage and drives wires on the MMIO interface. The wire-level interface and functional correctness. A trusted layer bridg…

**Figure 6.** Figure 6: The freer-monad encoding of modular hardware in Rocq. For verification convenience (elided here), [PITH_FULL_IMAGE:figures/full_fig_p017_6.png]

**Figure 7.** Figure 7: Zero-skip multiplier specification in Rocq. NB: simplified to remove value/action method distinction. [PITH_FULL_IMAGE:figures/full_fig_p018_7.png]

**Figure 8.** Figure 8: Symbolic state and representative Beq rules of the constant-time analysis. Proof sketch. Soundness of the static analysis gives IsConstantTimeISA(prog), so the ISA leakage trace is secret-independent; since the leakage transformer reads only public data and that trace…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

49 extracted references · 5 canonical work pages

[1]

Sam Ainsworth. 2021. GhostMinion: A Strictness-Ordered Cache System for Spectre Mitigation. InMICRO-54: 54th Annual IEEE/ACM International Symposium on Microarchitecture(Virtual Event, Greece)(MICRO ’21). Association for Computing Machinery, New York, NY, USA, 592–606

2021
[2]

Sam Ainsworth and Timothy M. Jones. 2020. MuonTrap: Preventing Cross-Domain Spectre-Like Attacks by Capturing Speculative State. In2020 ACM/IEEE 47th Annual International Symposium on Computer Architecture (ISCA). 132–144. https://doi.org/10.1109/ISCA45697.2020.00022

arXiv 2020
[3]

Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, and Swarn Priya. 2022. Enforcing fine-grained constant-time policies. InProceedings of the 2022 ACM SIGSAC conference on computer and communications security. 83–96

2022
[4]

Anish Athalye, Adam Belay, M Frans Kaashoek, Robert Morris, and Nickolai Zeldovich. 2019. Notary: A device for secure transaction approval. InProceedings of the 27th ACM Symposium on Operating Systems Principles. 97–113

2019
[5]

Anish Athalye, Henry Corrigan-Gibbs, Frans Kaashoek, Joseph Tassarotti, and Nickolai Zeldovich. 2024. Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level Implementation. InProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles(Austin, TX, USA)(SOSP ’24). Association for Computing M...

arXiv 2024
[6]

Anish Athalye, M Frans Kaashoek, and Nickolai Zeldovich. 2022. Verifying Hardware Security Modules with Information-Preserving Refinement. In16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22). 503–519

2022
[7]

Bluespec System Verilog: Efficient, Correct RTL from High Level Specifications

Bluespec 2004. Bluespec System Verilog: Efficient, Correct RTL from High Level Specifications. InProceedings of the Second ACM/IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE ’04). IEEE Computer Society, USA, 69–70. https://doi.org/10.1109/MEMCOD.2004.1459818

arXiv 2004
[8]

Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Pratap Singh, Andy Wright, and Adam Chlipala. 2023. Flexible Instruction-Set Semantics via Abstract Monads (Experience Report).Proc. ACM Program. Lang.7, ICFP, Article 192 (Aug. 2023), 17 pages. https://doi.org/10.1145/3607833

doi:10.1145/3607833 2023

Show all 49 references

[9]

Thomas Bourgeat, Jiazheng Liu, Adam Chlipala, and Arvind. 2025. Making Concurrent Hardware Verification Sequential.Proc. ACM Program. Lang.9, PLDI, Article 228 (June 2025), 25 pages. https://doi.org/10.1145/3729331

2025 doi
[11]

Gleissenthall, Dean Tullsen, Deian Stefan, Tamara Rezk, and Gilles Barthe

Sunjay Cauligi, Craig Disselkoen, Klaus v. Gleissenthall, Dean Tullsen, Deian Stefan, Tamara Rezk, and Gilles Barthe
[12]

Joonwon Choi, Jaewoo Kim, and Jeehoon Kang. 2025. Revamping Verilog Semantics for Foundational Verification. Proc. ACM Program. Lang.9, OOPSLA2, Article 306 (Oct. 2025), 28 pages. https://doi.org/10.1145/3763084

2025 doi
[13]

Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind. 2017. Kami: a platform for high-level parametric hardware specification and its modular verification.Proceedings of the ACM on Programming Languages1, ICFP (2017), 1–30

2017
[14]

Rutvik Choudhary, Jiyong Yu, Christopher Fletcher, and Adam Morrison. 2021. Speculative Privacy Tracking (SPT): Leaking Information From Speculative Execution Without Compromising Privacy. InMICRO-54: 54th Annual IEEE/ACM International Symposium on Microarchitecture(Virtual Ev...

2021
[15]

Owen Conoly, Andres Erbsen, and Adam Chlipala. 2025. Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers.Proc. ACM Program. Lang.9, PLDI, Article 215 (June 2025), 24 pages. https://doi.org/10.1145/3729318

2025 doi
[16]

Arthur Correnson, Haoyi Zeng, and Jana Hofmann. 2026. A Deductive System for Contract Satisfaction Proofs.Proc. ACM Program. Lang.10, PLDI, Article 173 (June 2026), 25 pages. https://doi.org/10.1145/3808251

2026 doi
[17]

David Costanzo, Zhong Shao, and Ronghui Gu. 2016. End-to-End Verification of Information-Flow Security for C and Assembly Programs. InProceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation(Santa Barbara, CA, USA)(PLDI ’16). Association...

2016
[18]

Lesly-Ann Daniel, Marton Bognar, Job Noorman, Sébastien Bardin, Tamara Rezk, and Frank Piessens. 2023. ProSpeCT: Provably Secure Speculation for the Constant-Time Policy. In32nd USENIX Security Symposium (USENIX Security 23). 7161–7178. Granite: A Modular Methodology for Found...

2023
[19]

Lucas Deutschmann, Johannes Müller, Mohammad Rahmani Fadiheh, Dominik Stoffel, and Wolfgang Kunz. 2024. A Scalable Formal Verification Methodology for Data-Oblivious Hardware.IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems43, 9 (2024), 2551–2564. ...

2024
[20]

Andres Erbsen, Samuel Gruetter, Joonwon Choi, Clark Wood, and Adam Chlipala. 2021. Integration verification across software and hardware for a simple embedded system. InProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementati...

2021
[21]

Mohammad Rahmani Fadiheh, Alex Wezel, Johannes Müller, Jörg Bormann, Sayak Ray, Jason M Fung, Subhasish Mitra, Dominik Stoffel, and Wolfgang Kunz. 2022. An exhaustive approach to detecting transient execution side channels in RTL designs of processors.IEEE Trans. Comput.72, 1 ...

2022
[22]

Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, and Bryan Parno. 2017. Komodo: Using Verification to Disentangle Secure-Enclave Hardware from Software. InProceedings of the 26th Symposium on Operating Systems Principles(Shanghai, China)(SOSP ’17). Association for Computin...

2017
[23]

Myers, and G

Andrew Ferraiuolo, Mark Zhao, Andrew C. Myers, and G. Edward Suh. 2018. HyperFlow: A Processor Architecture for Nonmalleable, Timing-Safe Information Flow Security. InProceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security(Toronto, Canada)(CCS ’18...

2018
[24]

Marco Guarnieri, Boris Köpf, Jan Reineke, and Pepe Vila. 2021. Hardware-software contracts for secure speculation. In2021 IEEE Symposium on Security and Privacy (SP). IEEE, 1868–1883

2021
[25]

Khasawneh, Esmaeil Mohammadian Koruyeh, Chengyu Song, Dmitry Evtyushkin, Dmitry Ponomarev, and Nael Abu-Ghazaleh

Khaled N. Khasawneh, Esmaeil Mohammadian Koruyeh, Chengyu Song, Dmitry Evtyushkin, Dmitry Ponomarev, and Nael Abu-Ghazaleh. 2019. SafeSpec: Banishing the Spectre of a Meltdown with Leakage-Free Speculation. In2019 56th ACM/IEEE Design Automation Conference (DAC). 1–6

2019
[26]

Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2010. seL4: formal verification of an operating-system kernel.Commun. A...

2010
[27]

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. In2019 IEEE Symposium on Security and Privacy (SP). 1–19. https://doi.org/10.1109/SP.2019.00002

2019
[28]

Stella Lau, Thomas Bourgeat, Clément Pit-Claudel, and Adam Chlipala. 2024. Specification and Verification of Strong Timing Isolation of Hardware Enclaves. InProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security(Salt Lake City, UT, USA)(CCS ’2...

2024
[29]

Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Anders Fogh, Jann Horn, Stefan Mangard, Paul Kocher, Daniel Genkin, Yuval Yarom, and Mike Hamburg. 2018. Meltdown: Reading Kernel Memory from User Space. In27th USENIX Security Symposium (USENIX Security...

2018
[30]

Nicholas Mosier, Hanna Lachnitt, Hamed Nemati, and Caroline Trippel. 2022. Axiomatic Hardware-Software Contracts for Security. InProceedings of the 49th Annual International Symposium on Computer Architecture(New York, New York) (ISCA ’22). Association for Computing Machinery,...

2022
[31]

Mitchell, and Caroline Trippel

Nicholas Mosier, Hamed Nemati, John C. Mitchell, and Caroline Trippel. 2024. Serberus: Protecting Cryptographic Code from Spectres at Compile-Time. In2024 IEEE Symposium on Security and Privacy (SP). 4200–4219. https: //doi.org/10.1109/SP54263.2024.00048

2024
[32]

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

2022
[33]

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. In2023 IEEE Symposium on Security and Privacy (SP). IEEE, 1737–1752

2023
[34]

O’Neill, M.R

K.R. O’Neill, M.R. Clarkson, and S. Chong. 2006. Information-flow security for interactive programs. In19th IEEE Computer Security Foundations Workshop (CSFW’06). 12 pp.–201. https://doi.org/10.1109/CSFW.2006.16

2006 doi
[35]

Wintersteiger, and Santiago Zanella-Beguelin

Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananan- dro, Aseem Rastogi, Nikhil Swamy, Christoph M. Winters...

2020
[36]

Christos Sakalis, Stefanos Kaxiras, Alberto Ros, Alexandra Jimborean, and Magnus Själander. 2019. Efficient Invisible Speculative Execution through Selective Delay and Value Prediction. In2019 ACM/IEEE 46th Annual International Symposium on Computer Architecture (ISCA). 723–735

2019
[37]

David Shah, Eddie Hung, Clifford Wolf, Serge Bazanski, Dan Gisselquist, and Miodrag Milanović. 2019. Yosys+nextpnr: an Open Source Framework from Verilog to Bitstream for Commercial FPGAs. arXiv:1903.10407 [cs.DC] https: //arxiv.org/abs/1903.10407

2019 arXiv
[38]

Jeffrey X Su, David L Dill, and Clark W Barrett. 1996. Automatic generation of invariants in processor verification. In International Conference on Formal Methods in Computer-Aided Design. Springer, 377–388

1996
[39]

Qinhan Tan, Yuheng Yang, Thomas Bourgeat, Sharad Malik, and Mengjia Yan. 2025. RTL Verification for Secure Spec- ulation Using Contract Shadow Logic. InProceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems...

2025
[40]

Caroline Trippel, Daniel Lustig, and Margaret Martonosi. 2018. Checkmate: Automated synthesis of hardware exploits and security litmus tests. In2018 51st Annual IEEE/ACM International Symposium on Microarchitecture (MICRO). IEEE, 947–960

2018
[41]

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 2023 ACM SIGSAC Conference on Computer and Communications S...

2023
[42]

2015.The risc-v instruction set manual volume 2: Privileged architecture version 1.7

Andrew Waterman, Yunsup Lee, Rimas Avizienis, David A Patterson, and Krste Asanovic. 2015.The risc-v instruction set manual volume 2: Privileged architecture version 1.7. Technical Report

2015
[43]

Robin Webbers, Robert Schenck, Wind Wong, Kristina Sojakova, and Klaus von Gleissenthall. 2026. Pantomime: Constructive Leakage Proofs via Simulation.Proc. ACM Program. Lang.10, PLDI, Article 262 (June 2026), 26 pages. https://doi.org/10.1145/3808340

2026 doi
[44]

Mengjia Yan, Jiho Choi, Dimitrios Skarlatos, Adam Morrison, Christopher Fletcher, and Josep Torrellas. 2018. InvisiSpec: Making Speculative Execution Invisible in the Cache Hierarchy. In2018 51st Annual IEEE/ACM International Symposium on Microarchitecture (MICRO). 428–441. ht...

2018
[45]

Yuheng Yang, Thomas Bourgeat, Stella Lau, and Mengjia Yan. 2023. Pensieve: Microarchitectural Modeling for Security Evaluation. InProceedings of the 50th Annual International Symposium on Computer Architecture(Orlando, FL, USA)(ISCA ’23). Association for Computing Machinery, N...

2023
[46]

Fletcher

Jiyong Yu, Mengjia Yan, Artem Khyzha, Adam Morrison, Josep Torrellas, and Christopher W. Fletcher. 2019. Speculative Taint Tracking (STT): A Comprehensive Protection for Speculatively Accessed Data. InProceedings of the 52nd Annual IEEE/ACM International Symposium on Microarch...

2019
[47]

Myers, and G

Drew Zagieboylo, Charles Sherk, Andrew C. Myers, and G. Edward Suh. 2023. SpecVerilog: Adapting Information Flow Control for Secure Speculation. InProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security(Copenhagen, Denmark)(CCS ’23). Association f...

2023
[48]

Edward Suh, and Andrew C

Danfeng Zhang, Yao Wang, G. Edward Suh, and Andrew C. Myers. 2015. A Hardware Design Language for Timing- Sensitive Information-Flow Security. InProceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems(Istan...

2015
[49]

Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. 2017. HACL*: A Verified Modern Cryptographic Library. InProceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security(Dallas, Texas, USA)(CCS ’17). Association ...

2017
[2020]

InProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation(London, UK)(PLDI 2020)

Constant-time foundations for the new Spectre era. InProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation(London, UK)(PLDI 2020). Association for Computing Machinery, New York, NY, USA, 913–926. https://doi.org/10.1145/3385412.3385970

2020

Pith tools

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

[1] [1]

Sam Ainsworth. 2021. GhostMinion: A Strictness-Ordered Cache System for Spectre Mitigation. InMICRO-54: 54th Annual IEEE/ACM International Symposium on Microarchitecture(Virtual Event, Greece)(MICRO ’21). Association for Computing Machinery, New York, NY, USA, 592–606

2021

[2] [2]

Sam Ainsworth and Timothy M. Jones. 2020. MuonTrap: Preventing Cross-Domain Spectre-Like Attacks by Capturing Speculative State. In2020 ACM/IEEE 47th Annual International Symposium on Computer Architecture (ISCA). 132–144. https://doi.org/10.1109/ISCA45697.2020.00022

arXiv 2020

[3] [3]

Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, and Swarn Priya. 2022. Enforcing fine-grained constant-time policies. InProceedings of the 2022 ACM SIGSAC conference on computer and communications security. 83–96

2022

[4] [4]

Anish Athalye, Adam Belay, M Frans Kaashoek, Robert Morris, and Nickolai Zeldovich. 2019. Notary: A device for secure transaction approval. InProceedings of the 27th ACM Symposium on Operating Systems Principles. 97–113

2019

[5] [5]

Anish Athalye, Henry Corrigan-Gibbs, Frans Kaashoek, Joseph Tassarotti, and Nickolai Zeldovich. 2024. Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level Implementation. InProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles(Austin, TX, USA)(SOSP ’24). Association for Computing M...

arXiv 2024

[6] [6]

Anish Athalye, M Frans Kaashoek, and Nickolai Zeldovich. 2022. Verifying Hardware Security Modules with Information-Preserving Refinement. In16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22). 503–519

2022

[7] [7]

Bluespec System Verilog: Efficient, Correct RTL from High Level Specifications

Bluespec 2004. Bluespec System Verilog: Efficient, Correct RTL from High Level Specifications. InProceedings of the Second ACM/IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE ’04). IEEE Computer Society, USA, 69–70. https://doi.org/10.1109/MEMCOD.2004.1459818

arXiv 2004

[8] [8]

Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Pratap Singh, Andy Wright, and Adam Chlipala. 2023. Flexible Instruction-Set Semantics via Abstract Monads (Experience Report).Proc. ACM Program. Lang.7, ICFP, Article 192 (Aug. 2023), 17 pages. https://doi.org/10.1145/3607833

doi:10.1145/3607833 2023