Pith. sign in

REVIEW 3 major objections 4 minor 98 references

dfence: Fine-Grained Speculation Barriers for Efficient and Effective Hardware-Software Protection in the Spectre Era (Extended Version)

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

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

Pith's one-line read dfence introduces a single CPU instruction that blocks both Spectre-PHT and Spectre-STL leakage at under 1% performance overhead.

desk verdict A serious formal contribution with a weaker empirical security story than its headline suggests; worth reviewing, needs revision. read the letter →

arxiv 2608.06124 v1 pith:FYP5DBGS submitted 2026-08-06 cs.CR

Davide Davoli , Marton Bognar , Lesly-Ann Daniel , Benjamin Grégoire , Frank Piessens , Tamara Rezk This is my paper · ORCID
classification cs.CR
keywords speculativeexecutionSpectre-PHTSpectre-STLstorebypassselectiveregisterfenceconstant-timetypesystemRISC-V
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

The paper tries to establish that a single new CPU instruction, dfence, can replace the error-prone software bookkeeping of Speculative Load Hardening with a hardware guarantee: dfence x holds the value of register x back from later instructions until that value is no longer speculative. If correct, this collapses two separate defenses — masking for Spectre-PHT and disabling store-to-load speculation for Spectre-STL — into one instruction, with an average measured overhead below 1% on the paper's RISC-V prototype. To make placement safe in practice, the paper builds a type system that accepts a program only when every value that can become secret during speculative execution is protected by dfence before it reaches a leaking operand, and proves that well-typed programs are speculative constant-time. The paper also checks 40 protected gadgets on a cycle-accurate simulator and reports no observable leakage, alongside a hardware cost of roughly 0.2–2.5% added area.

What carries the argument

The key machinery is the dfence instruction itself, a selective register fence whose semantics (rule [SDfence]) under misspeculation sets the protected register to $\bot$, so dependent instructions cannot transiently use it. Around this the paper wraps two supports: a two-level type system in which each register has a non-speculative and a speculative confidentiality level and every transient load's destination is typed $(\cdot,H)$, and hardware speculation tracking in the reorder buffer and reservation stations that keeps a dfence from executing until all older speculation has resolved. Together they make 'protect the secret before it reaches an unsafe operand' a checkable, enforceable contract rather than a programmer convention.

What would settle it

A concrete falsifier: on a processor implementing dfence, execute a predictive-store-forwarding gadget in which the forwarded store value is secret and the following load address depends on it, with dfence placed as prescribed; if the cache-set access pattern differs between two secret values, the [SDfence] rule or its hardware implementation is wrong.

Watch

Extended reading notes

Core claim

The central discovery is that a fine-grained, register-specific fence can generalize SLH's value protection to speculation sources that software cannot see. The paper specifies dfence x as a selective register fence: its operand x is not forwarded to subsequent instructions until the value becomes non-speculative, and the [SDfence] semantic rule makes x unavailable ($\bot$) whenever the misspeculation flag is set. Hardware taint tracking records every speculative source — conditional branches, store-to-load bypasses, and predictive store forwarding — and blocks a dfence in its reservation station until those sources resolve. On the software side, each register carries a pair of security levels (non-speculative, speculative), and a load is always given speculative type H because transient loads can be out-of-bounds or forward stale values; dfence x resets the speculative type of x to its non-speculative type. The paper proves (Theorem 1) that every program accepted by this type system is $\simeq_\Gamma$-speculative constant-time, meaning two runs that agree on public memory produce identical leakage traces under identical speculation directives.

Load-bearing premise

The guarantee depends on the leakage model being exactly the one proved — memory addresses and branch conditions — and on the hardware holding the protected register until every modeled speculation source resolves; any real processor that resolves store-to-load speculation by value instead of address, any transient jump outside the statically known target set, or any compiler-inserted memory access breaks the proof.

Editorial extensions

If this is right

  • Cryptographic code can be hardened against Spectre-PHT and Spectre-STL with one dfence per sensitive register instead of a global software mask or a global disable of store-to-load forwarding.
  • Because the hardware, not software, tracks speculation, dfence covers store-bypass and predictive-store-forwarding leaks that Speculative Load Hardening cannot detect.
  • The type system rejects gadgets such as Spectre v1.1 by requiring that indirect jump and return targets be protected with dfence, making transient control-flow redirection untypable.
  • A drop-in dfence replacement inside existing compiler-based SLH passes would likely reduce their overhead, since dfence removes the need for a dedicated misspeculation register and its updates.
  • Implementing dfence as a fully serializing fence or as an unoptimized delayed-forwarding instruction is already secure; the optimized variant just adds taint-based speculation tracking.

Reading between the lines

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

  • If dfence were adopted commercially, the roughly 12% average cost of disabling store-to-load speculation globally could disappear, since only registers that actually carry secret data are held back.
  • The same value-protection principle appears to extend to load-address prediction attacks by adding that speculation source to the hardware's tracking; the paper sketches this extension but does not implement it.
  • An automatic insertion pass that places dfence wherever the type system sees a value that is public architecturally but secret speculatively could push most of the annotation burden into the compiler; the paper's initial heuristics already protect several primitives without manual edits.
  • The source-level proof leaves two unverified links — the compiler must preserve speculative constant-time and the CPU must implement the dfence rule faithfully — so a formal end-to-end proof would close the remaining gap between the security contract and the shipped binary.
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

3 major / 4 minor

Summary. The paper introduces dfence, a new RISC-V instruction that acts as a selective register fence: it prevents a designated register's value from being forwarded to dependent instructions until the value becomes non-speculative. The authors present a small imperative language with a speculative operational semantics, a type system that tracks non-speculative and speculative confidentiality levels, and a soundness theorem (Theorem 1) stating that well-typed programs are speculative constant-time (SCT) against PHT, SSB, and PSF speculation in the abstract model. They implement dfence in the Proteus RISC-V core, report less than 1% geometric-mean overhead on cryptographic benchmarks, and perform a security evaluation on 40 secure and 40 insecure generated programs. The extended version contains the operational semantics (Appendix B), the soundness proof (Appendix C), a jump-target analysis (Appendix D), and detailed benchmark tables (Appendix E).

