Pith. sign in

REVIEW 3 major objections 6 minor 44 references

Global Microprocessor Correctness in the Presence of Transient Execution

T0 review · 3 major / 6 minor · reviewed 2026-08-15 · deepseek-v4-flash

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

Pith's one-line read The paper proposes global refinement-based correctness notions that make ISA conformance, functional correctness, and freedom from cache-based Meltdown and Spectre attacks a single proof obligation.

desk verdict Solid, novel refinement framework for TEA, but the Spectre guarantee is only as strong as the externally chosen auth-actions, and the decomposition is backed by testing rather than proof. read the letter →

arxiv 2506.17154 v1 pith:YKFBAKSB submitted 2025-06-20 cs.CR

Andrew T. Walter , Konstantinos Athanasiou , Panagiotis Manolios This is my paper · ORCID
classification cs.CR
keywords TransientexecutionattacksMeltdownSpectreMicroprocessorcorrectnessSkippingrefinementCachesidechannelsFormalverificationISAconformance
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

Modern processors are judged correct when they conform to their instruction set architecture, but that conformance is usually informal and, after Meltdown and Spectre, clearly insufficient: a processor can be functionally correct and still leak secrets through cache effects of transient instructions. This paper argues that the cure is a single global correctness specification, formalized as refinement between a microprocessor model and an ISA model, that bundles ISA conformance, functional correctness, and security against cache-based transient execution attacks. The specification is designed so that a microarchitecture vulnerable to Meltdown fails one refinement notion, a microarchitecture vulnerable to Spectre fails an extended action-labeled refinement notion, and a machine passing either proof is guaranteed conforming for every program. The paper demonstrates both notions on executable, bit- and cycle-accurate models of an ISA and an out-of-order, speculative microprocessor, using property-based testing to expose bugs in vulnerable variations and none in a safe one.

What carries the argument

The load-bearing machinery is a hierarchy of refinement notions. Skipping refinement lets a concrete system stutter or commit several instructions while still matching an abstract ISA trace; witness skipping refinement adds explicit stutter-wit, skip-wit, and run functions that bound how many steps are needed, turning infinite-trace matching into finite, checkable obligations. The in-cache abstraction adds a nondeterministic ISA instruction that returns whether an address is cached, so the ISA admits every reasonable cache implementation while still letting a cache side channel be observed. For Spectre, action skipping refinement compares paths whose transitions carry action labels, and intent models let the MA emit 'intent virtual instructions' that declare the addresses it prefetches or caches; the ISA-side only admits actions the designer's auth-actions function authorizes. Finally, entangled states and the shared-resource commitment refinement map isolate the reachable behavior of the MA by generating a superset of reachable states from history plus invalidation, eliminating unreachable counterexamples without design-specific inductive invariants.

What would settle it

Run the Spectre correctness obligations on a processor that executes a Spectre gadget and define auth-actions for the gadget's transient load to include the out-of-bounds cache fill; if the action skipping refinement and the cache-effect equation still hold, the guarantee is determined by the authorization choice rather than by the microarchitecture, contradicting the paper's framing. Conversely, showing that every auth-actions consistent with ISA memory-access permissions fails on that processor would confirm the claim.

Watch

Extended reading notes

Core claim

The paper's central claim is that conformance with an ISA can be expressed as a refinement relation that already contains the security property, so security does not have to be bolted on as a separate non-interference condition. For Meltdown, it says a microarchitecture is a correct implementation of the ISA exactly when it is a skipping refinement of the ISA with respect to a refinement map, where the ISA is extended by a nondeterministic 'in-cache' abstract instruction that reports whether an address is cached. For Spectre, correctness is an action skipping refinement between the same machines when the MA labels each transition with intent virtual instructions declaring which cache changes it makes, and the ISA is allowed to make exactly those authorized cache changes. The authors report these are the first global correctness notions that address transient execution attacks, and they show how to decompose the proofs using entangled states and shared-resource commitment refinement maps so the verification obligations become finite and machine-checkable.

Load-bearing premise

The load-bearing premise is that the designer-supplied function auth-actions correctly declares which cache modifications are authorized: if it is permissive or mistaken, the Spectre correctness proof can succeed for a processor that leaks through speculative cache fills.

Editorial extensions

