arxiv: 2604.09165 · v1 · submitted 2026-04-10 · 💻 cs.PL · cs.CR· cs.LO

Recognition: unknown

A Deductive System for Contract Satisfaction Proofs

Arthur Correnson , Haoyi Zeng , Jana Hofmann

Authors on Pith no claims yet

Pith reviewed 2026-05-10 17:09 UTC · model grok-4.3

classification 💻 cs.PL cs.CRcs.LO

keywords contract satisfactionrelative trace equalityrelative bisimulationdeductive proof systemhardware-software contractsside-channel verificationcoinductive proofsinteractive theorem proving

0 comments

The pith

A deductive proof system for relative trace equality enables modular interactive proofs that CPUs satisfy hardware-software leakage contracts.

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

The paper shows that contract satisfaction reduces to the problem of relative trace equality between a CPU and an abstract contract specification. It introduces relative bisimulation as the associated proof technique and builds a dedicated deductive system around it. The system is proved sound and complete, and it supports breaking proofs into independent modules while adding dedicated rules that exploit symmetries and transitivity to keep reasoning short. A reader cares because this gives a structured, human-guided alternative to exhaustive search methods when verifying that high-level code is protected against side-channel leakage.

Core claim

Contract satisfaction is an instance of relative trace equality, and relative bisimulation provides a practical proof principle for it. The authors construct a deductive proof system that is sound and complete for relative trace equality, permits modular and incremental development of proofs, and contains additional reasoning principles that simplify arguments by using symmetries and transitivity. The system has been formalized and successfully applied to two non-trivial contract satisfaction examples.

What carries the argument

The deductive proof system for relative trace equality, built on relative bisimulation and equipped with modular composition rules plus symmetry and transitivity principles.

If this is right

Proofs can be split into independent sub-proofs that are developed and maintained separately.
Interactive theorem provers become a viable alternative to model-checking approaches for contract verification.
Symmetries in leakage behavior can be used directly to shorten proofs rather than being rediscovered each time.
Completeness guarantees that any valid relative trace equality can eventually be established within the system.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same modular coinductive style could be reused for other infinite-trace properties of hardware abstractions beyond leakage contracts.
The symmetry and transitivity rules might transfer to verification tasks involving equivalent execution behaviors in compilers or operating systems.
Because the system is formalized, it opens the possibility of certified proof scripts that can be checked by independent tools.

Load-bearing premise

That contract satisfaction for real CPUs reduces exactly to relative trace equality and that relative bisimulation plus the supplied symmetry and transitivity rules suffice to finish the proofs without extra ad-hoc reasoning.

What would settle it

A concrete contract satisfaction instance that is true under the definition of relative trace equality yet cannot be proved inside the deductive system even after exhaustive use of its modular, symmetry, and transitivity rules.

Figures

Figures reproduced from arXiv: 2604.09165 by Arthur Correnson, Haoyi Zeng, Jana Hofmann.

**Figure 2.** Figure 2: Hardware semantics with a branch predictor [PITH_FULL_IMAGE:figures/full_fig_p014_2.png] view at source ↗

**Figure 3.** Figure 3: Always-mispredict contract. decision was correct. Our semantics does not allow nested speculation (this is further discussed in Section 6). Always-Mispredict Contract. We adapt the always-mispredict technique described in Section 2.3 to our example with the contract given in [PITH_FULL_IMAGE:figures/full_fig_p014_3.png] view at source ↗

**Figure 4.** Figure 4: Vanilla architectural semantics. Load (𝜎, load 𝑥1, 𝑥2) ⇒isa 𝜎 ′ (𝜎, 𝑐, load 𝑥1, 𝑥2) ⇒ c H (𝜎 ′ , 𝑎(𝑥2)::𝑐) Other (𝜎,𝑖) ⇒isa 𝜎 ′ (𝜎, 𝑐,𝑖) ⇒ c H (𝜎 ′ , 𝑐) [PITH_FULL_IMAGE:figures/full_fig_p026_4.png] view at source ↗

