Pith. sign in

REVIEW 3 major objections 4 minor 117 references

Comprehensive Kernel Safety in the Spectre Era: Mitigations and Performance Evaluation (Extended Version)

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

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

Pith's one-line read This paper proves that any kernel safe against ordinary attackers can be automatically transformed to be safe against Spectre-style, side-channel-equipped attackers, and it implements three such transformations whose optimized version…

desk verdict Solid formal KASLR-safety result with three fence transformations; 'comprehensive' overclaims because RSB/Phantom are excluded, but the paper is honest about it and merits refereeing. read the letter →

arxiv 2411.18094 v2 pith:5VTGFYP3 submitted 2024-11-27 cs.CR

Davide Davoli , Martin Avanzini , Tamara Rezk This is my paper · ORCID
classification cs.CR
keywords kernelsafetyspeculativeexecutionSpectrelayoutrandomizationKASLRprogramtransformationside-channelnon-interferencesystemcalls
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

This paper tries to establish that kernel address-space layout randomization, which formally protects ordinary programs under restricted conditions, also gives a probabilistic safety guarantee to kernels with system calls when attackers are classic unprivileged user programs, even if kernel code uses pointer arithmetic and indirect jumps. It then argues that this guarantee collapses when attackers can use side channels and speculative execution: probing kernel memory in transient execution does not crash the system, so randomization can be bypassed. The paper's central positive result is a reduction theorem: any kernel that is safe against classic attackers can be automatically transformed so that it is safe against speculative attackers, including Spectre v1, v2, and v4 mechanisms, while remaining indistinguishable to user programs. Three such transformations are proved sound; the optimized one, which inserts speculation barriers only where a static analysis says they are needed, is reported to keep overhead below 5 percent on compute-heavy workloads such as SPEC CPU 2017 and several I/O benchmarks, at the price of 3x to 10x slowdowns on system-call-heavy tests like UnixBench.

What carries the argument

The load-bearing object is the instrumented speculative semantics, in which each speculative step is driven by a directive (branch direction, branch target, or store-to-load forwarding) and emits an observation (branch taken, accessed address, jump target, or backtrack), modeling a side channel while kernel safety is defined as absence of a transition to unsafe, meaning a system call touches or invokes an object outside its declared capabilities. The transformations work by inserting speculation barriers that resolve outstanding speculation and by rewriting indirect calls to a jump instruction whose target cannot be speculatively predicted, called scall in the model. The optimized transformation carries two flags through a static analysis, tracking whether the current instruction could be reached under mis-speculation and whether the write buffer is empty, so that redundant fences can be omitted. Theorem 3 is the formal workhorse: it makes speculative kernel safety a corollary of classic kernel safety once the two conditions on the transformation hold.

What would settle it

Run the transformed kernel on a CPU that permits return-stack-buffer or Phantom-style speculation, which the paper explicitly leaves out of scope, and try a system call that transiently calls a kernel procedure outside its capability set; if the call executes and its address leak reaches the cache, the speculative kernel safety guarantee fails exactly where the model stops.

Watch

Extended reading notes

Core claim

The central discovery is that speculative kernel safety can be reduced to classic kernel safety by a semantics-preserving program transformation. Stated as Theorem 3: if a system is kernel safe, and a transformation both imposes speculative kernel safety and preserves system call semantics, then the transformed system is speculative kernel safe and semantically equivalent to the original. The three exhibited transformations meet these conditions by inserting speculation barriers before any instruction that could transiently violate a capability and by replacing ordinary indirect calls with non-speculable jumps. The transformations differ in how many fences they insert: the baseline fences every potentially unsafe operation, the optimized version uses a static analysis of mis-speculation and buffer state to drop redundant fences, and the third fences after every speculation source. The empirical claim is that the optimized transformation costs less than 5 percent on compute-heavy and several I/O workloads, while system-call-heavy workloads see 3x to 10x overhead.

Load-bearing premise

The proof depends on the CPU behaving exactly as the model does: user-space execution cannot influence kernel indirect-branch prediction, a non-speculable jump instruction exists, and only the three modeled speculation mechanisms (branch direction, branch target, store-to-load forwarding) are present.

Editorial extensions

If this is right

  • A kernel proved safe against ordinary attackers can be deployed with any of the three transformations and be formally safe against speculative attackers, without user programs observing any difference.
  • Layout randomization alone cannot be relied on for kernel safety in the Spectre era; the side-channel layout non-interference condition restores safety, but when it holds randomization is redundant.
  • The optimized transformation is cheap enough for production on compute-heavy and many I/O workloads, with overhead under 5 percent, but system-call-heavy workloads such as process creation and inter-process communication pay 3x to 10x.
  • Existing mitigations reviewed in the paper, including speculative load hardening, speculative constant-time, taint tracking, and the compiler side-effect suppression pass, do not uniformly stop the three representative attacks, whereas the new transformations do.
  • The reduction theorem extends in principle to additional speculation mechanisms such as load value injection and return-address speculation, but the transformations would need to be extended to block those additional sources.

Reading between the lines

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

  • The same reduction could apply to hypervisor-level privileged interfaces, since the model abstracts over the kernel; a hypercall-based system satisfying classic safety would inherit the speculative safety guarantee.
  • Because system-call-heavy overhead dominates the cost, the practical research target implied by the paper is a smarter static analysis that proves more reaches of kernel code fence-free, rather than faster fences.
  • The hidden hardware dependency is the existence of a true non-speculable jump instruction; if future CPUs expose one cheaply, the approach becomes substantially more attractive than today's retpoline and eIBRS combination.
  • A certification tool that checks whether every potentially unsafe instruction in a hardened kernel binary is fence-dominated would let existing kernels be audited against the paper's model without recompiling.
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 studies kernel safety in two threat models. In the classic (non-speculative) model, it proves that layout randomization gives a probabilistic kernel-safety guarantee for systems whose system calls satisfy a layout non-interference condition, relaxing the syntactic restrictions of Abadi et al. In the speculative model, it argues that layout randomization alone cannot restore safety, introduces a side-channel layout non-interference condition that suffices for speculative kernel safety, and proposes three program transformations (η, ψ, θ) that turn a kernel-safe system into a semantically equivalent speculative-kernel-safe system. The transformations are implemented as an LLVM pass and evaluated on SPEC CPU 2017, UnixBench, and several I/O workloads.

Significance. The paper makes a substantial formal contribution: it gives a clean probabilistic semantics for KASLR with a non-trivial bound δµ,σ, it identifies layout non-interference as the right classic-model assumption, and it reduces speculative kernel safety to classic kernel safety via program transformations. The three transformations are concrete, the LLVM implementation is open source, and the performance evaluation covers both compute-heavy and syscall-heavy workloads with a useful comparison between eIBRS and retpoline. The explicit admission in Section 10 that RSB speculation remains out of scope is honest, but it directly limits the practical reach of the title and abstract claims.