If this is right

  • A machine that passes Meltdown correctness is simultaneously ISA-conforming and free of cache-based Meltdown leakage for every program, terminating or not.
  • Spectre correctness decomposes into Meltdown-style conformance plus the requirement that the cache after an MA transition equals the cache produced by applying its emitted actions, isolating the new security obligation from the rest of the refinement proof.
  • The decomposition theorem composes bisimulation, simulation, and skipping refinements, so a large conformance proof can be split into independent, finite-step verification tasks.
  • Property-based testing over entangled states found functional bugs and transient-execution bugs in the buggy models and no transient-execution bugs in the safe model, indicating that the notions separate vulnerable from safe designs.

Reading between the lines

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

  • Beyond the paper: the Spectre guarantee inherits its strength from auth-actions; if that designer-supplied function treats the address fetched by a Spectre gadget as an authorized cache fill, the refinement and cache-effect equation can hold for a vulnerable machine. A principled rule for deriving auth-actions from ISA-level memory permissions would remove this dependence.
  • Beyond the paper: the in-cache abstraction observes only cache membership, so the same global refinement strategy would need new observer abstractions to cover other microarchitectural channels such as execution timing or port contention.
  • Beyond the paper: a testable extension would run the two refinement notions on an existing open-source out-of-order core and check whether permissive auth-actions can certify a known-vulnerable configuration; that experiment would measure how much of the security conclusion lives in the refinement rather than in the authorization choices.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 6 minor

Summary. The paper proposes global correctness notions for microprocessors in the presence of transient execution attacks. It models an ISA and a microarchitecture as transition systems, introduces witness skipping refinement and an in-cache abstract instruction, and defines Meltdown correctness as skipping refinement between the MA and ISA. For Spectre, it introduces action-labeled transition systems and action skipping refinement, where the MA emits authorized cache actions and correctness is an action skipping refinement with respect to a designer-supplied auth-actions function. The paper also presents a decomposition methodology based on entangled states and shared-resource commitment refinement maps, fully executable formal models in ACL2s, and property-based testing experiments that find functional and TEA bugs in the models. The headline claim is that these are the first global notions of correctness that formalize ISA conformance, include functional correctness, and are violated by microarchitectures allowing cache-based transient execution attacks.

Significance. If the framework were fully established, it would be a valuable complement to non-interference-based approaches: a single conformance specification covering functional correctness and important classes of transient execution attacks, with decomposition obligations amenable to automated reasoning. The paper ships fully executable bit- and cycle-accurate models and ACL2s artifacts, gives explicit definitions of witness skipping, entangled states, and the related decomposition, and demonstrates that counterexample search can identify TEA bugs. The Meltdown notion is plausible and well motivated, and the distinction between illegal-unprivileged accesses and legal-but-ISA-unobservable accesses is a genuine conceptual contribution. However, the Spectre guarantee is conditional on an externally chosen auth-actions function, and no adequacy condition is established that prevents the notion from being vacuous. The value of the artifact and the decomposition ideas is real, but the load-bearing Spectre security claim needs substantial reworking.