**Figure 6.** Figure 6: Hardware semantics with out-of-order execution. [PITH_FULL_IMAGE:figures/full_fig_p026_6.png] view at source ↗

**Figure 7.** Figure 7: Sequential contract. the combination of the predicate and the scheduling decision can result in the execution getting stuck. In our formalization, we only consider valid schedulers — that is, ones that return delay only when the hardware state is delayable, but not necessarily every time it is. Sequential Contract. The out-of-order execution can be abstracted away with a leakage contract that follows a sim… view at source ↗

read the original abstract

Hardware-software contracts are abstract specifications of a CPU's leakage behavior. They enable verifying the security of high-level programs against side-channel attacks without having to explicitly reason about the microarchitectural details of the CPU. Using the abstraction powers of a contract requires proving that the targeted CPU satisfies the contract in the sense that the contract over-approximates the CPU's leakage. Besides pen-and-paper reasoning, proving contract satisfaction has been approached mostly from the model-checking perspective, with approaches based on a (semi-)automated search for the necessary invariants. As an alternative, this paper explores how such proofs can be conducted in interactive proof assistants. We start by observing that contract satisfaction is an instance of a more general problem we call relative trace equality, and we introduce relative bisimulation as an associated proof technique. Leveraging recent advances in the field of coinductive proofs, we develop a deductive proof system for relative trace equality. Our system is provably sound and complete, and it enables a modular and incremental proof style. It also features several reasoning principles to simplify proofs by exploiting symmetries and transitivity properties. We formalized our deductive system in the Rocq proof assistant and applied it to two challenging contract satisfaction proofs.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a Rocq-formalized deductive system for relative trace equality via relative bisimulation, offering a modular alternative to model checking for hardware contract proofs, but the two examples need to show they run entirely inside the rules.

read the letter

The core contribution is a deductive system for relative trace equality, built around relative bisimulation, that is claimed sound and complete and has been mechanized in Rocq. It targets proofs that a CPU's leakage behavior satisfies a given hardware-software contract, replacing the usual search for invariants with structured coinductive reasoning plus rules for symmetries and transitivity. That is genuinely new in this corner of the literature, and the formalization plus the modular incremental style are the parts that actually move the needle. The authors also applied the system to two non-trivial contract satisfaction cases, which is concrete evidence they tried to make it work on realistic examples rather than just stating the rules. The formalization itself counts as reproducible work and should be taken at face value unless the Rocq development has gaps. The main soft spot is still the examples. The abstract says the system was used on two challenging proofs, but gives no indication whether those proofs stayed strictly inside the listed reasoning principles or needed extra state invariants, custom coinductive hypotheses, or ad-hoc lemmas that fall outside the deductive system. If the latter is true, the practical advantage over model checking shrinks for real CPUs. The reduction from contract satisfaction to relative trace equality also looks clean on paper but will need to hold up when the contracts get more detailed. This is worth sending to referees who work on coinductive proofs or side-channel verification in proof assistants. They can check the Rocq scripts and ask for the example derivations to be spelled out. I would bring it to a reading group focused on formal methods for security, but I would not cite it in my own work unless the examples turn out to be fully self-contained.

Referee Report

2 major / 0 minor

Summary. The paper develops a deductive proof system for relative trace equality (an instance of contract satisfaction for CPU leakage), based on relative bisimulation. It claims the system is sound and complete, formalized in Rocq, supports modular/incremental proofs, and includes rules exploiting symmetries and transitivity; the system is applied to two challenging contract satisfaction proofs as an alternative to model-checking approaches.

Significance. If the Rocq formalization is gap-free and the two examples confirm that proofs remain strictly inside the deductive system (using only the listed rules without external invariants or ad-hoc lemmas), the work provides a valuable machine-checked foundation for interactive verification of hardware-software contracts. The emphasis on modularity and the coinductive advances leveraged are strengths that could improve reliability over search-based methods for side-channel security proofs.