Significance. If the claims hold, this is a significant contribution: it provides a clean hardware-software co-design that generalizes SLH to store-to-load speculation, with a formally analyzed type system and a concrete, low-cost hardware implementation. The formal development is substantial and unusually detailed for a systems paper, including a Scott-continuity argument to handle recursive jump-continuation reasoning in the soundness proof. The open-source artifact and reproducibility materials are a concrete strength. The main caveat is that the end-to-end security guarantee is not actually established: the theorem applies to an abstract semantics, and the bridge to the Proteus binary relies on two unverified steps (compiler preservation of SCT and hardware conformance to the [SDfence] rule), while the empirical validation of that bridge is underpowered because only 20 of the 40 insecure control programs leaked.

major comments (3)
  1. [§6.1] The security evaluation reports that only 20 of the 40 deliberately insecure programs leaked, under both the conservative and liberal signal sets. Consequently, for the remaining 20 insecure programs, the harness produces identical signal sets for the two secret inputs whether the program is protected or not, so the companion result that all 40 protected programs are secure has no discriminating power for those leakage classes. The paper should either report which of the four speculation strategies and five leakage channels are actually exercised by the leaking controls, add tests that make the non-leaking classes leak, or explicitly weaken the statement that the evaluation confirms that dfence effectively closes leaks on Proteus. As written, the empirical validation of hardware conformance to the [SDfence] rule is substantially weaker than the 'all 40 programs secure' phrasing suggests.
  2. [§4, §9.2] The central theorem (Theorem 1) is proved for the abstract semantics of Appendix B, not for binaries running on Proteus. The paper explicitly acknowledges in Section 9.2 that compiler preservation of speculative constant-time and hardware conformance to the [SDfence] rule are open. This is a load-bearing gap: the paper's strongest claim—that dfence protects programs against PHT, SSB, and PSF at negligible overhead—requires those two unverified steps to connect the theorem to the actual CPU. The abstract and conclusion should state this scoping explicitly rather than presenting end-to-end protection as an achieved result.
  3. [§B, §9.1] The formal leakage model covers only memory operands and branch guards, and the SSB and PSF rules ([SLoad-PSF], [SLoad-SSB]) are address-based. Section 9.1 notes that value-based PSF/SSB resolution would break the model and require orthogonal defenses, and that BTB/RSB speculation is excluded. These are significant scope limitations, and the abstract's unqualified phrase 'mitigates both Spectre-PHT and Spectre-STL' overstates what the theorem and the Proteus configuration actually cover. The claims should be qualified to the address-based, PHT/SSB/PSF model used in the formal development.
minor comments (4)
  1. [Figure 2, rule [TOp]] The rule as printed requires every sub-expression op(E1,…,Ek) to have exactly the same type σ, which is needlessly restrictive for binary operators with mixed operands. Please clarify whether this is intentional (with [TSub] used to unify) or whether the rule is intended to take a join of per-operand types.
  2. [§6.2.1, Table 3] The negative overheads (e.g., -3.15% for Keccak-f1600) are explained by a hypothesis about reduced transient-instruction squashing. Since these are cycle-accurate simulator measurements, it would be helpful to report run-to-run variance or a sensitivity analysis to rule out measurement artifacts.
  3. [§6.1] Each program is run only twice, with a single pair of secret inputs, against two manually selected signal sets. The paper should state this sampling limitation explicitly in the security-evaluation methodology and discuss how the choice of inputs and signals affects the sensitivity of the leak test.
  4. [Appendix C, Lemma 22 proof] The proof of Lemma 22 refers to assumptions (H1)–(H4), but the lemma statement lists only (C1) and (C2); the numbering should be aligned to avoid confusion.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: Theorem 1 is proved against an explicit operational semantics, and the evaluation rests on measurements and open artifacts rather than on fitted or self-cited premises.

full rationale

The paper's central claim is the soundness theorem (Theorem 1: "If Γ⊢P : Σ then P is ≊Γ-SCT"), which is established in Appendix C by induction over the typing derivation against the operational semantics of Figure 3. The [SDfence] rule and the [TDfence] typing rule are co-designed, but that is not circular: the semantics fixes the instruction's behavior (setting x to ⊥ under misspeculation) and the type system is then proved to make observations equal on related states; the proof is a genuine subject-reduction/Scott-continuity argument, not a restatement of the conclusion. The claims for Spectre-PHT, SSB and PSF are accounted for by the speculative rules [SLoad-OOB], [SLoad-PSF] and [SLoad-SSB] used in the proof. The end-to-end security of the binary is explicitly acknowledged as an open gap in §9.2 ("There is currently a gap between our Jasmin-level security contract and its hardware implementation"), and the §6.1 evaluation's 20/40 sensitivity for insecure controls is an empirically underpowered validation, but that is a correctness-risk issue rather than a circular reduction. The performance numbers are direct cycle measurements on the Proteus simulator, with no fitted parameters renamed as predictions. Citations to Proteus, Jasmin, and ProSpeCT are references to open, code-reproduced infrastructure or prior comparison baselines; none is used as the sole justification of the security theorem, so they do not make the argument circular.

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

The central derivation is a formal type-soundness theorem, so it consumes no fitted numerical parameters. The mathematical proof uses standard order-theoretic machinery. The domain assumptions narrow the threat model (leakage set, address-based SSB/PSF, no BTB/RSB, compiler preservation, static jump targets), and these, rather than fitted constants, are the price of the security guarantee.