major comments (3)
  1. [§5.4 and §6, Eq. (17)] The Spectre correctness notion is parameterized by auth-actions, described in §5.4 as "a notion decided by the designer," and the only cache-related proof obligation is Eq. (17), which requires cache_u = apply-action(s, a) for each transition s -a-> u. Nothing constrains auth-actions to exclude the address array2[array1[x']] brought into the cache by a Spectre gadget. If the designer defines auth-actions(s, u) so that it emits exactly the cache difference between u and s, encoded as prefetch/cache actions, Eq. (17) holds by construction; since the MISA-IC-A rule in Appendix B.2 lets the ISA apply any action sequence through apply-prefetches, action skipping refinement can then hold for the buggy, Spectre-vulnerable MMA-IC. The claimed implication "conformance implies absence of Spectre" is therefore not established; the separation between legitimate prefetching and Spectre leakage is entirely delegated to an external, unverified function. The paper needs an adequacy condition for auth-actions, or a reformulation in which the security conclusion is explicitly relative to a fixed, machine-independent authorization policy, together with a proof that a conforming MA is Spectre-secure under that condition.
  2. [§6, Eqs. (13)–(16)] The central decomposition argument that proofs of Eqs. (13) and (14) imply Eq. (12) is informal and contains unproven uniqueness and equivalence assumptions. The text asserts that any MMA-IC-A state has a unique related MISA-IC-A state and that two action sequences starting from the same cache and producing the same cache must be equivalent up to "noop" actions; neither is justified. In particular, the relation B used in the unlabeled skipping refinement, as defined near Appendix C, relates an ISA state to every MA state whose r-ic image has the same label, so uniqueness is not immediate. Also, two different action sequences can have the same net cache effect without being interchangeable, e.g., a prefetch of an already-resident line versus a cache action. Since this decomposition is the main pathway to automated verification of the Spectre notion, the argument needs to be replaced by a formal proof, or at least a machine-checked statement in ACL2.
  3. [§4.4, §6.1, Appendix C, Eqs. (5)–(8), (18)–(20), (24)–(27)] The proof obligations for both the Meltdown and Spectre decompositions are listed but not discharged for the models described in Section 3 and Appendix B. The paper does not provide proofs or machine-checked ACL2 proofs that the entangled-state obligations, the witness-skipping obligations, or Eq. (17) hold for MMA-IC and MISA-IC. The evaluation in Section 7 is counterexample search by property-based testing, which is useful for finding bugs but does not establish the positive claim that a conforming MA is free of the relevant attacks. The wording in Section 1 that a TEA-vulnerable microprocessor "will not satisfy our notion of correctness" should therefore be made conditional on the proof obligations actually being discharged, and the paper should clarify that the contribution is a proof framework with identified obligations rather than a verified guarantee.
minor comments (6)
  1. [Abstract] There are two small typos: "an microarchitecture" should be "a microarchitecture," and "using the the concept" should be "using the concept."
  2. [§1] "in constrast" should be "in contrast" in the discussion of non-interference-based approaches.
  3. [§2.2 and Appendix B.1] The notation "in-cache(a, s)" is used both as an instruction mnemonic and as a predicate over addresses and states in Eq. (1); this overloading should be clarified, for example by naming the predicate in-cache-mem or in-cache?.
  4. [§6 and Appendix B.2] Equation (13) writes "MMA-IC ≲_r-a MISA-IC," but r-a is introduced as a map between MA-IC-A and ISA-IC-A states; since the underlying state sets are the same, this is understandable, but the differing label functions of the two systems should be stated explicitly to avoid confusion.
  5. [Appendix C] Obligations (24)–(27) duplicate (5)–(8) with different numbering; the paper should either cross-reference the earlier equations or omit the duplicate statements, as the repetition makes it harder to track which obligations are actually proven.
  6. [§7, Table 1] The evaluation reports counts of bugs found in three configurations but does not describe the number of test cases, randomness, or coverage; a sentence on the testing budget and on whether the same bugs were found across repeated runs would improve reproducibility.

Circularity Check

2 steps flagged · score 6.0 of 10

Spectre correctness is defined relative to designer-supplied auth-actions; a permissive choice makes Equation 17 and action skipping refinement hold by construction, so the Spectre security guarantee is not self-contained.

  1. self definitional [Section 5.4 (Statement of Correctness) and Section 6 (Equations 12-17)]
    "The actions A_ISA = A_MA used by these systems are used to indicate what changes to the cache are authorized, a notion decided by the designer of the system. ... s --a-->_MA-IC-A u iff s -->_MA-IC u and a = auth-actions(s,u)."

    Spectre correctness is action skipping refinement of MISA-IC-A, and the MA transition labels are exactly auth-actions(s,u), the same designer-supplied function that fixes the ISA's authorized cache updates. If the designer sets auth-actions(s,u) to the actual cache modification of each MA transition (for example, emitting a prefetch/cache action for the transient fill of array2[array1[x']]), then the MA emits exactly the actions matching its cache behavior, MISA-IC-A replays those actions via apply-prefetches, and action skipping refinement holds. The definition therefore cannot distinguish legitimate prefetching from a Spectre leak: the security property is asserted by the choice of auth-actions rather than derived from an independent criterion.

  2. self definitional [Section 6, Equation 17]
    "We would like to check that MMA-IC-A is not modifying the cache through some unauthorized actions that it is not emitting. This gives Equation 17, where apply-action is a function that takes in a MMA-IC-A state s, a cache c and an action a, and produces c after applying a to it."

    Equation 17 is the only cache-specific proof obligation for Spectre. Since the transition label a is defined to be auth-actions(s,u), the equation reduces to cache_u = apply-action(s, auth-actions(s,u)). If auth-actions returns the actual cache differences of the transition, the obligation is true by construction for a Spectre-vulnerable MA. It checks only that the emitted action describes the cache change, not that the cache change was authorized in any security-relevant sense. Thus the formal 'guarantee' is equivalent to the designer's choice of auth-actions, and the security-relevant question of whether the transient fill was permitted is never independently posed.