major comments (2)

The central claim that the deductive system enables modular contract-satisfaction proofs for real CPUs depends on the two Rocq examples using only the provided symmetries/transitivity rules and relative bisimulation without additional state invariants or external lemmas. The manuscript must include excerpts or proof outlines from the examples section showing this explicitly, as the abstract provides no such detail and the reduction from contract satisfaction to relative trace equality is assumed without further justification.
§ on formalization and completeness: while soundness and completeness are stated to be machine-checked in Rocq, the paper should reference the specific theorems or files establishing completeness for relative trace equality (beyond the abstract claim), to allow assessment of whether the system is sufficiently complete for the challenging examples without gaps.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the thoughtful and constructive review. The comments highlight important points for improving clarity and verifiability. We address each major comment below and will incorporate revisions to strengthen the manuscript.

read point-by-point responses

Referee: The central claim that the deductive system enables modular contract-satisfaction proofs for real CPUs depends on the two Rocq examples using only the provided symmetries/transitivity rules and relative bisimulation without additional state invariants or external lemmas. The manuscript must include excerpts or proof outlines from the examples section showing this explicitly, as the abstract provides no such detail and the reduction from contract satisfaction to relative trace equality is assumed without further justification.

Authors: We agree that explicit demonstration from the examples is essential to substantiate the modularity claim. In the revised manuscript, we will expand the examples section with proof outlines and selected excerpts from the Rocq developments. These will explicitly show that the two contract satisfaction proofs are carried out using only the deductive rules, relative bisimulation, symmetry, and transitivity principles, without external state invariants or ad-hoc lemmas. We will also add a concise justification of the reduction from contract satisfaction to relative trace equality in the introduction or a dedicated preliminaries subsection. revision: yes
Referee: § on formalization and completeness: while soundness and completeness are stated to be machine-checked in Rocq, the paper should reference the specific theorems or files establishing completeness for relative trace equality (beyond the abstract claim), to allow assessment of whether the system is sufficiently complete for the challenging examples without gaps.

Authors: We acknowledge the value of precise references for independent assessment. The revised manuscript will include explicit citations to the relevant Rocq theorems (in particular, the machine-checked completeness theorem for relative trace equality) together with the corresponding files and modules in the formalization. This will allow readers to locate the proofs and evaluate their applicability to the examples. revision: yes

Circularity Check

0 steps flagged

No circularity: deductive system derived from explicit definitions of relative trace equality with independent soundness proof in Rocq.

full rationale

The paper begins by defining relative trace equality as the target relation and relative bisimulation as the associated proof technique. It then constructs a deductive proof system whose rules are justified directly from these definitions, with soundness and completeness established via a separate formalization in the Rocq proof assistant. No step reduces a derived claim back to its own inputs by construction, no parameters are fitted and then relabeled as predictions, and no load-bearing premises rest on self-citations or prior ansatzes from the same authors. The two contract-satisfaction examples are presented as applications of the system rather than as inputs that define it. The development is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on the reduction of contract satisfaction to relative trace equality and the adequacy of relative bisimulation as a proof technique. Since only the abstract is available, the ledger is necessarily incomplete; no free parameters are mentioned, standard coinductive axioms are invoked, and relative bisimulation is the primary invented concept.

axioms (1)

standard math Coinductive principles suffice to establish relative trace equality via bisimulation
The paper leverages recent advances in coinductive proofs to build the deductive system.

invented entities (1)

relative bisimulation no independent evidence
purpose: Proof technique to establish relative trace equality for contract satisfaction
Introduced as the associated proof technique for the relative trace equality problem.

pith-pipeline@v0.9.0 · 5511 in / 1461 out tokens · 89889 ms · 2026-05-10T17:09:31.343085+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