assumptions (7)
  • domain assumption Non-speculative (architectural) memory safety of programs
    The type system and proofs assume arrays are fixed-size, offsets stay in bounds in normal execution, and out-of-bounds access happens only on misspeculated paths (Section 3.3, Section 4).
  • domain assumption Leakage model is restricted to memory operands and guards of control-flow instructions
    Observations in the operational semantics are mem(a,n) and br b; other channels such as power, port contention, and prefetch are out of scope (Section 2.1, Section 3.3).
  • domain assumption SSB and PSF speculation resolve by address, not by value
    The paper assumes Proteus-style address-based store-to-load speculation; value-based resolution would turn store/load values into unsafe operands and invalidate dfence's guarantee (Section 9.1).
  • domain assumption BTB and RSB speculation are handled by complementary defenses
    The threat model considers only PHT speculation; the Proteus test chip has a BTB that is broader, and the paper requires external BTB/RSB mitigations or extensions for full security (Section 3.3, Section 5.1, Section 9.1).
  • domain assumption Compilation preserves speculative constant-time
    Theorem 1 typifies source programs; lifting it to binaries requires Jasmin to preserve SCT, which the paper states is still an active research topic (Section 3.2, Section 9.2).
  • domain assumption Jump targets can be statically over-approximated for v1.1 protection
    Rule [TJmp] and Appendix D rely on a fixed set V of possible targets; in Jasmin this holds for return instructions only if return addresses are protected and RSB is not speculated (Section 4, Appendix D).
  • standard math Scott-continuity and fixed-point reasoning for the jump context
    The soundness proof uses an indexed semantics and Scott-continuity (Lemma 4) to justify the [TCont] rule; this is standard order-theoretic machinery, not specific to dfence (Appendix C).
invented entities (1)
  • dfence instruction
    purpose: A new ISA-level selective speculation barrier that withholds a register value until speculation resolves, generalizing SLH to cover Spectre-PHT, SSB, and PSF.
    The instruction exists only in the paper's Proteus extension and formal model; it has not been independently implemented or ratified by any hardware vendor, so its effectiveness rests on the authors' own simulator evaluation and proof.

how reviews work

0 comments
Cite this review

Pith. "Pith review of dfence: Fine-Grained Speculation Barriers for Efficient and Effective Hardware-Software Protection in the Spectre Era (Extended Version)." pith.science (2026). https://pith.science/paper/FYP5DBGS

@misc{pith2026260806124,
  author       = {Pith},
  title        = {Pith review of: dfence: Fine-Grained Speculation Barriers for Efficient and Effective Hardware-Software Protection in the Spectre Era (Extended Version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/FYP5DBGS}},
  note         = {Machine review of arXiv:2608.06124}
}
read the original abstract

Speculative execution attacks such as Spectre-PHT and Spectre-STL remain a critical security concern in modern processors. While software-based mitigations like Speculative Load Hardening (SLH) offer effective protection against Spectre-PHT, they are limited in scope and require software-managed speculative masks, which can be error-prone and costly. Defenses against Spectre-STL, such as the Speculative Store Bypass Disable bit (SSBD), incur additional performance overhead and lack fine-grained control. In this work, we introduce dfence, a new CPU instruction that generalizes SLH to mitigate both Spectre-PHT and Spectre-STL with minimal hardware support. dfence enables developers to annotate sensitive registers, with the hardware ensuring that these values do not leak transiently. We implement dfence in the Proteus CPU and evaluate its security and performance, demonstrating less than 1% average performance overhead for our benchmarks. In addition, to support easy and secure adoption, we design a type system that statically verifies the correct placement of dfence instructions in code.

Figures

Figures reproduced from arXiv: 2608.06124 by the authors.