full rationale

The Meltdown portion of the paper is largely self-contained: the in-cache abstraction restricts the ISA to return false for inaccessible addresses, the witness skipping refinement obligations in Section 4 are stated as independent proof obligations, and the Section 7 property-based testing found functional bugs, so that derivation chain is not circular. The skipping refinement and commitment-map machinery are imported from prior refinement literature in the normal way and are not load-bearing self-citations here. The Spectre portion, however, is partially circular in the sense of the rubric: the central security distinction is delegated to auth-actions, which the paper explicitly labels as 'a notion decided by the designer of the system' and for which no adequacy condition or derivation procedure is given. Equation 17 then holds by construction under a permissive choice of auth-actions, making action skipping refinement and the resulting Spectre correctness vacuous for a vulnerable MA. This is not merely a missing proof; it is definitional, because the correctness predicate itself is parameterized by the function that decides which cache fills are authorized. The Section 7 Spectre counterexample is still meaningful for the particular models and actions used, but it does not rescue the general claim that a conforming MA is Spectre-secure. Score 6 reflects one central partial circularity; the rest of the derivation chain is independent.

Assumptions & free parameters 1 free parameters · 4 assumptions · 2 invented entities

The framework introduces no fitted numeric constants, but it does depend on several externally supplied formal objects: the in-cache instruction, the auth-actions contract, and the entangled-state machinery. The Meltdown guarantee rests on the domain assumption that inaccessible addresses are never cached in abstract ISA semantics. The Spectre guarantee rests on the adequacy of the designer-supplied authorization function. These are load-bearing and should be made explicit in any acceptance decision.

free parameters (1)
  • auth-actions (authorized cache action generator) = designer-supplied function per microarchitecture
    The Spectre correctness statement and Equation 17 are parameterized by this function. The TEA guarantee is conditional on its adequacy, so it is a hand-chosen component of the framework rather than a number fitted to data.
assumptions (4)
  • standard math Background results on skipping refinement and simulation compositionality are assumed from Jain and Manolios and Manolios.
    Definitions 2.2 through 2.4 rely on skipping refinement, and Theorem 4.1 relies on compositionality of bisimulation, simulation, and skipping refinement from the cited prior work.
  • domain assumption The in-cache abstraction assumes an architecturally visible in-cache instruction exists and that inaccessible addresses are never cached in the abstract ISA, as stated in Equation 1.
    This is the security-relevant boundary for Meltdown. If a conforming ISA were allowed to observe kernel addresses in cache, the refinement would not detect the attack.
  • ad hoc to paper Spectre correctness assumes the designer-supplied auth-actions function exactly characterizes all and only legitimate cache modifications.
    Section 5.4 and Equation 17 define correctness relative to this external contract. A permissive or incorrect auth-actions can make a vulnerable MA satisfy the notion.
  • domain assumption The deterministic MA behavior is a subset of the nondeterministic MA-N, and the entangled-state inclusion and closure obligations (Equations 5-8 and 24-27) hold.
    The decomposition to MMA-G-IC rests on these obligations, which are listed but not machine-checked in the paper.
invented entities (2)
  • in-cache abstract instruction
    purpose: Adds architecturally visible cache membership queries to both ISA and MA so cache side channels can be expressed in refinement.
    A formal abstraction not present in real ISAs. Its semantics for inaccessible addresses, Equation 1, is what makes Meltdown detectable.
  • intent virtual instructions and authorized cache actions (prefetch_a, cache_a)
    purpose: Let the MA emit the cache changes it intends, and let the ISA apply those actions so Spectre-relevant unauthorized cache updates can be checked.
    The authorization notion is supplied by the designer, not independently justified. If mis-specified, the correctness notion can be vacuous.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Global Microprocessor Correctness in the Presence of Transient Execution." pith.science (2026). https://pith.science/paper/YKFBAKSB

@misc{pith2026250617154,
  author       = {Pith},
  title        = {Pith review of: Global Microprocessor Correctness in the Presence of Transient Execution},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YKFBAKSB}},
  note         = {Machine review of arXiv:2506.17154}
}
read the original abstract