55 extracted references · 33 canonical work pages

[1]

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(Los Angeles, CA, USA)(CCS ’22). Association for Computing Machinery, New York, NY, USA, 83–96. doi:10.1145/3548606.3560689

work page doi:10.1145/3548606.3560689 2022
[2]

Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, and Vincent Laporte. 2025. Preservation of Speculative Constant-Time by Compilation.Proc. ACM Program. Lang.9, POPL, Article 44 (Jan. 2025), 33 pages. doi:10.1145/3704880

work page doi:10.1145/3704880 2025
[3]

Frans Kaashoek, Joseph Tassarotti, and Nickolai Zeldovich

Anish Athalye, Henry Corrigan-Gibbs, M. Frans Kaashoek, Joseph Tassarotti, and Nickolai Zeldovich. 2024. Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level Implementation. In Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, SOSP 2024, Austin, TX, USA, November 4-6, 2024. AC...

2024
[4]

Frans Kaashoek, and Nickolai Zeldovich

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). USENIX Association, 503–519

2022
[5]

Enrico Barberis, Pietro Frigo, Marius Muench, Herbert Bos, and Cristiano Giuffrida. 2022. Branch History Injection: On the Effectiveness of Hardware Mitigations Against Cross-Privilege Spectre-v2 Attacks. In31st USENIX Security Symposium (USENIX Security 22). USENIX Association, Boston, MA, 971–988. https://www.usenix.org/conference/ usenixsecurity22/pres...

2022
[6]

Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu. 2019. Formal verification of a constant-time preserving C compiler.Proc. ACM Program. Lang.4, POPL, Article 7 (Dec. 2019), 30 pages. doi:10.1145/3371075

work page doi:10.1145/3371075 2019
[7]

Gilles Barthe, Benjamin Grégoire, Vincent Laporte, and Swarn Priya. 2021. Structured leakage and applications to cryp- tographic constant-time and cost. InProceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security. 462–476

2021
[8]

Digital twins in health care: ethical implications of an emerging engineering paradigm,

Gilles Barthe, Benjamin Grégoire, and Vincent Laporte. 2018. Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic “Constant-Time”. In2018 IEEE 31st Computer Security Foundations Symposium (CSF). 328–343. doi:10.1109/CSF.2018.00031

work page doi:10.1109/csf.2018.00031 2018
[9]

Gilles Barthe, Tamara Rezk, and Amitabh Basu. 2007. Security types preserving compilation.Computer Languages, Systems & Structures33, 2 (2007), 35–59. doi:10.1016/j.cl.2005.05.002

work page doi:10.1016/j.cl.2005.05.002 2007
[10]

Gilles Barthe, Tamara Rezk, Alejandro Russo, and Andrei Sabelfeld. 2010. Security of multithreaded programs by compilation.ACM Trans. Inf. Syst. Secur.13, 3, Article 21 (July 2010), 32 pages. doi:10.1145/1805974.1805977

work page doi:10.1145/1805974.1805977 2010
[11]

Claudio Canella, Daniel Genkin, Lukas Giner, Daniel Gruss, Moritz Lipp, Marina 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 2019 ACM SIGSAC Conference on Computer and Communications Security(London, United Kingdom)(CCS ’19)....

work page doi:10.1145/3319535 2019
[12]

Minki Cho, Youngju Song, Dongjae Lee, Lennard Gäher, and Derek Dreyer. 2023. Stuttering for Free.Proc. ACM Program. Lang.7, OOPSLA2, Article 281 (Oct. 2023), 28 pages. doi:10.1145/3622857

work page doi:10.1145/3622857 2023
[13]

Arthur Correnson and Bernd Finkbeiner. 2025. Coinductive Proofs for Temporal Hyperliveness.Proc. ACM Program. Lang.9, POPL, Article 53 (Jan. 2025), 28 pages. doi:10.1145/3704889 24 Arthur Correnson, Haoyi Zeng, and Jana Hofmann