major comments (3)
  1. [Section 4 / Section 10 / Figure 3] The formal safety guarantee and the transformations cover only PHT, BTB, and STL speculation. Section 4 explicitly excludes return-address (RSB) and Phantom speculation, and the language has no return instruction: procedures return through the [Pop] rule, which none of η, ψ, or θ fences or replaces. Section 10 then states that systems protected with these mitigations 'may still be vulnerable to attacks relying on RSB speculation.' Since Retbleed-style RSB prediction can transiently redirect returns even with eIBRS and retpoline, Theorem 3 and Lemmas 4-6 do not establish speculative kernel safety for real CPUs. The title's 'Comprehensive' and the abstract's 'guarantee speculative kernel safety in the Spectre era' therefore overstate the result. The authors should either extend the model and transformations to returns or systematically qualify the central claims to the PHT/BTB/STL model.
  2. [Section 8, Lemmas 4-6] The soundness proofs of the three transformations are only sketched. The proof of Lemma 5 says that it relies on 'a form of subject reduction and of soundness of our static analysis' plus 'other technical invariant properties', but these invariants are never stated, and the appendix does not contain proofs for Lemmas 4-6 (Appendix A.2 covers Section 6 only). Since the applicability of Theorem 3 depends entirely on these lemmas, the central formal claim of the paper is not fully verified in the manuscript. The authors should provide complete proofs, a machine-checked formalization, or a precise statement of the invariants with a detailed proof outline.
  3. [Section 6.3] The claim that layout randomization 'cannot be restored' in the speculative threat model is supported only by two example gadgets and a reference to BlindSide, not by a formal theorem. The examples show that certain systems violate speculative kernel safety, but they do not show that no layout distribution and no system satisfying the paper's assumptions can have a probabilistic guarantee. Since the demise of KASLR is presented as one of the paper's main contributions, the authors should state and prove a concrete impossibility result, for example: for any layout distribution µ and any sufficiently expressive kernel, there exists a speculative attacker that learns a kernel address through the model's observations and then triggers an unsafe access. Without such a theorem, the broad statement in the introduction and abstract is not established.
minor comments (4)
  1. [Abstract] The sentence 'We show that kernel safety cannot be restored for attackers capable of using side-channels and speculative execution' appears twice; one occurrence should be removed.
  2. [Section 9, final remarks] The sentence claiming that ψ's overhead 'never exceeds 5%' should explicitly say 'on SPEC CPU 2017 and on SQLite/CrossDB/grep/vbench', because Tables 5-6 show about 3.5x overhead on Apache, 4.1x on nginx, and 3.3x on AES for the same transformation.
  3. [Section 3.1 and elsewhere] There are several typos: 'idenitifiers' in Section 3.1, 'specualtive' in Section 8, 'F ormal' in Section 10, and 'ngninx' in Tables 5-6. These should be corrected.
  4. [Figure 14] The y-axis origin is set to 0.975 in Figures 14a-14b, which visually magnifies differences below 2.5%; the caption should state this explicitly so that the normalized run times are not misinterpreted.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the main theorems are proved from the paper's explicit speculative semantics, and the stated exclusions and hardware assumptions are scope limits, not fitted inputs.

full rationale

The claimed derivation chain is self-contained rather than circular. Theorem 3 is a conditional statement: it holds for any transformation satisfying Definition 6 (system call semantics preservation) and Definition 7 (imposition of speculative kernel safety), and Lemmas 4-6 establish those conditions by induction over the speculative semantics of Sections 6.1.1 and 8, not by assuming the conclusion. The probabilistic bound in Theorem 1 is not a fitted prediction: the parameter delta_mu_sigma is defined directly as the minimum probability that a probe for an unallocated kernel address fails, and the proof bounds the probability of unsafe by 1 - delta_mu_sigma via Lemma 2; no value is calibrated afterward to make the result come out. The only self-reference is to the companion CCS paper [30] as provenance for the baseline transformation; because the transformation eta is defined in Figure 11 and its soundness is argued in the text, that citation is not load-bearing. The paper explicitly scopes out return-address speculation (Retbleed) and Phantom speculation in Section 4, and acknowledges in Section 10 that protected systems 'may still be vulnerable to attacks relying on RSB speculation'; this is an honest threat-model limitation, not a circular derivation. Likewise, the non-speculable 'scall' instruction is introduced under the stated hardware assumption of fully effective retpoline or eIBRS with BHI_DIS_S, an assumption the paper acknowledges rather than derives. Nothing in the paper reduces a claimed result to its own input by construction, so the circularity score is minimal.

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

The central claims rest on a detailed operational model of speculation and on hardware features whose effectiveness is assumed (eIBRS/retpoline, BHI_DIS_S, PTI, IBT, SMAP, SMEP). No numeric free parameters are fitted. The probabilistic bound δµ,σ is defined directly from the layout distribution, not fitted. The three transformations are proven sound only inside the modeled speculation mechanisms.