Correctness for microprocessors is generally understood to be conformance with the associated instruction set architecture (ISA). This is the basis for one of the most important abstractions in computer science, allowing hardware designers to develop highly-optimized processors that are functionally "equivalent" to an ideal processor that executes instructions atomically. This specification is almost always informal, e.g., commercial microprocessors generally do not come with conformance specifications. In this paper, we advocate for the use of formal specifications, using the theory of refinement. We introduce notions of correctness that can be used to deal with transient execution attacks, including Meltdown and Spectre. Such attacks have shown that ubiquitous microprocessor optimizations, appearing in numerous processors for decades, are inherently buggy. Unlike alternative approaches that use non-interference properties, our notion of correctness is global, meaning it is single specification that: formalizes conformance, includes functional correctness and is parameterized by an microarchitecture. We introduce action skipping refinement, a new type of refinement and we describe how our notions of refinement can be decomposed into properties that are more amenable to automated verification using the the concept of shared-resource commitment refinement maps. We do this in the context of formal, fully executable bit- and cycle-accurate models of an ISA and a microprocessor. Finally, we show how light-weight formal methods based on property-based testing can be used to identify transient execution bugs.

Figures

Figures reproduced from arXiv: 2506.17154 by the authors.

Figure 1
Figure 1. The model variants that we use to decompose the [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

44 extracted references · 28 canonical work pages

  1. [1]

    Hardware Prefetcher on Intel Processors

    2014. Hardware Prefetcher on Intel Processors. https://software.intel.com/ content/www/us/en/develop/articles/disclosure-of-hw-prefetcher-control-on- some-intel-processors.html

    work page 2014

  2. [2]

    CVE-2018-3639: Speculative Store Bypass

    2018. CVE-2018-3639: Speculative Store Bypass. Available from MITRE. https: //cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2018-3639

    work page 2018

  3. [3]

    Martín Abadi and Leslie Lamport. 1991. The Existence of Refinement Mappings. Theor. Comput. Sci.82, 2 (1991), 253–284. doi:10.1016/0304-3975(91)90224-P

    doi:10.1016/0304-3975(91)90224-p 1991

  4. [4]

    Wenisch, Yuval Yarom, and Raoul Strackx

    Jo Van Bulck, Marina Minkin, Ofir Weisse, Daniel Genkin, Baris Kasikci, Frank Piessens, Mark Silberstein, Thomas F. Wenisch, Yuval Yarom, and Raoul Strackx

    work page

  5. [5]

    Finocchiaro, and Danilo Ven- draminetto

    Gianpiero Cabodi, Paolo Camurati, Fabrizio F. Finocchiaro, and Danilo Ven- draminetto. 2019. Model Checking Speculation-Dependent Security Properties: Abstracting and Reducing Processor Models for Sound and Complete Verification. InCodes, Cryptology and Information Security - Third International Conference, C2SI 2019, Proceedings - In Honor of Said El Haj...

    work page 2019

  6. [6]

    Claudio Canella, Daniel Genkin, Lukas Giner, Daniel Gruss, Moritz Lipp, Marina Minkin, Daniel Moghimi, Frank Piessens, Michael Schwarz, Berk Sunar, et al

    work page

  7. [7]

    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. In28th {USENIX}Security Symposium ({USENIX}Security 19). 249–266

    work page 2019

  8. [8]

    Dillinger, Panagiotis Manolios, and Daron Vroon

    Harsh Chamarthi, Peter C. Dillinger, Panagiotis Manolios, and Daron Vroon

    work page

Show all 44 references
  1. [9]

    2016.Interactive Non-theorem Disproving

    Harsh Raju Chamarthi. 2016.Interactive Non-theorem Disproving. Ph. D. Disser- tation. Northeastern University. doi:10.17760/D20467205

    2016 doi

  2. [10]

    Dillinger, Matt Kaufmann, and Panagiotis Manolios

    Harsh Raju Chamarthi, Peter C. Dillinger, Matt Kaufmann, and Panagiotis Manolios. 2011. Integrating Testing and Interactive Theorem Proving. InIn- ternational Workshop on the ACL2 Theorem Prover and its Applications (EPTCS). doi:10.4204/EPTCS.70.1

    2011 doi

  3. [11]

    Dillinger, and Panagiotis Manolios

    Harsh Raju Chamarthi, Peter C. Dillinger, and Panagiotis Manolios. 2014. Data Definitions in the ACL2 Sedan. InProceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications (EPTCS). doi:10.4204/EPTCS.152.3

    2014 doi

  4. [12]

    Harsh Raju Chamarthi and Panagiotis Manolios. 2011. Automated specification analysis using an interactive theorem prover. InInternational Conference on Formal Methods in Computer-Aided Design, FMCAD ’11, Per Bjesse and Anna Slobodová (Eds.). FMCAD Inc., 46–53. https://dl.acm.o...

    2011 doi

  5. [13]

    The ACL2 Sedan

    Peter C. Dillinger, Panagiotis Manolios, Daron Vroon, and J. Strother Moore. 2007. ACL2s: “The ACL2 Sedan”. InProceedings of the 7th Workshop on User Interfaces for Theorem Provers (UITP 2006) (Electronic Notes in Theoretical Computer Science). doi:10.1016/j.entcs.2006.09.018

    2007 doi

  6. [14]

    2022.Unique Program Execution Checking: A Novel Approach for Formal Security Analysis of Hardware

    Mohammad Rahmani Fadiheh. 2022.Unique Program Execution Checking: A Novel Approach for Formal Security Analysis of Hardware. Ph. D. Dissertation. Technische Universität Kaiserslautern. doi:10.26204/KLUEDO/6930

    2022 doi

  7. [15]

    Barrett, Subhasish Mitra, and Wolfgang Kunz

    Mohammad Rahmani Fadiheh, Dominik Stoffel, Clark W. Barrett, Subhasish Mitra, and Wolfgang Kunz. 2019. Processor Hardware Security Vulnerabili- ties and their Detection by Unique Program Execution Checking. InDesign, Automation & Test in Europe Conference & Exhibition, DATE 20...

    2019

  8. [16]

    Luís Fiolhais and Leonel Sousa. 2024. Transient-Execution Attacks: A Computer Architect Perspective.ACM Comput. Surv.56, 3 (2024), 74:1–74:38. doi:10.1145/ 3603619

    2024

  9. [17]

    Marco Guarnieri, Boris Köpf, Jan Reineke, and Pepe Vila. 2021. Hardware- Software Contracts for Secure Speculation. In42nd IEEE Symposium on Security and Privacy, SP 2021. IEEE, 1868–1883. doi:10.1109/SP40001.2021.00036

    2021

  10. [18]

    2011.Computer architecture: a quanti- tative approach

    John L Hennessy and David A Patterson. 2011.Computer architecture: a quanti- tative approach. Elsevier

    2011

  11. [19]

    2016.Intel ® 64 and IA-32 Architectures Optimization Reference Manual

    Intel Corporation. 2016.Intel ® 64 and IA-32 Architectures Optimization Reference Manual. Intel Corporation

    2016

  12. [20]

    Mitesh Jain and Panagiotis Manolios. 2015. Skipping refinement. InInternational Conference on Computer Aided Verification. Springer, 103–119

    2015

  13. [21]

    Mitesh Jain and Panagiotis Manolios. 2019. Local and Compositional Reasoning for Optimized Reactive Systems. InCA V

    2019

  14. [23]

    2000.Computer- Aided Reasoning: Case Studies

    Matt Kaufmann, Panagiotis Manolios, and J Strother Moore. 2000.Computer- Aided Reasoning: Case Studies. Kluwer Academic Publishers. doi:10.1007/978-1- 4757-3188-0

    2000 doi

  15. [24]

    Matt Kaufmann and J Strother Moore. 2025. ACL2 homepage. (2025). https: //www.cs.utexas.edu/users/moore/acl2/

    2025

  16. [25]

    Paul Kocher, Jann Horn, Anders Fogh, , Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. 2019. Spectre Attacks: Exploiting Speculative Execu- tion. In40th IEEE Symposium on Security and Priva...

    2019

  17. [26]

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

    2018

  18. [27]

    Andrea Mambretti, Alexandra Sandulescu, Alessandro Sorniotti, Wil Robertson, Engin Kirda, and Anil Kurmus. 2020. Bypassing memory safety mechanisms through speculative control flow hijacks.arXiv preprint arXiv:2003.05503(2020)

    2020 arXiv

  19. [28]

    Panagiotis Manolios. 2000. Correctness of Pipelined Machines. InFormal Methods in Computer-Aided Design, Third International Conference, FMCAD 2000, Proceed- ings. 161–178. doi:10.1007/3-540-40922-X_11

    2000 doi

  20. [29]

    Srinivasan, and Kushal K

    Nimish Mathure, Sudarshan K. Srinivasan, and Kushal K. Ponugoti. 2022. A Refinement-Based Approach to Spectre Invulnerability Verification.IEEE Access 10 (2022), 80949–80957. doi:10.1109/ACCESS.2022.3195508

    2022

  21. [30]

    Sparsh Mittal. 2016. A survey of recent prefetching techniques for processor caches.ACM Computing Surveys (CSUR)49, 2 (2016), 1–35

    2016

  22. [31]

    Patterson and John L

    David A. Patterson and John L. Hennessy. 2013.Computer Organization and De- sign, Fifth Edition: The Hardware/Software Interface(5th ed.). Morgan Kaufmann Andrew T. Walter, Konstantinos Athanasiou, and Panagiotis Manolios Publishers Inc., San Francisco, CA, USA

    2013

  23. [32]

    Allison Randal. 2023. This is How You Lose the Transient Execution War.CoRR abs/2309.03376 (2023). doi:10.48550/ARXIV.2309.03376 arXiv:2309.03376

    2023 doi arXiv

  24. [33]

    Michael Schwarz, Moritz Lipp, Daniel Moghimi, Jo Van Bulck, Julian Steck- lina, Thomas Prescher, and Daniel Gruss. 2019. ZombieLoad: Cross-privilege- boundary data sampling. InProceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. 753–768

    2019

  25. [34]

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

  26. [35]

    Robert M Tomasulo. 1967. An efficient algorithm for exploiting multiple arith- metic units.IBM Journal of research and Development11, 1 (1967), 25–33

    1967

  27. [36]

    Jo Van Bulck, Daniel Moghimi, Michael Schwarz, Moritz Lipp, Marina Minkin, Daniel Genkin, Yarom Yuval, Berk Sunar, Daniel Gruss, and Frank Piessens

  28. [37]

    Walter, Konstantinos Athanasiou, and Panagiotis Manolios

    Andrew T. Walter, Konstantinos Athanasiou, and Panagiotis Manolios. 2025. Global Microprocessor Correctness in the Presence of Transient Execution - Support- ing Material. doi:10.5281/zenodo.15706553

    2025 doi

  29. [38]

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

    2023

  30. [39]

    jump if greater than

    Yuheng Yang, Thomas Bourgeat, Stella Lau, and Mengjia Yan. 2023. Pensieve: Microarchitectural Modeling for Security Evaluation. InProceedings of the 50th Annual International Symposium on Computer Architecture, ISCA 2023, Yan Solihin and Mark A. Heinrich (Eds.). ACM, 59:1–59:1...

    2023

  31. [1008]

    https://www.usenix.org/conference/usenixsecurity18/presentation/bulck

  32. [2011]

    InTools and Algorithms for the Construction and Analysis of Systems (TACAS)

    The "ACL2" Sedan Theorem Proving System. InTools and Algorithms for the Construction and Analysis of Systems (TACAS). doi:10.1007/978-3-642-19835-9_27

    doi

  33. [2018]

    In27th USENIX Security Symposium, USENIX Security 2018, William Enck and Adrienne Porter Felt (Eds.)

    Foreshadow: Extracting the Keys to the Intel SGX Kingdom with Transient Out-of-Order Execution. In27th USENIX Security Symposium, USENIX Security 2018, William Enck and Adrienne Porter Felt (Eds.). USENIX Association, 991–

    2018

  34. [2019]

    InProceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security

    Fallout: Leaking data on meltdown-resistant cpus. InProceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. 769–784

    2019

  35. [2020]

    In41th IEEE Symposium on Security and Privacy (S&P’20)

    LVI: Hijacking transient execution through microarchitectural load value injection. In41th IEEE Symposium on Security and Privacy (S&P’20). 1399–1417

  36. [2025]

    RTL Verification for Secure Speculation Using Contract Shadow Logic. In Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1, ASPLOS 2025, Lieven Eeckhout, Georgios Smaragdakis, Kaitai Liang, Ad...

    2025

Pith tools

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