work page doi:10.1145/3704889 2025
[14]

Arthur Correnson, Iona Kuhn, and Bernd Finkbeiner. 2025. Almost Fair Simulations.Proc. ACM Program. Lang.9, ICFP, Article 243 (Aug. 2025), 24 pages. doi:10.1145/3747512

work page doi:10.1145/3747512 2025
[15]

Brijesh Dongol, Matt Griffin, Andrei Popescu, and Jamie Wright. 2024. Relative Security: Formally Modeling and (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities. In37th IEEE Computer Security Foundations Symposium, CSF 2024, Enschede, Netherlands, July 8-12, 2024. IEEE, 403–418. doi:10.1109/CSF61375.2024.00027

work page doi:10.1109/csf61375.2024.00027 2024
[16]

Mohammad Rahmani Fadiheh, Johannes Müller, Raik Brinkmann, Subhasish Mitra, Dominik Stoffel, and Wolfgang Kunz. 2020. A Formal Approach for Detecting Vulnerabilities to Transient Execution Attacks in Out-of-Order Processors. In2020 57th ACM/IEEE Design Automation Conference (DAC). 1–6. doi:10.1109/DAC18072.2020.9218572

work page doi:10.1109/dac18072.2020.9218572 2020
[17]

Alameldeen, Marco Guarnieri, Mark Silberstein, Oleksii Oleksenko, and Gururaj Saileshwar

Bo Fu, Leo Tenenbaum, David Adler, Assaf Klein, Arpit Gogia, Alaa R. Alameldeen, Marco Guarnieri, Mark Silberstein, Oleksii Oleksenko, and Gururaj Saileshwar. 2025. AMuLeT: Automated Design-Time Testing of Secure Speculation Countermeasures. InProceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Opera...

work page doi:10.1145/3676641.3716247 2025
[18]

Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer. 2022. Simuliris: a separation logic framework for verifying concurrent program optimizations.Proc. ACM Program. Lang.6, POPL, Article 28 (Jan. 2022), 31 pages. doi:10.1145/3498689

work page doi:10.1145/3498689 2022
[19]

Marco Guarnieri, Boris Köpf, José F Morales, Jan Reineke, and Andrés Sánchez. 2020. Spectector: Principled detection of speculative information flows. In2020 IEEE Symposium on Security and Privacy (SP). IEEE, 1–19

2020
[20]

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

2021
[21]

Jana Hofmann, Emanuele Vannacci, Cedric Fournet, Boris Kopf, and Oleksii Oleksenko. 2023. Speculation at Fault: Modeling and Testing Microarchitectural Leakage of CPU Exceptions. In32nd USENIX Security Symposium (USENIX Security 23). USENIX Association, Anaheim, CA, 7143–7160. https://www.usenix.org/conference/usenixsecurity23/ presentation/hofmann

2023
[22]

Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. 2013. Paco: A Coq Library for Parameterized Coinduction. https://plv.mpi-sws.org/paco/

2013
[23]

Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. 2013. The power of parameterization in coinductive proof. InProceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Rome, Italy)(POPL ’13). Association for Computing Machinery, New York, NY, USA, 193–206. doi:10.1145/2429069. 2429093

work page doi:10.1145/2429069 2013
[24]

Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. InProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(Mumbai, India)(POPL ’15). Association for Computing Machinery, Ne...

work page doi:10.1145/2676726.2676980 2015
[25]

Paul Kocher, Jann Horn, Anders Fogh, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. 2019. Spectre Attacks: Exploiting Speculative Execution. In2019 IEEE Symposium on Security and Privacy (SP). 1–19. doi:10.1109/SP.2019.00002

work page doi:10.1109/sp.2019.00002 2019
[26]

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 18)

2018
[27]

McCullough

D. McCullough. 1988. Noninterference and the composability of security properties. InProceedings. 1988 IEEE Symposium on Security and Privacy (S&P’88). 177–186. doi:10.1109/SECPRI.1988.8110