assumptions (5)
  • domain assumption Speculative execution is fully captured by PHT, BTB and STL directives; RSB, LVI, and Phantom speculation are out of scope.
    Section 4 and Section 8 final remarks. All formal results and the three transformations are validated only against these speculation mechanisms; Retbleed or Phantom attacks would fall outside the model.
  • domain assumption The victim CPU provides eIBRS (or fully effective retpoline) and BHI_DIS_S, so that indirect branch targets cannot be influenced by user-space execution, and the scall instruction is non-predictable.
    Assumed in Section 4 ('we assume that the victim's machine supports a specific class of indirect branch instructions...') and relied on by Theorem 3 to guarantee that scall blocks BTB speculation.
  • domain assumption Layout non-interference of system calls (Definition 2) is a prerequisite for the probabilistic kernel-safety result (Theorem 1).
    Theorem 1 is conditional on layout non-interference; systems with layout-dependent behavior (e.g., the motivating recv/send example) are excluded from the guarantee.
  • domain assumption Side-channel layout non-interference (Definition 4) is assumed for Theorem 2, and requires a kernel address space large enough to move any object (κk ≥ sum of sizes + 2*max size).
    Theorem 2 is conditional on this non-interference property; the paper notes it is too restrictive for realistic syscalls that access memory dynamically.
  • domain assumption The attacker model includes IBT, PTI, SMAP, SMEP and a W^X memory policy; these hardware features behave as specified in the operational rules.
    Section 4: the paper assumes these protections are present and models them via side conditions in the semantics; the security theorems are relative to this model.
invented entities (2)
  • fence instruction (modeled lfence) independent evidence
    purpose: Stops speculative execution before potentially unsafe memory or call operations; used by transformations η, ψ, θ.
    lfence exists on x86 and is the real instruction used in the implementation; its modeled semantics (requiring mis-speculation flag = ⊥) is an abstraction of the real timing barrier.
  • scall instruction (speculative-safe call) independent evidence
    purpose: Indirect call whose target cannot be speculated; models retpoline thunks or eIBRS-hardened indirect branches.
    Implemented in the LLVM pass via Linux retpoline thunks or eIBRS; real-world existence of these mechanisms gives independent support.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Comprehensive Kernel Safety in the Spectre Era: Mitigations and Performance Evaluation (Extended Version)." pith.science (2026). https://pith.science/paper/5VTGFYP3

@misc{pith2026241118094,
  author       = {Pith},
  title        = {Pith review of: Comprehensive Kernel Safety in the Spectre Era: Mitigations and Performance Evaluation (Extended Version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/5VTGFYP3}},
  note         = {Machine review of arXiv:2411.18094}
}
read the original abstract

The efficacy of address space layout randomization has been formally demonstrated in a shared-memory model by Abadi et al., contingent on specific assumptions about victim programs. However, modern operating systems, implementing layout randomization in the kernel, diverge from these assumptions and operate on a separate memory model with communication through system calls. In this work, we relax Abadi et al.'s language assumptions while demonstrating that layout randomization offers a comparable safety guarantee in a system with memory separation. However, in practice, speculative execution and side-channels are recognized threats to layout randomization. We show that kernel safety cannot be restored for attackers capable of using side-channels and speculative execution, and introduce enforcement mechanisms that can guarantee speculative kernel safety for safe system calls in the Spectre era. We implement three suitable mechanisms and we evaluate their performance overhead on the Linux kernel.

Figures

Figures reproduced from arXiv: 2411.18094 by the authors.

Figure 1
Figure 1. System Calls vulnerable to memory corruption [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Syntax of the language. Here, v is a value, x a register, a an array identifier, f a procedure identifier, and op is an operator. Addr, modeled as non-negative integers, and an undefined value null. Within expressions, x ∈ Reg ranges over registers, a ∈ ArrId and f ∈ ProcId over array and procedure identifiers, and op ∈ Ops over operators. Identifiers Id ≜ ArrId ⊎ ProcId are mapped to addresses at runtime, as govern… view at source ↗
Figure 3
Figure 3. Semantics w.r.t. system σ = (τ, γ, ξ), first part. Register maps Besides memory locations, our program can also manipulate the content of registers. In our semantics, we model registers through functions ρ : Reg → Val, associating register identifiers to their value. As for memories, the notation ρ[x ← v] denotes the register map that is pointwise identical to ρ, except for the register x, which is mapped to the val… view at source ↗
Figures from the paper (19 more)
Figure 4
Figure 4. Figure 4: Semantics w.r.t. system σ = (τ, γ, ξ), second part. indicating that, w.r.t. system σ, configuration ϕ reduces to χ in one step, under layout w. The reduction rules are defined in Figures 3 and 4. Rule [Load] implements a successful memory load x := *E. Expression E is …
Figure 5
Figure 5. Figure 5: Speculative semantics, excerpt. Some illustrative rules of the semantics are given in [PITH_FULL_IMAGE:figures/full_fig_p017_5.png]
Figure 6
Figure 6. Figure 6: Speculative semantics, speculative call instructions. [PITH_FULL_IMAGE:figures/full_fig_p018_6.png]
Figure 8
Figure 8. Figure 8: Semantics for speculative attackers, excerpt. [PITH_FULL_IMAGE:figures/full_fig_p019_8.png]
Figure 9
Figure 9. Figure 9: Attacks witnessing that σ does not enjoy speculative kernel safety. Theorem 2. Under the assumption κk ≥ P id∈Idk size(id) + 2 · maxid∈Idk size(id), if a system σ is side-channel layout non-interfering, then it is speculative kernel safe. Proof Sketch. As for Theorem 1…
Figure 10
Figure 10. Figure 10: Speculative semantics, additional constructs. [PITH_FULL_IMAGE:figures/full_fig_p027_10.png]
Figure 11
Figure 11. Figure 11: Simple fencing transformation SESES does, it prevents BTB speculation by rewriting ordinary call instructions with non-speculating call instructions. With η, any ongoing speculation is stopped before executing potentially unsafe op￾erations (including non-speculative …
Figure 12
Figure 12. Figure 12: Optimized fencing transformation. When there is no risk of ambiguity, we use the notation [PITH_FULL_IMAGE:figures/full_fig_p028_12.png]
Figure 13
Figure 13. Figure 13: Speculation-blocking transformation. Finally, the flag m is set to ⊤ and e to ⊥ when returning from an indirect call, due to the lack of information on the called function. Our optimizations do not impact the security of the transformation ψ, as expressed by the follo…
Figure 14
Figure 14. Figure 14: Overheads of the different transformations of the kernel. In the figures, the scale of the [PITH_FULL_IMAGE:figures/full_fig_p033_14.png]
Figure 15
Figure 15. Figure 15: Speculative rules for Cmd and a system σ = (τ, γ, ξ), Part I. A.2 Appendix for Section 6 Kernel-mode stack In this section, the predicate ks additionally requires that all the commands within the stack belong to Cmd, i.e., that they do not contain spec on ·, poison(·)…
Figure 16
Figure 16. Figure 16: Speculative rules for Cmd and a system σ = (τ, γ, ξ), Part II. 60 [PITH_FULL_IMAGE:figures/full_fig_p060_16.png]
Figure 17
Figure 17. Figure 17: Speculative rules for Cmd and a system σ = (τ, γ, ξ), Part III. 61 [PITH_FULL_IMAGE:figures/full_fig_p061_17.png]
Figure 18
Figure 18. Figure 18: Semantics of the non-standard constructs of [PITH_FULL_IMAGE:figures/full_fig_p062_18.png]
Figure 19
Figure 19. Figure 19: Semantics of standard construct of SpAdv for the system σ = (τ, γ, ξ), part I. 63 [PITH_FULL_IMAGE:figures/full_fig_p063_19.png]
Figure 20
Figure 20. Figure 20: Semantics of standard construct of SpAdv for the system σ = (τ, γ, ξ), part II. - Case i + 1. The claim now states: ∀i.∀v.([p ′ 7→ v] : µ, m) i+1(p) = v, ⊥ ⇒ ([p ′ 7→ v] : µ, m) i+1(p) = ([p ′ 7→ v] : µ, m) 0 (p). Fix i, v and assume ([p ′ 7→ v] : µ, m) i+1(p) = v, ⊥,…
Figure 21
Figure 21. Figure 21: Well-formedness relation with respect to a system [PITH_FULL_IMAGE:figures/full_fig_p077_21.png]
Figure 22
Figure 22. Figure 22: Well-formedness relation with respect to a system [PITH_FULL_IMAGE:figures/full_fig_p077_22.png]
Figure 23
Figure 23. Figure 23: Well-formedness relation with respect to a system [PITH_FULL_IMAGE:figures/full_fig_p078_23.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

117 extracted references · 77 canonical work pages

  1. [1]

    On layout randomization for arrays and functions

    Mart ´ ın Abadi and J´ er´ emy Planul. On layout randomization for arrays and functions. InPrinciples of Security and Trust, pages 167–185, Berlin, Heidelberg, 2013. Springer. ISBN 978-3-642-36830- 1

    2013

  2. [2]

    Mart ´ ın Abadi and Gordon D. Plotkin. On protection by layout randomization.ACM Trans. Inf. Syst. Secur., 15(2), jul 2012. ISSN 1094-9224

    2012

  3. [3]

    Control-flow integrity

    Mart ´ ın Abadi, Mihai Budiu,´Ulfar Erlingsson, and Jay Ligatti. Control-flow integrity. In Pro- ceedings of the 12th ACM Conference on Computer and Communications Security , page 340–353, New York, NY, USA, 2005. ACM. ISBN 1595932267

    2005

  4. [4]

    Plotkin.Layout Randomization and Nondetermin- ism, pages 1–39

    Mart ´ ın Abadi, J´ er´ emy Planul, and Gordon D. Plotkin.Layout Randomization and Nondetermin- ism, pages 1–39. Springer International Publishing, Berlin, Heidelberg, 2014

    2014

  5. [5]

    Technical guidance for mitigating branch type confusion

    AMD. Technical guidance for mitigating branch type confusion. Technical report, AMD, November 2022. URL https://www.amd.com/content/dam/amd/en/documents/resources/ technical-guidance-for-mitigating-branch-type-confusion.pdf . White Paper

    2022

  6. [6]

    Enforcing fine-grained constant-time policies

    Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Gr´ egoire, Vincent Laporte, and Swarn Priya. Enforcing fine-grained constant-time policies. In Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security , page 83–96, New York, NY, USA, 2022. ACM. ISBN 9781450394505

    2022

  7. [7]

    The meaning of memory safety

    Arthur Azevedo de Amorim, C˘ at˘ alin Hrit ¸cu, and Benjamin C Pierce. The meaning of memory safety. In Proceedings of Principles of Security and Trust: 7th International Conference , pages 79–105, Springer, 2018. Springer Berlin, Heidelberg

    2018

  8. [8]

    Branch history injection: On the effectiveness of hardware mitigations against Cross-Privilege spectre-v2 attacks

    Enrico Barberis, Pietro Frigo, Marius Muench, Herbert Bos, and Cristiano Giuffrida. Branch history injection: On the effectiveness of hardware mitigations against Cross-Privilege spectre-v2 attacks. In 31st USENIX Security Symposium (USENIX Security’22) , pages 971–988, Boston, MA, August 2022. USENIX Association

    2022

Show all 117 references
  1. [9]

    System-level non-interference for constant-time cryptography

    Gilles Barthe, Gustavo Betarte, Juan Campo, Carlos Luna, and David Pichardie. System-level non-interference for constant-time cryptography. In Proceedings of the 2014 ACM SIGSAC Con- ference on Computer and Communications Security, page 1267–1279, New York, NY, USA, 2014. ACM

    2014

  2. [10]

    High-assurance cryptography in the spectre era

    Gilles Barthe, Sunjay Cauligi, Benjamin Gr´ egoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, and Peter Schwabe. High-assurance cryptography in the spectre era. In 2021 IEEE Symposium on Security and Privacy (SP) , pages 1884–1901, New York, NY, USA,

    2021

  3. [11]

    Frans Kaashoek

    Jonathan Behrens, Adam Belay, and M. Frans Kaashoek. Performance evolution of mitigating transient execution attacks. In Proceedings of the Seventeenth European Conference on Computer Systems, page 251–265, New York, NY, USA, 2022. ACM. ISBN 9781450391627. 38

    2022

  4. [12]

    Berger and Benjamin G

    Emery D. Berger and Benjamin G. Zorn. Diehard: Probabilistic memory safety for unsafe lan- guages. In Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation , page 158–168, New York, NY, USA, 2006. ACM. ISBN 1595933204

    2006

  5. [13]

    Understanding the Linux Kernel: from I/O ports to process management

    Daniel P Bovet and Marco Cesati. Understanding the Linux Kernel: from I/O ports to process management. ” O’Reilly Media, Inc.”, 2005

    2005

  6. [14]

    Kaslr: Break it, fix it, repeat

    Claudio Canella, Michael Schwarz, Martin Haubenwallner, Martin Schwarzl, and Daniel Gruss. Kaslr: Break it, fix it, repeat. In Proceedings of the 15th ACM Asia Conference on Computer and Communications Security, page 481–493, New York, NY, USA, 2020. ACM. ISBN 9781450367509

    2020

  7. [15]

    Speculative load hardening, Sep 2018

    Chandler Carruth. Speculative load hardening, Sep 2018. URL https://llvm.org/docs/ SpeculativeLoadHardening.html

    2018

  8. [16]

    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. Constant-time foundations for the new spectre era. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation , page 9...

    2020

  9. [17]

    A systematic study of elastic objects in kernel exploitation

    Yueqi Chen, Zhenpeng Lin, and Xinyu Xing. A systematic study of elastic objects in kernel exploitation. In Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communi- cations Security, page 1165–1184, New York, NY, USA, 2020. ACM. ISBN 9781450370899

    2020

  10. [18]

    Speculative privacy tracking (spt): Leaking information from speculative execution without compromising privacy

    Rutvik Choudhary, Jiyong Yu, Christopher Fletcher, and Adam Morrison. Speculative privacy tracking (spt): Leaking information from speculative execution without compromising privacy. In MICRO-54: 54th Annual IEEE/ACM International Symposium on Microarchitecture , page 607–622,...

    2021

  11. [19]

    Gaidis, Vaggelis Atlidakis, and Vasileios P

    Neophytos Christou, Alexander J. Gaidis, Vaggelis Atlidakis, and Vasileios P. Kemerlis. Eclipse: Preventing speculative memory-error abuse with artificial data dependencies. In Proceedings of the 2024 ACM SIGSAC Conference on Computer and Communications Security , CCS ’24, New...

    2024

  12. [20]

    Supervisor mode access prevention, 2012

    Jonathan Corbet. Supervisor mode access prevention, 2012. URL https://lwn.net/Articles/ 517475/

    2012

  13. [21]

    Intel analysis of speculative execution side channels

    Intel Corporation. Intel analysis of speculative execution side channels. Technical re- port, Intel Corporation, May 2018. URL https://www.intel.com/content/www/us/en/ content-details/671163/intel-analysis-of-speculative-execution-side-channels. html. White Paper

    2018

  14. [22]

    Indirect branch restricted speculation, 2018

    Intel Corporation. Indirect branch restricted speculation, 2018. URL https://www.intel. com/content/www/us/en/developer/articles/technical/software-security-guidance/ technical-documentation/indirect-branch-restricted-speculation.html

    2018

  15. [23]

    Retpoline: A branch target injection mitigation, 2018

    Intel Corporation. Retpoline: A branch target injection mitigation, 2018. URL https://www.intel.com/content/dam/develop/external/us/en/documents/ retpoline-a-branch-target-injection-mitigation.pdf

    2018

  16. [24]

    Branch history injection and intra-mode branch target injection / cve-2022-0001, cve-2022-0002 / intel-sa-00598

    Intel Corporation. Branch history injection and intra-mode branch target injection / cve-2022-0001, cve-2022-0002 / intel-sa-00598. Technical report, Intel Corporation, May

    2022

  17. [25]

    Affected processors: Guidance for security issues on intel ® processors,

    Intel Corporation. Affected processors: Guidance for security issues on intel ® processors,

  18. [26]

    Bench test, 2024

    CrossDB. Bench test, 2024. URL https://crossdb.org/get-started/bench/

    2024

  19. [27]

    cryptsetup, 2025

    cryptsetup Group. cryptsetup, 2025. URL https://gitlab.com/cryptsetup/cryptsetup

    2025

  20. [28]

    ProSpeCT: Provably secure speculation for the Constant-Time policy

    Lesly-Ann Daniel, Marton Bognar, Job Noorman, S´ ebastien Bardin, Tamara Rezk, and Frank Piessens. ProSpeCT: Provably secure speculation for the Constant-Time policy. In 32nd USENIX Security Symposium (USENIX Security 23) , pages 7161–7178, Anaheim, CA, August 2023. USENIX Ass...

    2023

  21. [29]

    Comprehensive kernel safety in the spectre era, 2024

    Davide Davoli. Comprehensive kernel safety in the spectre era, 2024. URL https://gitlab. inria.fr/ddavoli/comprehensive-kernel-safety-in-the-spectre-era

    2024

  22. [30]

    On kernel’s safety in the spectre era (and kaslr is formally dead)

    Davide Davoli, Martin Avanzini, and Tamara Rezk. On kernel’s safety in the spectre era (and kaslr is formally dead). In Proceedings of the 2024 ACM SIGSAC Conference on Computer and Communications Security, CCS 2024, USA, October 14-18, 2023 , New York, NY, USA, 2024. ACM

    2024

  23. [31]

    Openbsd 6.3, Oct 2017

    Theo de Raadt. Openbsd 6.3, Oct 2017. URL https://www.openbsd.org/33.html

    2017

  24. [32]

    Kernel address space layout randomization, 2013

    Jake Edge. Kernel address space layout randomization, 2013. URL https://lwn.net/Articles/ 569635/

    2013

  25. [33]

    Jump over aslr: attacking branch predictors to bypass aslr

    Dmitry Evtyushkin, Dmitry Ponomarev, and Nael Abu-Ghazaleh. Jump over aslr: attacking branch predictors to bypass aslr. In The 49th Annual IEEE/ACM International Symposium on Microarchitecture, New York, NY, USA, 2016. IEEE

    2016

  26. [34]

    Supervisor mode execution protection, 2011

    Stephen Fischer. Supervisor mode execution protection, 2011. URL https://www.ncsi.com/ nsatc11/presentations/wednesday/emerging_technologies/fischer.pdf

    2011

  27. [35]

    ab – apache http server benchmarking tool, 2025

    The Apache Software Foundation. ab – apache http server benchmarking tool, 2025. URL https://httpd.apache.org/docs/2.4/programs/ab.html

    2025

  28. [36]

    Randomizing the linux kernel heap freelists, Sep 2016

    Thomas Garnier. Randomizing the linux kernel heap freelists, Sep 2016. URL https://mxatone. medium.com/randomizing-the-linux-kernel-heap-freelists-b899bb99c767

    2016

  29. [37]

    Fine-grained control-flow in- tegrity for kernel software

    Xinyang Ge, Nirupama Talele, Mathias Payer, and Trent Jaeger. Fine-grained control-flow in- tegrity for kernel software. In 2016 IEEE European Symposium on Security and Privacy (Eu- roS&P), pages 179–194, New York, NY, USA, 2016. IEEE. doi: 10.1109/EuroSP.2016.24

    2016 doi

  30. [38]

    Fix rsb fill on context switch for serialize

    Thomas Gleixner. Fix rsb fill on context switch for serialize. https://lore.kernel.org/all/ 20220716230344.239749011@linutronix.de/, July 2022. Linux Kernel Mailing List

    2022

  31. [39]

    J. A. Goguen and J. Meseguer. Security policies and security models. In 1982 IEEE Symposium on Security and Privacy , New York, NY, USA, 1982. IEEE

    1982

  32. [40]

    Spec- ulative probing: Hacking blind in the spectre era

    Enes G¨ oktas, Kaveh Razavi, Georgios Portokalidis, Herbert Bos, and Cristiano Giuffrida. Spec- ulative probing: Hacking blind in the spectre era. In Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security , page 1871–1885, New York, NY, USA,

    2020

  33. [41]

    Prefetch side-channel attacks: Bypassing smap and kernel aslr

    Daniel Gruss, Cl´ ementine Maurice, Anders Fogh, Moritz Lipp, and Stefan Mangard. Prefetch side-channel attacks: Bypassing smap and kernel aslr. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security , page 368–379, New York, NY, USA,

    2016

  34. [42]

    Kaslr is dead: Long live kaslr

    Daniel Gruss, Moritz Lipp, Michael Schwarz, Richard Fellner, Cl´ ementine Maurice, and Stefan Mangard. Kaslr is dead: Long live kaslr. In Engineering Secure Software and Systems , pages 161–176, Berlin, Heidelberg, 2017. Springer International Publishing. ISBN 978-3-319-62105-0

    2017

  35. [43]

    Morales, Jan Reineke, and Andr´ es S´ anchez

    Marco Guarnieri, Boris K¨ opf, Jos´ e F. Morales, Jan Reineke, and Andr´ es S´ anchez. Spectector: Principled detection of speculative information flows. In 2020 IEEE Symposium on Security and Privacy (SP) , pages 1–19, New York, NY, USA, 2020. IEEE

    2020

  36. [44]

    Hardware-software contracts for secure speculation

    Marco Guarnieri, Boris K¨ opf, Jan Reineke, and Pepe Vila. Hardware-software contracts for secure speculation. In 2021 IEEE Symposium on Security and Privacy (SP) , pages 1868–1883, New York, NY, USA, 2021. IEEE

    2021

  37. [45]

    Practical timing side channel attacks against kernel space aslr

    Ralf Hund, Carsten Willems, and Thorsten Holz. Practical timing side channel attacks against kernel space aslr. In 2013 IEEE Symposium on Security and Privacy , pages 191–205, New York, NY, USA, 2013. IEEE

    2013

  38. [46]

    Mac os x has you covered, May 2011

    Apple Inc. Mac os x has you covered, May 2011. URL http://www.apple.com/macosx/ security/

    2011

  39. [47]

    ugrep, 2025

    Genivia Inc. ugrep, 2025. URL https://github.com/Genivia/ugrep-benchmarks

    2025

  40. [48]

    Intel Corporation, September 2023

    Intel ®64 and IA-32 Architectures Software Developer’s Manualx . Intel Corporation, September 2023

    2023

  41. [49]

    Page table isolation (pti), 2023

    The kernel development community. Page table isolation (pti), 2023. URLhttps://www.kernel. org/doc/html/next/x86/pti.html

    2023

  42. [50]

    Spectre attacks: Exploiting speculative execution

    Paul Kocher, Jann Horn, Anders Fogh, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Ham- burg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. Spectre attacks: Exploiting speculative execution. In 2019 IEEE Symposium on Security and Privacy (SP)...

    2019

  43. [51]

    Tagbleed: Breaking kaslr on the isolated kernel address space using tagged tlbs

    Jakob Koschel, Cristiano Giuffrida, Herbert Bos, and Kaveh Razavi. Tagbleed: Breaking kaslr on the isolated kernel address space using tagged tlbs. In 2020 IEEE European Symposium on Security and Privacy (EuroS&P) , pages 309–321, New York, NY, USA, 2020. IEEE

    2020

  44. [52]

    Un- contained: Uncovering container confusion in the linux kernel

    Jakob Koschel, Pietro Borrello, Daniele Cono D’Elia, Herbert Bos, and Cristiano Giuffrida. Un- contained: Uncovering container confusion in the linux kernel. In 32nd USENIX Security Sympo- sium (USENIX Security 23), pages 5055–5072, Anaheim, CA, August 2023. USENIX Association...

    2023

  45. [53]

    Lattner and V

    C. Lattner and V. Adve. Llvm: a compilation framework for lifelong program analysis & transfor- mation. In International Symposium on Code Generation and Optimization, 2004. CGO 2004. , pages 75–86, New York, NY, USA, 2004. IEEE

    2004

  46. [54]

    Com- prehensive and efficient protection of kernel control data

    Jinku Li, Zhi Wang, Tyler Bletsch, Deepa Srinivasan, Michael Grace, and Xuxian Jiang. Com- prehensive and efficient protection of kernel control data. IEEE Transactions on Information Forensics and Security, 6(4):1404–1417, 2011

    2011

  47. [55]

    Learn the architecture – providing protection for complex software, 2022

    Arm Limited. Learn the architecture – providing protection for complex software, 2022. URL https://developer.arm.com/documentation/102433/0100. 41

    2022

  48. [56]

    Meltdown: Reading kernel memory from user space

    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. Meltdown: Reading kernel memory from user space. In 27th USENIX Security Symposium (USENIX Security 18),...

    2018

  49. [57]

    Entrybleed: A universal kaslr bypass against kpti on linux

    William Liu, Joseph Ravichandran, and Mengjia Yan. Entrybleed: A universal kaslr bypass against kpti on linux. In Proceedings of the 12th International Workshop on Hardware and Architectural Support for Security and Privacy , HASP ’23, page 10–18, New York, NY, USA,

  50. [58]

    Towards unveiling exploitation potential with multiple error behaviors for kernel bugs

    Ziqin Liu, Zhenpeng Lin, Yueqi Chen, Yuhang Wu, Yalong Zou, Dongliang Mu, and Xinyu Xing. Towards unveiling exploitation potential with multiple error behaviors for kernel bugs. IEEE Transactions on Dependable and Secure Computing , 21(1):1–18, 2023

    2023

  51. [59]

    Kim, Parthasarathy Ranganathan, Daniel Stodolsky, and Mark Wachsler

    Andrea Lottarini, Alex Ramirez, Joel Coburn, Martha A. Kim, Parthasarathy Ranganathan, Daniel Stodolsky, and Mark Wachsler. vbench: Benchmarking video transcoding in the cloud. In Proceedings of the Twenty-Third International Conference on Architectural Support for Program- mi...

    2018

  52. [60]

    Mambretti, A

    A. Mambretti, A. Sandulescu, A. Sorniotti, W. Robertson, E. Kirda, and A. Kurmus. Bypassing memory safety mechanisms through speculative control flow hijacks. In 2021 IEEE European Symposium on Security and Privacy (EuroS&P) , pages 633–649, Los Alamitos, CA, USA, sep

    2021

  53. [61]

    Attacking the ios kernel: A look at ‘evasi0n’, March 2013

    Tarjei Mandt. Attacking the ios kernel: A look at ‘evasi0n’, March 2013. URL https://papers. put.as/papers/ios/2013/NISlecture201303.pdf

    2013

  54. [62]

    Address space layout randomization (aslr), July 2023

    Ed Maste. Address space layout randomization (aslr), July 2023. URL https://wiki.freebsd. org/AddressSpaceLayoutRandomization

    2023

  55. [63]

    Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson, Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena, and Deian Stefan

    Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson, Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena, and Deian Stefan. Mswasm: Soundly enforcing memory-safe execution of unsafe code. In Proceedings of the 50th ACM SI...

    2023

  56. [64]

    Drop the rop fine-grained control-flow integrity for the linux kernel, 2017

    Jo˜ ao Moreira, Sandro Rigo, Michalis Polychronakis, and Vasileios P Kemerlis. Drop the rop fine-grained control-flow integrity for the linux kernel, 2017

    2017

  57. [65]

    Martin, and Steve Zdancewic

    Santosh Nagarakatte, Jianzhou Zhao, Milo M.K. Martin, and Steve Zdancewic. Softbound: Highly compatible and complete spatial memory safety for c. SIGPLAN Not. , 44(6):245–258, 2009

    2009

  58. [66]

    Exorcising spectres with secure compilers

    Marco Patrignani and Marco Guarnieri. Exorcising spectres with secure compilers. In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, page 445–461, New York, NY, USA, 2021. ACM. ISBN 9781450384544

    2021

  59. [67]

    Kernel hardening, August 2022

    Android Open Source Project. Kernel hardening, August 2022. URL https://source.android. com/docs/core/architecture/kernel/hardening

    2022

  60. [68]

    X86speculativeexecutionsideeffectsuppression.cpp file reference, 2025

    The LL VM Project. X86speculativeexecutionsideeffectsuppression.cpp file reference, 2025. URL https://www.llvm.org/doxygen/X86SpeculativeExecutionSideEffectSuppression_8cpp. html. 42

    2025

  61. [69]

    Linux 6.1: Rust to hit mainline kernel, October 2022

    Liam Proven. Linux 6.1: Rust to hit mainline kernel, October 2022. URL https://www. theregister.com/2022/10/05/rust_kernel_pull_request_pulled/

    2022

  62. [70]

    Pacman: Attacking arm pointer authentication with speculative execution

    Joseph Ravichandran, Weon Taek Na, Jay Lang, and Mengjia Yan. Pacman: Attacking arm pointer authentication with speculative execution. InProceedings of the 49th Annual International Symposium on Computer Architecture, pages 685–698, New York, NY, USA, 2022. ACM

    2022

  63. [71]

    Toward linux kernel memory safety

    Elena Reshetova, Hans Liljestrand, Andrew Paverd, and N Asokan. Toward linux kernel memory safety. Software: Practice and Experience , 48(12):2237–2256, 2018

    2018

  64. [72]

    Linux kernel heap feng shui in 2022, May 2022

    Michael S and Vitaly Nikolenko. Linux kernel heap feng shui in 2022, May 2022. URL https: //duasynt.com/blog/linux-kernel-heap-feng-shui-2022

    2022

  65. [73]

    Threat overview for linux kernel, November 2022

    SecurityScorecard. Threat overview for linux kernel, November 2022. URL https://www. cvedetails.com/product/47/Linux-Linux-Kernel.html

    2022

  66. [74]

    On the effectiveness of address-space randomization

    Hovav Shacham, Matthew Page, Ben Pfaff, Eu-Jin Goh, Nagendra Modadugu, and Dan Boneh. On the effectiveness of address-space randomization. In Proceedings of the 11th ACM Conference on Computer and Communications Security , page 298–307, New York, NY, USA, 2004. ACM. ISBN 1581139616

    2004

  67. [75]

    Tanenbaum and Herbert Bos

    Andrew S. Tanenbaum and Herbert Bos. Modern Operating Systems. Prentice Hall Press, USA, 4th edition, 2014. ISBN 013359162X

    2014

  68. [76]

    Documentation for the pax project, 2003

    PaX Team. Documentation for the pax project, 2003. URL https://pax.grsecurity.net/ docs/

    2003

  69. [77]

    Inception: Exposing new attack surfaces with training in transient execution

    Dani¨ el Trujillo, Johannes Wikner, and Kaveh Razavi. Inception: Exposing new attack surfaces with training in transient execution. In 32nd USENIX Security Symposium (USENIX Security 23), pages 7303–7320, Anaheim, CA, August 2023. USENIX Association. ISBN 978-1-939133-37-

    2023

  70. [78]

    Retpoline: a software construct for preventing branch-target-injection, 2018

    Paul Turner. Retpoline: a software construct for preventing branch-target-injection, 2018. URL https://support.google.com/faqs/answer/7625886

    2018

  71. [79]

    Hypersafe: A lightweight approach to provide lifetime hypervisor control-flow integrity

    Zhi Wang and Xuxian Jiang. Hypersafe: A lightweight approach to provide lifetime hypervisor control-flow integrity. In 2010 IEEE Symposium on Security and Privacy , pages 380–395, New York, NY, USA, 2010. IEEE. doi: 10.1109/SP.2010.30

    2010 doi

  72. [80]

    Watson, Jonathan Woodruff, Peter G

    Robert N.M. Watson, Jonathan Woodruff, Peter G. Neumann, Simon W. Moore, Jonathan An- derson, David Chisnall, Nirav Dave, Brooks Davis, Khilan Gudka, Ben Laurie, Steven J. Murdoch, Robert Norton, Michael Roe, Stacey Son, and Munraj Vadera. Cheri: A hybrid capability-system arc...

    2015

  73. [81]

    Wenisch, and Baris Kasikci

    Ofir Weisse, Ian Neal, Kevin Loughlin, Thomas F. Wenisch, and Baris Kasikci. Nda: Preventing speculative execution attacks at their source. In Proceedings of the 52nd Annual IEEE/ACM International Symposium on Microarchitecture, page 572–586, New York, NY, USA, 2019. ACM. ISBN...

    2019

  74. [82]

    InSpectre gadget: Inspecting the residual attack surface of cross-privilege spectre v2

    Sander Wiebing, Alvise de Faveri Tron, Herbert Bos, and Cristiano Giuffrida. InSpectre gadget: Inspecting the residual attack surface of cross-privilege spectre v2. In 33rd USENIX Security Symposium (USENIX Security 24) , pages 577–594, Philadelphia, PA, August 2024. USENIX As...

    2024

  75. [83]

    URL https://www.usenix.org/conference/usenixsecurity23/presentation/trujillo

  76. [84]

    Phantom: Exploiting decoder-detectable mispredictions

    Johannes Wikner, Dani¨ el Trujillo, and Kaveh Razavi. Phantom: Exploiting decoder-detectable mispredictions. In Proceedings of the 56th Annual IEEE/ACM International Symposium on Mi- croarchitecture, MICRO ’23, page 49–61, New York, NY, USA, 2023. Association for Computing Mac...

    2023

  77. [85]

    Fletcher

    Jiyong Yu, Mengjia Yan, Artem Khyzha, Adam Morrison, Josep Torrellas, and Christopher W. Fletcher. Speculative taint tracking (stt): A comprehensive protection for speculatively accessed data. In Proceedings of the 52nd Annual IEEE/ACM International Symposium on Microarchi- te...

    2019

  78. [86]

    Ultimate slh: taking speculative load hardening to the next level

    Zhiyuan Zhang, Gilles Barthe, Chitchanok Chuengsatiansup, Peter Schwabe, and Yuval Yarom. Ultimate slh: taking speculative load hardening to the next level. In Proceedings of the 32nd USENIX Conference on Security Symposium , USA, 2023. USENIX Association. ISBN 978-1- 939133-3...

    2023

  79. [89]

    RETBLEED: Arbitrary speculative code execution with return instructions

    Johannes Wikner and Kaveh Razavi. RETBLEED: Arbitrary speculative code execution with return instructions. In 31st USENIX Security Symposium (USENIX Security 22) , pages 3825– 3842, Boston, MA, August 2022. USENIX Association. ISBN 978-1-939133-31-1

    2022

  80. [93]

    ∧ u(F1) ⇒ w ⊢σ2 ϕ2 →∗ (F, w⋄ τ′

  81. [94]

    We prove this by induction on n: - Case 0

    ∧ τ′ 1 =Idu∪ArrIdk τ′ 2. We prove this by induction on n: - Case 0. This case is trivial. - Case n + 1. In this case, we assume: w ⊢σ1 ϕ1 →n (F, w⋄ τ′

  82. [95]

    We apply the IH to the n-step transition, obtaining: w ⊢σ2 ϕ2 →∗ (F, w⋄ τ′

    → (F ′, w⋄ τ′′ 1 ) ∧ u(F ′). We apply the IH to the n-step transition, obtaining: w ⊢σ2 ϕ2 →∗ (F, w⋄ τ′

  83. [96]

    Our goal is to establish: w ⊢σ2 (F, w⋄ τ′

    ∧ τ′ 1 =Idu∪ArrIdk τ′ 2. Our goal is to establish: w ⊢σ2 (F, w⋄ τ′

  84. [97]

    The proof proceeds by case analysis on the rule used in: w ⊢σ1 (F, w⋄ τ′

    →∗ (F ′, w⋄ τ′′ 2 ) ∧ τ′′ 1 =Idu∪ArrIdk τ′′ 2 . The proof proceeds by case analysis on the rule used in: w ⊢σ1 (F, w⋄ τ′

  85. [98]

    (†) In most cases, the identity of the frame stack and the equivalence τ′ 1 =Idu∪ArrIdk τ′ 2 suffice to show that the same rule applies to the corresponding transition in σ2

    → (F ′, w⋄ τ′′ 1 ). (†) In most cases, the identity of the frame stack and the equivalence τ′ 1 =Idu∪ArrIdk τ′ 2 suffice to show that the same rule applies to the corresponding transition in σ2. To illustrate this, we consider [Load] as an example. Another notable case is [ Po...

  86. [99]

    - Case [Pop]

    → (F ′, w⋄ τ′ 2) In particular, the stack frame is F ′ because τ′ 1(a, i) = τ′ 2(a, i). - Case [Pop]. We can refine the assumption ( †) as follows: w ⊢σ1 (⟨ε, ρ′, b⟩ : F , w⋄ τ′

  87. [100]

    Additionally, we have u(F ′ ) which also implies u(F )

    → (F ′ , w⋄ τ′ 1) where, in particular, F ′ is obtained by updating the register map of F according to the rule. Additionally, we have u(F ′ ) which also implies u(F ). We proceed by cases on b. - Case b = u. In this case, we can apply the IH, and the remaining part of the pro...

  88. [101]

    In ( ∗), we tacitly unrolled the first reduction step of the system call invocation

    ( ∗) and w ⊢σ1 (⟨γ1(s), ρ′ 0, ks⟩, w⋄ τ′′ 1 ) →n−n′−1 (⟨ε, ρ′, ks⟩ : F ′′ , w⋄ τ′ 1), (‡) with F ′′ : ⟨D, ρ,u⟩ : F ′′ = F and k(F ′′ ). In ( ∗), we tacitly unrolled the first reduction step of the system call invocation. From k(F ′′ ) and u(F ), we deduce that F ′′ must be emp...

  89. [102]

    → (⟨γ1(s), ρ′ 0, ks⟩ : ⟨D, ρ′, u⟩ : F, w⋄ τ′

  90. [103]

    →∗ (F ′ : ⟨D, ρ′, u⟩ : F, w⋄ τ′′ 1 ) → err, and that: w ⊢σ1 (⟨γ1(s), ρ′ 0, ks⟩, w⋄ τ′

  91. [104]

    By case analysis on the rules that has been used to prove w ⊢σ1 ϕ′ 1 → err, we observe that the same rule can also be used to prove w ⊢σ1 (F ′, w⋄ τ′′ 1 ) → err

    →∗ (F ′, w⋄ τ′′ 1 ) In the first conclusion, we tacitly replaced ϕ′ 1 with ( F ′ : ⟨D, ρ′, u⟩ : F, w⋄ τ′′ 1 ) and we made the first reduction step after the system call invocation explicit. By case analysis on the rules that has been used to prove w ⊢σ1 ϕ′ 1 → err, we observe ...

  92. [105]

    →∗ err, and by applying the assumption on the preservation of system call semantics, we deduce: w ⊢σ2 (⟨γ2(s), ρ′ 0, ks⟩, w⋄ τ′

  93. [106]

    By applying the auxiliary claim, we prove: w ⊢σ2 ϕ2 →∗ (⟨syscall s(E1,

    →∗ err. By applying the auxiliary claim, we prove: w ⊢σ2 ϕ2 →∗ (⟨syscall s(E1, . . . ,Ek); D, ρ′, u⟩ : F, w⋄ τ′

  94. [107]

    We conclude with an application of Lemma 9, which proves w ⊢σ2 ϕ2 →∗ err

    → (⟨γ2(s), ρ′ 0, ks⟩ : ⟨D, ρ′, u⟩ : F, w⋄ τ′ 2), Here, we unrolled the first step of the execution of the system call using the rule [ SC]. We conclude with an application of Lemma 9, which proves w ⊢σ2 ϕ2 →∗ err. - Case unsafe. This case is analogous to the previous one. - Ca...

  95. [109]

    : ⟨Ck, ρk, bk⟩ for C0,

    F = ⟨C0, ρ0, b0⟩ : . . .: ⟨Ck, ρk, bk⟩ for C0, . . . ,Ck such that Σ(C0, ⊤, ⊥), . . . ,Σ(Ck, ⊤, ⊥)

  96. [110]

    C = ψm e (C′) ∧ bms ⇒ m ∧ e ⇒ µ = ϵ

  97. [111]

    Consequently, we can apply Remark 8 to establish that τ ′ =ProcId τ =ProcId τ ′′

    dom([JEKAddr ρ,w 7→ JFKρ,w]) ⊆ w(ArrId) From (H2), we conclude that the domain of µ is a subset of ArrId. Consequently, we can apply Remark 8 to establish that τ ′ =ProcId τ =ProcId τ ′′. This follows directly from (H2), and hence ψ, σ⊢ twfw(τ ′), given that σ ∈ im(ψ). Point (...

  98. [112]

    (µ, w⋄ τ) = w ⋄ τ ′ for some τ ′ such that ψ, σ⊢ twfw(τ ′)

  99. [113]

    ,Ck such that Σ(C0, ⊤, ⊥),

    All frames in the stack of the final configuration carry commands C0, . . . ,Ck such that Σ(C0, ⊤, ⊥), . . . ,Σ(Ck, ⊤, ⊥)

  100. [114]

    Point (2) is a consequence of (H2), and follows by introspection of the target configuration

    dom(ϵ) ⊆ w(ArrId) The proof of point (1) is analogous to the one given for stores. Point (2) is a consequence of (H2), and follows by introspection of the target configuration. Points (3) and (4) (where we already replaced m, e, bms and µ with their actual value for this sub-d...

  101. [115]

    w ⋄ τ =ProcId w ⋄ τ ′′, which directly follows from (H2)

  102. [116]

    : ⟨Ck, ρk, bk⟩, where C0,

    The stack F is of the form⟨C0, ρ0, b0⟩ : . . .: ⟨Ck, ρk, bk⟩, where C0, . . . ,Ck satisfies Σ(C0, ⊤, ⊥), . . . ,Σ(Ck, ⊤, ⊥). This follows trivially from (H2), as the frame stack remains unchanged

  103. [117]

    Σ( ψ⊤ ⊥(Ci); ψ⊤ ⊥(D)), that is trivial

  104. [118]

    - Case ⃗Q ̸= ε

    dom(µ) ⊆ w(ArrId), which is a consequence of (H2). - Case ⃗Q ̸= ε. This remaining case is analogous to the case where ⃗Q = ε and C ̸= ε, as the premises (H1), (H2), (H3) also hold for the first element of ⃗Q. Lemma 25. Let σ = (τ, γ, ξ) be a system. For every configuration sta...

  105. [2016]

    ISBN 9781450341394

    ACM. ISBN 9781450341394

  106. [2021]

    IEEE Computer Society

  107. [2022]

    URL https://www.intel.com/content/www/us/en/developer/articles/technical/ software-security-guidance/technical-documentation/branch-history-injection. html. Technical Documentation. 39

  108. [2023]

    ISBN 9798400716232

    ACM. ISBN 9798400716232

  109. [2025]

    URL https://www.intel.com/content/www/us/en/developer/topic-technology/ software-security-guidance/processors-affected-consolidated-product-cpu-model. html

Pith tools

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