Figure 1
Figure 1. Syntax of the language. Here v ∈ V is a value, x ∈ Reg is a register variable and a ∈ Arr is an array name. mechanisms that prevent the introduction of exploitable specula￾tive gadgets. This approach is consistent with existing practice, where different protection techniques are combined to secure dif￾ferent layers of the system. For instance, cryptographic routines can be isolated using compartmentalization mechani… view at source ↗
Figure 2
Figure 2. Type system. reflects the principle that public data can always be treated as secret. For simplicity’s sake, we assume that applying an operator op to a sequence of sub-expressions takes the same amount of time regardless of the values involved, so that no information can leak through the timing of expression evaluation itself. This assumption can be easily relaxed by imposing that arguments of expressions with data… view at source ↗
Figure 3
Figure 3. Speculative semantics. Rules for ordinary configurations: 𝑟1 ∼⊥ 𝑟2 𝑟1 ≃ 𝛽 Γ 𝑟2 𝑚1 ≃Γ 𝑚2 𝜇1 ≃ 𝛽 Γ 𝜇2 𝑟1, 𝜇1,𝑚1, 𝛽 ≊Γ 𝑟2, 𝜇2,𝑚2, 𝛽 ∀x ∈ Reg.𝑟1 (x) = ⊥ ⇔ 𝑟2 (x) = ⊥ 𝑟1 ∼⊥ 𝑟2 ∀a ∈ Arr.Γ(a) = L ⇒ 𝑚1 (a) = 𝑚2 (a) 𝑚1 ≃Γ 𝑚2 ∀x ∈ Reg.𝜋1 (Γ(x)) = L ∨ 𝜋2 (Γ(x)) = L ⇒ 𝑟1 (x) = 𝑟2 (x) 𝑟1 ≃ ⊥ Γ 𝑟2 ∀x ∈ Reg.𝜋2 (Γ(x)) = L ⇒ 𝑟1 (x) = 𝑟2 (x) 𝑟1 ≃ ⊤ Γ 𝑟2 Γ(a) = L ⇒ v1 = v2 𝜇1 ≃ ⊥ Γ 𝜇2 [(a, 𝑛) ↦→ v1] : 𝜇1 ≃ ⊥ Γ [(a, 𝑛) ↦→ v2] : 𝜇2 𝜇1 ≃… view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Rules defining the ≊Γ relation. a proof of a judgment. For instance we now can write: TSeq 𝜋1 ⊲ Φ | Γ1 ⊢ P1 : Γ2 𝜋2 𝜋 ⊲ Φ | Γ1 ⊢ P1; P2 : Γ3 In this notation, 𝜋 is the proof tree for the entire derivation of Φ | Γ1 ⊢ P1; P2 : Γ3, and 𝜋1, 𝜋2 are proof trees for the sub-…
Figure 5
Figure 5. Figure 5: Definition of judgment’s semantics By expanding the definition of J·K, the claim becomes: ∀𝑛 ′ ≤ 𝑛.∀𝑠, 𝑡 ∈ States𝑖+1.∀𝐷,𝑂.𝑠 ≊Γ1 𝑡 ⇒ ∀P ′ , 𝑠′ . 𝜙 ⊢ jmp E𝑉 ; P, 𝑠 𝑂 −→𝐷 𝑛 ′ P ′ , 𝑠′ ⇒ ∃𝑡 ′ . 𝜙 ⊢ jmp E𝑉 ; P, 𝑡 𝑂 −→𝐷 𝑛 ′ P ′ , 𝑡′ ∧ (P ′ = 𝜖 ⇒ 𝑠 ′ ≊Γ3 𝑡 ′ ). Fix 𝑛 ′ , 𝑠, 𝑡…
Figure 6
Figure 6. Figure 6: Non-speculative semantics. this property via the predicate D (P), which is defined as follows: D (x := E) D (x := a[E]) D (a[E] := F) D (P1) D (P2) D (if E then P1 else P2 fi) D (P) D (while E do P od) Dfence D (dfencex) D (fence) D (I) D (P) D (I; P) Jump D (P) D (dfe…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

98 extracted references · 43 canonical work pages

  1. [1]

    Intel 2024.Hardware Features and Behaviors Related to Speculative Execution. Intel. https://www.intel.com/content/www/us/en/developer/articles/technical/ software-security-guidance/technical-documentation/hardware-behavior- related-to-speculative-execution.html

    2024

  2. [2]

    Alejandro Cabrera Aldaya, Billy Bob Brumley, Sohaib ul Hassan, Cesar Pereida García, and Nicola Tuveri. 2019. Port Contention for Fun and Profit. InIEEE S&P. IEEE. doi:10.1109/SP.2019.00066

    arXiv 2019

  3. [3]

    José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, and Pierre-Yves Strub. 2017. Jasmin: High-Assurance and High-Speed Cryptography. InCCS. ACM. doi:10.1145/3133956.3134078

    arXiv 2017

  4. [4]

    José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, and Michael Emmi. 2016. Verifying Constant-Time Implementations. InUSENIX Secu- rity. USENIX Association. https://www.usenix.org/conference/usenixsecurity16/ technical-sessions/presentation/almeida

    2016

  5. [5]

    2021.Security Analysis of AMD Predictive Store Forwarding

    AMD. 2021.Security Analysis of AMD Predictive Store Forwarding. https://www.amd.com/system/files/documents/security-analysis-predictive- store-forwarding.pdf

    2021

  6. [6]

    2023.Software Techniques for Managing Speculation on AMD Processors

    AMD. 2023.Software Techniques for Managing Speculation on AMD Processors. White Paper Revision 5.09.23. https://www.amd.com/content/dam/amd/en/ documents/processor-tech-docs/programmer-references/software-techniques- for-managing-speculation.pdf

    2023

  7. [7]

    Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, and Lucas Tabary-Maujean

  8. [8]

    Herinomena Andrianatrehina, Ronan Lashermes, Joseph Paturel, Simon Rokicki, and Thomas Rubiano. 2025. Exploring speculation barriers for RISC-V selective speculation. InARES. ACM. https://hal.science/hal-05061555

    2025

Show all 98 references
  1. [9]

    Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, and Vincent Laporte. 2025. Preservation of Speculative Constant-Time by Com- pilation.Proceedings of the ACM on Programming Languages9, POPL (2025). doi:10.1145/3704880

    2025 doi

  2. [10]

    Santiago Arranz Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Peter Schwabe, Yuval Yarom, and Zhiyuan Zhang. 2025. Protecting Cryptographic Code Against Spectre-RSB: (and, in Fact, All Known Spectre Variants). InASPLOS, V...

    2025

  3. [11]

    Jonathan Baumann, Roberto Blanco, Léon Ducruet, Sebastian Harwig, and Catalin Hritcu. 2025. FSLH: Flexible Mechanized Speculative Load Hardening. InIEEE CSF. IEEE, 569–584. doi:10.1109/CSF64896.2025.00023

    2025

  4. [12]

    Bernstein

    Daniel J. Bernstein. 2005. Cache-timing attacks on AES. https://cr.yp.to/ antiforgery/cachetiming-20050414.pdf

    2005

  5. [13]

    Bernstein

    Daniel J. Bernstein. 2005. The Poly1305-AES Message-Authentication Code. In FSE. Springer. doi:10.1007/11502760_3 Davide Davoli, Marton Bognar, Lesly-Ann Daniel, Benjamin Grégoire, Frank Piessens, and Tamara Rezk

    2005 doi

  6. [14]

    Bernstein

    Daniel J. Bernstein. 2006. Curve25519: New Diffie-Hellman Speed Records. In PKC. Springer. doi:10.1007/11745853_14

    2006 doi

  7. [15]

    Bernstein

    Daniel J. Bernstein. 2008. ChaCha, a variant of Salsa20. InSASC, Vol. 8. ECRYPT. https://www.ecrypt.eu.org/stvl/sasc2008/SASCRecord.zip

    2008

  8. [16]

    Daniel J. Bernstein, Stefan Kölbl, Stefan Lucks, Pedro Maat Costa Massolino, Florian Mendel, Kashif Nawaz, Tobias Schneider, Peter Schwabe, François-Xavier Standaert, Yosuke Todo, and Benoît Viguier. 2017. Gimli : A Cross-Platform Permutation. InCHES. Springer. doi:10.1007/978...

    2017 doi

  9. [17]

    Bernstein, Tanja Lange, and Peter Schwabe

    Daniel J. Bernstein, Tanja Lange, and Peter Schwabe. 2012. The Security Impact of a New Cryptographic Library. InLATINCRYPT. Springer. doi:10.1007/978-3- 642-33481-8_9

    2012 doi

  10. [18]

    2011.The Keccak Reference

    Guido Bertoni, Joan Daemens, Michaël Peeters, and Gilles Van Assche. 2011.The Keccak Reference. Reference Specification Version 3.0. https://keccak.team/files/ Keccak-reference-3.0.pdf

    2011

  11. [19]

    Atri Bhattacharyya, Alexandra Sandulescu, Matthias Neugschwandtner, Alessan- dro Sorniotti, Babak Falsafi, Mathias Payer, and Anil Kurmus. 2019. SMoTh- erSpectre: Exploiting Speculative Execution through Port Contention. InCCS. ACM. doi:10.1145/3319535.3363194

    2019

  12. [20]

    G. R. Blakley. 1979. Safeguarding cryptographic keys. InMARK. IEEE. doi:10. 1109/MARK.1979.8817296

    1979

  13. [21]

    RISC-V Summit Europe

    Marton Bognar, Job Noorman, and Frank Piessens. 2023. Proteus: An Extensible RISC-V Core for Hardware Extensions. Presented at "RISC-V Summit Europe". https://lirias.kuleuven.be/4088721

    2023

  14. [22]

    Schanck, Peter Schwabe, Gregor Seiler, and Damien Stehle

    Joppe Bos, Leo Ducas, Eike Kiltz, T Lepoint, Vadim Lyubashevsky, John M. Schanck, Peter Schwabe, Gregor Seiler, and Damien Stehle. 2018. CRYSTALS - Kyber: A CCA-Secure Module-Lattice-Based KEM. InIEEE EuroS&P. IEEE. doi:10.1109/EuroSP.2018.00032

    2018

  15. [23]

    Lucy Bowen and Chris Lupo. 2020. The Performance Cost of Software-based Security Mitigations. InICPE. ACM. doi:10.1145/3358960.3379139

    2020

  16. [24]

    Claudio Canella, Jo Van Bulck, Michael Schwarz, Moritz Lipp, Benjamin von Berg, Philipp Ortner, Frank Piessens, Dmitry Evtyushkin, and Daniel Gruss. 2019. A Systematic Evaluation of Transient Execution Attacks and Defenses. InUSENIX Security. USENIX Association, 249–266. https...

    2019

  17. [25]

    2018.Speculative Load Hardening

    Chandler Carruth. 2018.Speculative Load Hardening. https://llvm.org/docs/ SpeculativeLoadHardening.html

    2018

  18. [27]

    Tullsen, Deian Stefan, Tamara Rezk, and Gilles Barthe

    Sunjay Cauligi, Craig Disselkoen, Klaus von Gleissenthall, Dean M. Tullsen, Deian Stefan, Tamara Rezk, and Gilles Barthe. 2020. Constant-time foundations for the new spectre era. InPLDI. ACM. doi:10.1145/3385412.3385970

    2020

  19. [28]

    Fletcher, David Kohlbrenner, Riccardo Paccagnella, and Daniel Genkin

    Boru Chen, Yingchen Wang, Pradyumna Shome, Christopher W. Fletcher, David Kohlbrenner, Riccardo Paccagnella, and Daniel Genkin. 2024. GoFetch: Breaking Constant-Time Cryptographic Implementations Using Data Memory-Dependent Prefetchers. InUSENIX Security. USENIX Association. h...

    2024

  20. [29]

    Xiaoyu Cheng, Fei Tong, Hongyu Wang, Zhe Zhou, Fang Jiang, and Yuxing Mao

  21. [30]

    Rutvik Choudhary, Jiyong Yu, Christopher Fletcher, and Adam Morrison. 2021. Speculative Privacy Tracking (SPT): Leaking Information From Speculative Exe- cution Without Compromising Privacy. InMICRO. ACM. doi:10.1145/3466752. 3480068

    2021 doi

  22. [31]

    Md Hafizul Islam Chowdhuryy and Fan Yao. 2022. Leaking Secrets Through Modern Branch Predictors in the Speculative World.IEEE Trans. Comput.71, 9 (2022). https://doi.org/10.1109/TC.2021.3122830

    2022

  23. [32]

    Gaidis, Vaggelis Atlidakis, and Vasileios P

    Neophytos Christou, Alexander J. Gaidis, Vaggelis Atlidakis, and Vasileios P. Ke- merlis. 2024. Eclipse: Preventing Speculative Memory-error Abuse with Artificial Data Dependencies. InCCS. ACM. doi:10.1145/3658644.3690201

    2024

  24. [33]

    2025.formosa-mldsa

    Formosa Crypto. 2025.formosa-mldsa. https://github.com/formosa-crypto/ formosa-mlkem

    2025

  25. [34]

    2025.formosa-mlkem

    Formosa Crypto. 2025.formosa-mlkem. https://github.com/formosa-crypto/ formosa-mldsa/tree/armv7m-riscv32

    2025

  26. [35]

    2025.libjade

    Formosa Crypto. 2025.libjade. https://github.com/formosa-crypto/libjade

    2025

  27. [36]

    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. InUSENIX Security. USENIX Association. https: //www.usenix.org/conference/usenixsecurity23/presentation/daniel

    2023

  28. [37]

    Davide Davoli, Marton Bognar, Lesly-Ann Daniel, Benjamin Grégoire, Frank Piessens, and Tamara Rezk. 2026. dfence: Fine-Grained Speculation Barriers for Efficient and Effective Hardware-Software Protection in the Spectre Era. InCCS. ACM, 35. doi:10.1145/3830454.3832748

    2026

  29. [38]

    Jesse De Meulemeester, Quinten Norga, Frank Piessens, Ingrid Verbauwhede, and Marton Bognar. 2025. Hardware Cost Evaluation in Systems Security. In ACM REP. doi:10.1145/3736731.3746155

    2025

  30. [39]

    Jack Doweck. 2006. Intel Smart Memory Access and the Energy- Efficient Performance of the Intel Core Microarchitecture. https: //web.archive.org/web/20231026102745/https://www.all-electronics.de/wp- content/uploads/migrated/document/196371/413ei0507-intel-sma.pdf

    2006

  31. [40]

    Léo Ducas, Eike Kiltz, Tancrède Lepoint, Vadim Lyubashevsky, Peter Schwabe, Gregor Seiler, and Damien Stehlé. 2018. CRYSTALS-Dilithium: A Lattice-Based Digital Signature Scheme.IACR Transactions on Cryptographic Hardware and Embedded Systems2018, 1 (2018). doi:10.13154/TCHES.V...

    2018 doi

  32. [41]

    Jacob Fustos, Michael Garrett Bechtel, and Heechul Yun. 2020. SpectreRewind: Leaking Secrets to Past Instructions. InASHES@CCS. ACM. doi:10.1145/3411504. 3421216

    2020 doi

  33. [42]

    1996.Speculative Execution Based on Value Prediction

    Freddy Gabbay. 1996.Speculative Execution Based on Value Prediction. Technical Report 1080. Technion — Israel Institute of Technology, Electrical Engineering Department

    1996

  34. [43]

    Johann Großschädl, Elisabeth Oswald, Dan Page, and Michael Tunstall. 2009. Side-Channel Analysis of Cryptographic Software via Early-Terminating Multi- plications. InICISC. Springer. doi:10.1007/978-3-642-14423-3_13

    2009 doi

  35. [44]

    Marco Guarnieri, Boris Köpf, Jan Reineke, and Pepe Vila. 2021. Hardware- Software Contracts for Secure Speculation. InIEEE S&P. IEEE. doi:10.1109/ SP40001.2021.00036

    2021

  36. [45]

    Ali Hajiabadi and Trevor E. Carlson. 2024. Providing High-Performance Execution with a Sequential Contract for Cryptographic Programs. arXiv:2406.04290 [cs.CR]

    2024 arXiv

  37. [46]

    Ali Hajiabadi and Trevor E. Carlson. 2025. Cassandra: Efficient Enforcement of Sequential Execution for Cryptographic Programs. InISCA. ACM. doi:10.1145/ 3695053.3731048

    2025

  38. [47]

    2018.Speculative Execution, Variant 4: Speculative Store Bypass

    Jann Horn. 2018.Speculative Execution, Variant 4: Speculative Store Bypass. https://bugs.chromium.org/p/project-zero/issues/detail?id=1528

    2018

  39. [48]

    2018.Bounds Check Bypass / CVE-2017-5753 / INTEL-SA-00088

    Intel. 2018.Bounds Check Bypass / CVE-2017-5753 / INTEL-SA-00088. https: //www.intel.com/content/www/us/en/developer/articles/technical/software- security-guidance/advisory-guidance/bounds-check-bypass.html

    2018

  40. [49]

    2018.Speculative Store Bypass / CVE-2018-3639 / INTEL-SA- 00115

    Intel. 2018.Speculative Store Bypass / CVE-2018-3639 / INTEL-SA- 00115. https://www.intel.com/content/www/us/en/developer/articles/technical/ software-security-guidance/advisory-guidance/speculative-store-bypass.html

    2018

  41. [50]

    2018.Using Intel®Compilers to Mitigate Speculative Execution Side- Channel Issues

    Intel. 2018.Using Intel®Compilers to Mitigate Speculative Execution Side- Channel Issues. https://www.intel.com/content/www/us/en/developer/articles/ troubleshooting/using-intel-compilers-to-mitigate-speculative-execution- side-channel-issues.html

    2018

  42. [51]

    2020.An Optimized Mitigation Approach for Load Value Injection

    Intel. 2020.An Optimized Mitigation Approach for Load Value Injection. https://www.intel.com/content/www/us/en/developer/articles/technical/ software-security-guidance/best-practices/optimized-mitigation-approach- load-value-injection.html

    2020

  43. [52]

    2022.Fast Store Forwarding Predictor

    Intel. 2022.Fast Store Forwarding Predictor. Intel. https://www.intel. com/content/www/us/en/developer/articles/technical/software-security- guidance/technical-documentation/fast-store-forwarding-predictor.html

    2022

  44. [53]

    2025.Data Operand Independent Timing ISA Guidance

    Intel. 2025.Data Operand Independent Timing ISA Guidance. Intel Corporation. https://www.intel.com/content/www/us/en/developer/articles/technical/ software-security-guidance/best-practices/data-operand-independent-timing- isa-guidance.html

    2025

  45. [54]

    2025.Intel®64 and IA-32 Architectures Software Developer’s Manual

    Intel. 2025.Intel®64 and IA-32 Architectures Software Developer’s Manual

    2025

  46. [55]

    2024.The RISC-V Instruction Set Manual, Volume I: User- Level ISA version 20240411

    RISC-V International. 2024.The RISC-V Instruction Set Manual, Volume I: User- Level ISA version 20240411. RISC-V

    2024

  47. [56]

    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: Ban- ishing the Spectre of a Meltdown with Leakage-Free Speculation. InDAC. ACM. doi:10.1145/3316781.3317903

    2019

  48. [57]

    Jason Kim, Jalen Chuang, Daniel Genkin, and Yuval Yarom. 2025. FLOP: Break- ing the Apple M3 CPU via False Load Output Predictions. InUSENIX Security. USENIX Association. https://www.usenix.org/conference/usenixsecurity24/ presentation/chen-boru

    2025

  49. [58]

    Jason Kim, Daniel Genkin, and Yuval Yarom. 2025. SLAP: Data Speculation Attacks via Load Address Prediction on Apple Silicon. InIEEE S&P. IEEE. doi:10. 1109/SP61157.2025.00098

    2025

  50. [59]

    Vladimir Kiriansky and Carl Waldspurger. 2018. Speculative Buffer Overflows: Attacks and Defenses. arXiv:1807.03757 [cs.CR]

    2018 arXiv

  51. [60]

    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. In IEEE S&P. IEEE. doi:10.1109/SP.2019.00002

    2019

  52. [61]

    Paul C. Kocher. 1996. Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems. InCRYPTO. Springer. doi:10.1007/3-540-68697-5_9

    1996 doi

  53. [62]

    Matthew Kolosick, Basavesh Ammanaghatta Shivakumar, Sunjay Cauligi, Marco Patrignani, Marco Vassena, Ranjit Jhala, and Deian Stefan. 2025. Robust Constant- Time Cryptography.Proceedings of the ACM on Programming Languages9, PLDI (2025), 1491–1515. doi:10.1145/3729310

    2025 doi

  54. [63]

    Khasawneh, Chengyu Song, and Nael B

    Esmaeil Mohammadian Koruyeh, Khaled N. Khasawneh, Chengyu Song, and Nael B. Abu-Ghazaleh. 2018. Spectre Returns! Speculation Attacks Using the Return Stack Buffer. InUSENIX WOOT. USENIX Association. https://www. dfence: Fine-Grained Speculation Barriers for Efficient and Effec...

    2018

  55. [64]

    Kha- sawneh, Chengyu Song, and Nael B

    Esmaeil Mohammadian Koruyeh, Shirin Haji Amin Shirazi, Khaled N. Kha- sawneh, Chengyu Song, and Nael B. Abu-Ghazaleh. 2020. SpecCFI: Miti- gating Spectre Attacks using CFI Informed Speculation. InIEEE S&P. IEEE. doi:10.1109/SP40000.2020.00033

    2020

  56. [65]

    2015.Programmer’s Guide for ARMv8-A

    Arm Limited. 2015.Programmer’s Guide for ARMv8-A

    2015

  57. [66]

    2018.Addressing Spectre Variant 1 (CVE-2017-5753) in Software

    Arm Limited. 2018.Addressing Spectre Variant 1 (CVE-2017-5753) in Software. White Paper Version 1.0. https://developer.arm.com/documentation/102820/ latest/

    2018

  58. [67]

    2020.DIT, Data Independent Timing

    Arm Limited. 2020.DIT, Data Independent Timing. Arm Lim- ited. https://developer.arm.com/documentation/ddi0601/2020-12/AArch64- Registers/DIT--Data-Independent-Timing

    2020

  59. [68]

    Lipasti and John Paul Shen

    Mikko H. Lipasti and John Paul Shen. 1996. Exceeding the Dataflow Limit via Value Prediction. InMICRO. IEEE. doi:10.1109/MICRO.1996.566464

    1996

  60. [69]

    Lipasti, Christopher B

    Mikko H. Lipasti, Christopher B. Wilkerson, and John Paul Shen. 1996. Value Locality and Load Value Prediction. InASPLOS. ACM. doi:10.1145/237090.237173

    1996

  61. [70]

    Chen Liu, Abhishek Chakraborty, Nikhil Chawla, and Neer Roggel. 2022. Fre- quency Throttling Side-Channel Attack. InCCS. ACM. doi:10.1145/3548606. 3560682

    2022 doi

  62. [71]

    Giorgi Maisuradze and Christian Rossow. 2018. ret2spec: Speculative Execution Using Return Stack Buffers. InCCS. ACM. doi:10.1145/3243734.3243761

    2018

  63. [72]

    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. InIEEE S&P. IEEE. doi:10.1109/SP46215.2023.10179391

    2023

  64. [73]

    Marco Patrignani and Marco Guarnieri. 2021. Exorcising Spectres with Secure Compilers. InCCS. ACM. doi:10.1145/3460120.3484534

    2021

  65. [74]

    Hany Ragab, Enrico Barberis, Herbert Bos, and Cristiano Giuffrida. 2021. Rage against the Machine Clear: A Systematic Analysis of Machine Clears and Their Im- plications for Transient Execution Attacks. InUSENIX Security. USENIX Associ- ation. https://www.usenix.org/conference...

    2021

  66. [75]

    Allison Randal. 2023. This is How You Lose the Transient Execution War. arXiv:2309.03376 [cs.CR]

    2023 arXiv

  67. [76]

    Tullsen, and Ashish Venkat

    Xida Ren, Logan Moody, Mohammadkazem Taram, Matthew Jordan, Dean M. Tullsen, and Ashish Venkat. 2021. I See Dead𝜇ops: Leaking Secrets via Intel/AMD Micro-Op Caches. InISCA. IEEE. doi:10.1109/ISCA52012.2021.00036

    2021

  68. [77]

    Fadiheh, Thore Tie- mann, Jonah Heller, Thomas Eisenbarth, Dominik Stoffel, and Wolfgang Kunz

    Philipp Schmitz, Tobias Jauch, Alex Wezel, Mohammad R. Fadiheh, Thore Tie- mann, Jonah Heller, Thomas Eisenbarth, Dominik Stoffel, and Wolfgang Kunz

  69. [78]

    Michael Schwarz, Martin Schwarzl, Moritz Lipp, Jon Masters, and Daniel Gruss

  70. [79]

    Adi Shamir. 1979. How to Share a Secret.Commun. ACM22, 11 (1979). doi:10. 1145/359168.359176

    1979

  71. [80]

    arXiv:2312.08156 [cs.CR]

    Okapi: Efficiently Safeguarding Speculative Data Accesses in Sandboxed Environments. arXiv:2312.08156 [cs.CR]

    arXiv

  72. [81]

    Mohammadkazem Taram, Ashish Venkat, and Dean M. Tullsen. 2019. Context- Sensitive Fencing: Securing Speculative Execution via Microcode Customization. InASPLOS. ACM. doi:10.1145/3297858.3304060

    2019

  73. [82]

    Tullsen, and Deian Stefan

    Marco Vassena, Craig Disselkoen, Klaus von Gleissenthall, Sunjay Cauligi, Rami Gökhan Kici, Ranjit Jhala, Dean M. Tullsen, and Deian Stefan. 2021. Automatically eliminating speculative leaks from cryptographic code with blade.Proceedings of the ACM on Programming Languages5, P...

    2021 doi

  74. [83]

    Fletcher, and David Kohlbrenner

    Jose Rodrigo Sanchez Vicarte, Michael Flanders, Riccardo Paccagnella, Grant Garrett-Grossman, Adam Morrison, Christopher W. Fletcher, and David Kohlbrenner. 2022. Augury: Using Data Memory-Dependent Prefetchers to Leak Data at Rest. InIEEE S&P. IEEE. doi:10.1109/SP46214.2022.9833570

    2022

  75. [84]

    Fletcher, Ling Ren, Xiangyao Yu, and Srinivas Devadas

    Emil Stefanov, Marten van Dijk, Elaine Shi, Christopher W. Fletcher, Ling Ren, Xiangyao Yu, and Srinivas Devadas. 2013. Path ORAM: An Extremely Simple Oblivious RAM Protocol. InCCS. ACM, 299–310. doi:10.1145/2508859.2516660

    2013

  76. [85]

    Wenisch, and Baris Kasikci

    Ofir Weisse, Ian Neal, Kevin Loughlin, Thomas F. Wenisch, and Baris Kasikci

  77. [86]

    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. InCCS. ACM. doi:10.1145/3658644.3690319

    2024

  78. [87]

    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. InIEEE S&P. IEEE. doi:10.1109/SP54263.2024.00047

    2024

  79. [88]

    Fletcher, and David Kohlbrenner

    Yingchen Wang, Riccardo Paccagnella, Elizabeth Tang He, Hovav Shacham, Christopher W. Fletcher, and David Kohlbrenner. 2022. Hertzbleed: Turn- ing Power Side-Channel Attacks into Remote Timing Attacks on X86. In USENIX Security. USENIX Association. https://www.usenix.org/confe...

    2022

  80. [89]

    Fletcher

    Jiyong Yu, Lucas Hsiung, Mohamad El Hajj, and Christopher W. Fletcher

  81. [90]

    NDA: Preventing Speculative Execution Attacks at Their Source. InMICRO. ACM. doi:10.1145/3352460.3358306

  82. [91]

    Zhiyuan Zhang, Gilles Barthe, Chitchanok Chuengsatiansup, Peter Schwabe, and Yuval Yarom. 2023. Ultimate SLH: Taking Speculative Load Hardening to the Next Level. InUSENIX Security. USENIX Association. https://www.usenix. org/conference/usenixsecurity23/presentation/zhang-zhiy...

    2023 doi

  83. [93]

    Gürkaynak, Luca Benini, and Gernot Heiser

    Nils Wistoff, Moritz Schneider, Frank K. Gürkaynak, Luca Benini, and Gernot Heiser. 2021. Microarchitectural Timing Channels and their Prevention on an Open-Source 64-bit RISC-V Core. InDATE. IEEE. doi:10.23919/DATE51398.2021. 9474214

    2021

  84. [95]

    Data Oblivious ISA Extensions for Side Channel-Resistant and High Performance Computing. InNDSS. https://www.ndss-symposium.org/ndss- paper/data-oblivious-isa-extensions-for-side-channel-resistant-and-high- performance-computing/

  85. [96]

    Fletcher

    Jiyong Yu, Mengjia Yan, Artem Khyzha, Adam Morrison, Josep Torrellas, and Christopher W. Fletcher. 2019. Speculative Taint Tracking (STT): A Comprehen- sive Protection for Speculatively Accessed Data. InMICRO. ACM. doi:10.1145/ 3352460.3358274

    2019

  86. [98]

    - Case[ TIf]

    In turn, this conclusion follows from Lemma 13 and 𝑟1[x←JEK 𝑟1]∼⊥𝑟2[x←JEK 𝑟2]. - Case[ TIf]. In this case, we can assume that the type deriva- tion is the one below: TSeq TIf Γ1⊢E:𝜎Φ|Γ 1⊢P 1 :Γ 2 Φ|Γ 1⊢P 2 :Γ 2 Φ|Γ 1⊢ifEthenP 1 elseP 2 fi:Γ 2 𝜋2 𝜋⊲Φ|Γ 1⊢ifEthenP 1 elseP 2 fi;P...

  87. [99]

    When this is the case, the claim follows from𝜇1≃⊥ Γ 𝜇2 and Γ(a)=L

    We go by cases on(b,𝑚)=(a,𝑛) : when this is not the case, the claim is a direct consequence of the IH. When this is the case, the claim follows from𝜇1≃⊥ Γ 𝜇2 and Γ(a)=L. □ Lemma 17.If𝑟 1≃𝛽 Γ 𝑟2, then𝑟 1[x←v 1]≃⊤ Γ[x←(𝜏,H)] 𝑟2[x←v 2]. Proof.The assumptions are 𝑟1≃𝛽 Γ 𝑟2 (H1) Th...

  88. [100]

    From the IH—whose assumptions are discharged by (H1) and 𝑚1≃𝛽 Γ 𝑚2—we deduce that (𝜇′ 1,𝑚 1)≃ Γ(𝜇′ 2,𝑚 2) Therefore, the conclusion is a consequence of Lemma 20

    From the definition of≃𝛽 Γ, we deduce that 𝜇2 =[(a,𝑛)↦→v 2]:𝜇 ′ 2 (H) 𝜇′ 1≃𝛽 Γ 𝜇′ 2 (H1) 𝛽=⊥⇒Γ(a)=L⇒v 1 =v 2 (H2) We have to establish: ([(a,𝑛)↦→v 1]:𝜇 ′ 1,𝑚 1)≃ Γ([(a,𝑛)↦→v 2]:𝜇 ′ 2,𝑚 2), which means establishing that: (𝜇′ 1,𝑚 1)[(a,𝑛)←v 1]≃ Γ(𝜇′ 2,𝑚 2)[(a,𝑛)←v 2]. From the I...

  89. [2019]

    InESORICS

    NetSpectre: Read Arbitrary Memory over Network. InESORICS. Springer. doi:10.1007/978-3-030-29959-0_14

    doi

  90. [2024]

    In USENIX Security

    SpecLFB: Eliminating Cache Side Channels in Speculative Executions. In USENIX Security. USENIX Association. https://www.usenix.org/conference/ usenixsecurity24/presentation/cheng-xiaoyu

Pith tools

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