work page doi:10.1109/secpri.1988.8110 1988
[28]

Gideon Mohr, Marco Guarnieri, and Jan Reineke. 2024. Synthesizing Hardware-Software Leakage Contracts for RISC-V Open-Source Processors(DATE’24). 1–6

2024
[29]

Oleksii Oleksenko, Christof Fetzer, Boris Köpf, and Mark Silberstein. 2022. Revizor: Testing Black-box CPUs against Speculation Contracts. In27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS ’22). ACM

2022
[30]

Oleksii Oleksenko, Marco Guarnieri, Boris Kopf, 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 Computer Society, Los Alamitos, CA, USA, 1737–1752. doi:10.1109/SP46215.2023.10179391

work page doi:10.1109/sp46215.2023.10179391 2023
[31]

Marco Patrignani and Deepak Garg. 2017. Secure Compilation and Hyperproperty Preservation. In2017 IEEE 30th Computer Security Foundations Symposium (CSF). 392–404. doi:10.1109/CSF.2017.13

work page doi:10.1109/csf.2017.13 2017
[32]

Marco Patrignani and Marco Guarnieri. 2021. Exorcising Spectres with Secure Compilers. InProceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security(Virtual Event, Republic of Korea)(CCS ’21). Association for Computing Machinery, New York, NY, USA, 445–461. doi:10.1145/3460120.3484534

work page doi:10.1145/3460120.3484534 2021
[33]

Damien Pous. 2007. Complete Lattices and Up-To Techniques. InProgramming Languages and Systems, Zhong Shao (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 351–366. A Deductive System for Contract Satisfaction Proofs 25

2007
[34]

Damien Pous. 2016. Coinduction All the Way Up. InProceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science(New York, NY, USA)(LICS ’16). Association for Computing Machinery, New York, NY, USA, 307–316. doi:10.1145/2933575.2934564

work page doi:10.1145/2933575.2934564 2016
[35]

Julian Rosemann, Sebastian Hack, and Deepak Garg. 2025. Non-interference Preserving Optimising Compilation.Proc. ACM Program. Lang.9, OOPSLA2, Article 323 (Oct. 2025), 26 pages. doi:10.1145/3763101

work page doi:10.1145/3763101 2025
[36]

DAVIDE SANGIORGI. 1998. On the bisimulation proof method.Mathematical Structures in Computer Science8, 5 (1998), 447–479. doi:10.1017/S0960129598002527

work page doi:10.1017/s0960129598002527 1998
[37]

Michael Schwarz, Moritz Lipp, Daniel Moghimi, Jo Van Bulck, Julian Stecklina, Thomas Prescher, and Daniel Gruss
[38]

InProceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security(London, United Kingdom)(CCS ’19)

ZombieLoad: Cross-Privilege-Boundary Data Sampling. InProceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security(London, United Kingdom)(CCS ’19). Association for Computing Machinery, New York, NY, USA, 753–768. doi:10.1145/3319535.3354252

work page doi:10.1145/3319535.3354252 2019
[39]

Hirsch, and Steve Zdancewic

Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, and Steve Zdancewic. 2023. Semantics for Noninterference with Interaction Trees. In37th European Conference on Object-Oriented Programming (ECOOP 2023) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 263), Karim Ali and Guido Salvaneschi (Eds.). Schloss Dagstuhl – Leibniz- Zentrum ...

work page doi:10.4230/lipics.ecoop.2023.29 2023
[40]

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, Volume 1(Rotterdam, Netherlands)(ASPLOS ’25). Association for Computing Machin...

work page doi:10.1145/3669940.3707243 2025
[41]

Alfred Tarski. 1955. A lattice-theoretical fixpoint theorem and its applications. (1955)

1955
[42]

Daniël Trujillo, Johannes Wikner, and Kaveh Razavi. 2023. INCEPTION: exposing new attack surfaces with training in transient execution. InProceedings of the 32nd USENIX Conference on Security Symposium(Anaheim, CA, USA)(SEC ’23). USENIX Association, USA, Article 409, 18 pages

2023
[43]

Wenisch, Yuval Yarom, and Raoul Strackx

Jo Van Bulck, Marina Minkin, Ofir Weisse, Daniel Genkin, Baris Kasikci, Frank Piessens, Mark Silberstein, Thomas F. Wenisch, Yuval Yarom, and Raoul Strackx. 2018. Foreshadow: extracting the keys to the intel SGX kingdom with transient out-of-order execution. InProceedings of the 27th USENIX Conference on Security Symposium(Baltimore, MD, USA)(SEC’18). USE...

2018
[44]

Jo Van Bulck, Daniel Moghimi, Michael Schwarz, Moritz Lippi, Marina Minkin, Daniel Genkin, Yuval Yarom, Berk Sunar, Daniel Gruss, and Frank Piessens. 2020. LVI: Hijacking Transient Execution through Microarchitectural Load Value Injection. In2020 IEEE Symposium on Security and Privacy (SP). 54–72. doi:10.1109/SP40000.2020.00089

work page doi:10.1109/sp40000.2020.00089 2020
[45]

Sören van der Wall and Roland Meyer. 2025. SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations.Proc. ACM Program. Lang.9, POPL, Article 51 (Jan. 2025), 30 pages. doi:10.1145/3704887

work page doi:10.1145/3704887 2025
[46]

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. In2019 IEEE Symposium on Security and Privacy (SP). 88–105. doi:10.1109/SP.2019.00087

work page doi:10.1109/sp.2019.00087 2019
[47]

Zilong Wang, Gideon Mohr, Klaus Gleissenthall, Jan Reineke, and Marco Guarnieri. 2025. Synthesis of Sound and Precise Leakage Contracts for Open-Source RISC-V Processors

2025
[48]

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. (2023), 2128–2142. doi:10. 1145/3576915.3623192

work page arXiv 2023
[49]

Pierce, and Steve Zdancewic

Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic
[50]

Pierce, and Steve Zdancewic

Interaction trees: representing recursive and impure programs in Coq.Proc. ACM Program. Lang.4, POPL, Article 51 (Dec. 2019), 32 pages. doi:10.1145/3371119

work page doi:10.1145/3371119 2019
[51]

Yannick Zakowski, Paul He, Chung-Kil Hur, and Steve Zdancewic. 2020. An equational theory for weak bisimulation via generalized parameterized coinduction. InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs(New Orleans, LA, USA)(CPP 2020). Association for Computing Machinery, New York, NY, USA, 71–84. doi:10.1145...

work page doi:10.1145/3372885.3373813 2020
[52]

∈bisim∧ (𝑠 ′ 1, 𝑠2, ℎ1, ℎ2) ∈𝑅} H-Leak-Eq 𝑓(𝑅)≜{ (𝑠 1, 𝑠2, ℎ1, ℎ2) | (ℎ 1, ℎ′
[53]

∈bisim∧ (𝑠 1, 𝑠2, ℎ1, ℎ′
[54]

∈𝑅} Reduce-C-Leakage 𝑓(𝑅)≜{ (𝑠 1, 𝑠2, ℎ1, ℎ2) | (𝑠 1, 𝑠2, 𝑠′ 1, 𝑠′
[55]

∈rbisim∧ (𝑠 ′ 1, 𝑠′ 2, ℎ1, ℎ2) ∈𝑅} Augment-H-Leakage 𝑓(𝑅)≜{ (𝑠 1, 𝑠2, ℎ1, ℎ2) | (ℎ ′ 1, ℎ′ 2, ℎ1, ℎ2) ∈rbisim lockstep ∧ (𝑠 1, 𝑠2, ℎ′ 1, ℎ′