KLEESPECTRE: Detecting Information Leakage through Speculative Cache Attacks via Symbolic Execution

Abhik Roychoudhury; Arnab Kumar Biswas; Guanhua Wang; Sudipta Chattopadhyay; Tulika Mitra

REVIEW 3 major objections 4 minor 29 references

KLEESPECTRE: Detecting Information Leakage through Speculative Cache Attacks via Symbolic Execution

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

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

Pith's one-line read Cache-aware symbolic execution catches Spectre-style leaks

desk verdict A genuinely useful integration of speculative symbolic execution with a symbolic LRU cache model, but the no-false-negatives claim outruns the termination-only cache model and collides with the paper's own trace-based threat model. read the letter →

arxiv 1909.00647 v1 pith:7TWF7PPU submitted 2019-09-02 cs.CR

Guanhua Wang , Sudipta Chattopadhyay , Arnab Kumar Biswas , Tulika Mitra , Abhik Roychoudhury This is my paper · ORCID

classification cs.CR

keywords SpectreattacksboundscheckbypasssymbolicexecutioncachesidechannelsspeculativemodelLRUreplacementvulnerabilitydetection

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 sets out to show that software testing can expose Spectre-style cache leaks if symbolic execution is taught what the processor does speculatively. At every branch whose condition depends on symbolic input, the tool KLEESPECTRE explores not just the two correctly predicted paths but also the two mis-predicted paths, and it records memory accesses made along those speculative paths that depend on data read outside its intended bounds. A symbolic model of a least-recently-used cache then converts the question "does this secret still sit in the cache when the program ends?" into an SMT formula; if the formula is satisfiable, an access-based attacker can still recover the secret. The paper reports that this engine finds all fifteen litmus-test variants of the Bounds Check Bypass attack and several real cryptographic gadgets, and that the cache model removes flagged leaks that later memory accesses would have evicted.

What carries the argument

The load-bearing mechanism is a symbolic cache-conflict formula restricted by Definition 4 to conflicts from normal-path accesses to speculatively accessed secret blocks. For each candidate secret block $i$ and each later normal-path access $j$, Equation 5 requires equal cache set and different tag, Equation 6 keeps only the last access to block $j$, and Equation 7 rules out a reload of block $i$; the implications in Equations 8-9 set a conflict bit, and Equation 10 compares the number of propagated conflicts with associativity $A$. The Speculative Execution Window bounds how far the mis-predicted paths are explored, and the tool's taint propagation marks every expression built from an out-of-bounds read as sensitive. This combination turns a microarchitectural question, whether an attacker will still see the secret in the cache at program termination, into an SMT query that a software symbolic executor can discharge.

What would settle it

Run the paper's modified litmus pattern (speculative secret read, then an eviction loop, then termination) on real hardware while the tool reports leakage-free; if a cache-timing probe still recovers the secret, the LRU conflict formula missed evictions and the central claim fails. Repeat with a second mis-speculated window touching the same cache set to test whether only normal-path conflicts matter.

Watch

Extended reading notes

Core claim

The central claim is that information leakage through speculative cache attacks can be detected, at the software-testing layer, by combining speculative symbolic execution with a symbolic least-recently-used cache model. For an unresolved branch with condition $\varphi$, KLEESPECTRE forks four states: taken and correctly predicted, taken and mis-predicted, not-taken and correctly predicted, and not-taken and mis-predicted; the mis-predicted states explore code that a real processor would run only transiently, bounded by a Speculative Execution Window. Memory loads in those transient paths that read out of bounds are treated as secret reads, and any later load whose address depends on such a read is recorded as a candidate leak site. Each recorded access sequence is paired with the normal-path accesses that follow, and Equations 5-10 encode whether a normal-path access conflicts with the secret block (same cache set, different tag) without the secret block being reloaded afterward. Equation 11 conjoins these constraints and asks whether fewer than $A$ propagated conflicts push the secret out; if $\Gamma_{\mathrm{spectre}}$ is satisfiable, the secret can remain cached at the observation point and the program is flagged. The paper reports correct detection on all fifteen litmus tests, detection of gadgets in ten cryptographic programs, and removal of several leakage alarms once eviction is accounted for; it also claims that over-approximation gives absence of false negatives within the modeled speculative window.

Load-bearing premise

The load-bearing premise is that the real cache evicts exactly as a least-recently-used cache would, and that only normal-path memory accesses made after the speculative secret access can push the secret out.

Editorial extensions

If this is right

The tool detects all fifteen Bounds Check Bypass litmus variants, a superset of what the compiler-mitigation baseline used for comparison reported catching.
Enabling the cache model removes false positives: several leakage flags on real cryptographic programs disappear because later normal-path memory accesses evict the secret before termination.
Detection results depend on cache configuration, so a program that leaks under a 2-way cache may be leakage-free under 4-way or 8-way caches under the model.
Larger speculative execution windows find more vulnerable branches and secret-read sites, for example 8 versus 14 vulnerable branches in one benchmark when the window grows from 50 to 100 instructions.
As an over-approximation, the approach is positioned to guarantee no false negatives for secret accesses inside the speculative window, at the cost of possible false positives.

Reading between the lines

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

The same four-way fork and conflict-formula machinery should transfer to other transient-execution channels, such as Meltdown-style faults, store-to-load forwarding, or speculation through memory dependencies, by replacing the out-of-bounds secret trigger and the cache-conflict equations accordingly.
The least-recently-used-specific formulas could be re-derived for pseudo-LRU or random replacement; comparing those models on the same litmus tests would show how much of the tool's precision depends on the replacement-policy assumption.
Because the tool already reports which secret loads survive to program end, it could be extended to quantify the number of bits exposed, for example how many cache sets a byte-indexed probe can distinguish, a measure the paper explicitly leaves for future work.
A guided mode that runs the cache model only at points where a fence could be inserted might turn detection into a mitigation tool: place fences only where the formula says the secret is still observable, reducing the overhead of blanket speculation barriers.

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.

Desk Editor's Note

read the letter

Short version: this is a solid tool paper with one load-bearing overclaim. The integration of speculative-path symbolic execution with a symbolic LRU cache model is genuinely new and useful; the cache model makes detection more precise in the synthetic eviction experiments. But the Section 7 no-false-negatives guarantee does not survive contact with the paper's own trace-based threat model, and that needs to be fixed or qualified before the paper is acceptable.

What's good: KLEESPECTRE builds on KLEE and explores mis-predicted paths within a speculative window, tracking secret-dependent addresses through nested speculation. The cache model uses standard LRU conflict equations, but applying them to the sequence of normal-path accesses after a speculative secret access is a real integration, not a trivial composition. On Kocher's 15 litmus tests it detects all, which is a clear improvement over the Microsoft compiler's pattern matching. The Figure 3 eviction experiment behaves as expected: as N grows, the secret block is evicted and the verdict flips to "leakage free". The real-benchmark evaluation is modest but reasonable for a subfield where no in-the-wild BCB gadget was known; the inserted-function experiments without cache modeling over-report, and cache modeling prunes some of those, which is a meaningful demonstration. The oo7 comparison is a fair baseline, not a circular appeal: the current result does not reduce to that prior work.

The main problem is the over-approximation claim. Section 7 says the tool has "absence of false negatives" and detects all leakage in real execution. The cache model in Section 4.2 only asks whether the secret block is still in cache at program termination; Section 5 says so explicitly for the access-based attacker. But Section 2 explicitly includes trace-based attackers who can observe cache state after any instruction. A block that is resident immediately after the speculative access is observable to a trace-based attacker even if later normal-path accesses evict it before return. The model's Equation 10 counts those later conflicts, concludes the block is gone, and returns "leakage free". So the no-false-negatives statement fails for a stated part of the threat model. This is not a minor wording issue; the RQ3 "leakage-free" rows are only sound for access-based attacks.

Also worth noting: the real-benchmark inserted vulnerable functions have no hardware ground truth, so the false-positive reduction is validated only against the tool's own cache model, not against actual hardware behavior. That is a soft spot, not fatal, if framed as a testing heuristic.

If the authors restrict the threat model to access-based attacks, or add a check for post-speculation transient residency, the central results stand. This paper is for people building Spectre detectors and microarchitectural testing tools; it deserves a serious referee who will push on the threat-model mismatch and the artifact. I would send it to review rather than desk reject.

Referee Report

3 major / 4 minor

Summary. The paper presents KLEESPECTRE, an extension of the KLEE symbolic execution engine that adds speculative execution paths and a symbolic cache model. For each conditional branch, KLEESPECTRE explores both correctly predicted and mispredicted legs up to a bounded Speculative Execution Window (SEW), records memory accesses that are dependent on potential secrets (identified as out-of-bound accesses), and then builds a symbolic cache-conflict formula to decide whether a speculatively loaded secret block can still be observed in the cache after program termination. The tool is evaluated on fifteen Kocher litmus tests and ten cryptographic benchmarks, with additional experiments inserting Spectre-v1 gadgets to measure the effect of cache modeling. The authors report detection of all litmus-test variants and a reduction of reported leaks when the cache model is enabled, and they claim in Section 7 that the method is an over-approximation with no false negatives.

Significance. If the central claims were fully supported, KLEESPECTRE would be a useful contribution: it is one of the first symbolic-execution tools to combine speculative path exploration with a concrete LRU cache model, it ships with public code and benchmarks, and the synthetic eviction experiment in Figure 3 provides a clear check that the cache model behaves as intended on a simple access-based attack scenario. The comparison with oo7 and SPECTECTOR also positions the contribution usefully. However, the strength of the contribution is limited by the gap between the stated trace-based threat model and the termination-only cache observation, and by the fact that the Section 7 no-false-negatives guarantee is not entailed by the cache model as defined.

major comments (3)

[§7 vs. §2 and §5] The claim in Section 7 that KLEESPECTRE has 'absence of false negatives' and 'guarantees that all leakage in the real execution can be detected' is not supported for the trace-based attacker defined in Section 2. Section 5 states that the symbolic cache model is constructed 'upon the termination of an execution,' and Equations 5-10 in Section 4.2 decide whether a secret block remains in the cache after all normal-path accesses have been processed. A trace-based attacker, however, may observe the cache immediately after the speculative access, before later normal-path accesses evict the secret block. For such an attacker, a secret-dependent block that is resident right after the leak instruction is a genuine leak even if it is gone at program termination. The cache model would report 'leakage free' in that case, so the unconditional no-false-negatives statement fails for a stated part of the paper's own threat model. The RQ3 'leakage-free' rows in Table 3 should be explicitly restricted to access-based attackers at program termination, and Section 7 should be revised accordingly.
[§4.2, Definition 4 and Equations 5-10] The cache model is not an over-approximation of real miss/eviction behavior, so the Section 7 guarantee is also too strong even for access-based attackers. Definition 4 only counts conflicts from normal-path accesses (rj in Nt) to speculatively accessed secret blocks (ri in Ns); conflicts caused by other speculative accesses, including later speculation windows, are ignored. Equations 6 and 7 treat every unique normal-path access to a conflicting set as an eviction, but whether that access actually misses and replaces the secret block depends on the initial cache state and on whether the accessed line is already resident. With a non-empty initial cache, a normal-path access can hit an existing line and change LRU order without evicting the secret block, so the model can over-approximate evictions and return 'leakage free' when a real access-based leak exists. To substantiate the no-false-negatives claim, the authors need either to extend the model with initial cache states and all interfering speculative accesses, or to weaken the claim to correctness with respect to the simplified cold-cache, single-speculation-window LRU model.
[§6.3 and Table 3] The RQ3 evaluation does not exercise the trace-based threat model, so the reported precision gain of cache modeling is only demonstrated for one specific observation point. The inserted gadgets and the eviction loop in Listing 3 are designed so that the secret block is either present or absent at the end of the program, but no experiment observes the cache immediately after the speculative leak instruction. Consequently, Table 3 cannot validate the claim that the cache model 'can verify whether the sensitive data leakage due to speculative execution can be observed by an attacker at a given program point' (Abstract). An additional experiment with an early observation point, or an explicit statement that the tool only targets access-based attackers, is needed to align the evaluation with the claimed scope.

minor comments (4)

[§3, Equation (1)] Equation (1) uses 'taд' with a Cyrillic character instead of 'tag'; this appears to be a rendering artifact and should be fixed throughout the paper.
[§3 and §6.2] The paper is inconsistent about the unit of SEW: Section 3 describes it as the number of speculatively executed instructions, while Section 6.2 says 'micro-instructions' and Table 2 reports average instruction counts close to the SEW values. Please clarify whether SEW counts instructions or micro-operations.
[§6.1] The statement that 'array2 was mapped to the first cache set' is an assumption about the concrete address layout after linking; the experiment description should state how this mapping is ensured or verified, since the eviction thresholds in Figure 3 depend on it.
[§4.2, Property 2] Property 2 says that any element in tail(Γ, <*,*, ms>) 'must be accessed' following ms in any concrete execution, but Γ may omit non-secret-dependent memory accesses that still affect the cache; the wording should be qualified to avoid implying that Γ is a complete memory-access trace.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the secret definition is an explicit threat-model choice, external benchmarks are used, and self-citations are not load-bearing.

full rationale

KLEESPECTRE's derivation chain is not circular. The tool's secret definition—“we consider that r accesses a secret if and only if r points to an out-of-bound memory location” (Section 4.1)—is an explicit threat-model choice rather than a hidden equation that forces the evaluation outcomes; the litmus tests are taken from Kocher's external benchmark suite and the real benchmarks from libTomCrypt, openssl, hpn-ssh, and Linux-tegra. The symbolic cache model (Section 4.2, Definitions 3–4 and Equations 5–11) is an independent LRU-conflict construction whose satisfiability determines whether a speculative secret block survives to program termination; Equation 11 is not a restatement of the experimental results. No fitted parameter is renamed as a prediction; SEW is a configurable bound, and cache associativity is varied experimentally. The paper self-cites oo7 [25] and CACHEFIX [8], but only as baseline/comparison and related work, so no load-bearing premise depends on these citations. The Section 7 statement that KLEESPECTRE “guarantees that all leakage in the real execution can be detected” is a soundness claim that is not fully proven and may be too strong under the paper's own trace-based attacker definition and termination-time cache model, but that is an unsupported over-claim, not circularity: the conclusion is not equal by definition to the inputs.

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

The central claim rests on a small set of microarchitectural and threat-model assumptions: speculative loads persist in cache, all branches are mispredictable, out-of-bound accesses are secrets, LRU replacement, and an access-based attacker. The only hand-chosen numeric parameter is the speculative execution window SEW. No new entities are introduced.

free parameters (1)

Speculative Execution Window (SEW) = 50 or 100 micro-instructions in experiments
SEW bounds the number of speculatively executed instructions after a branch; results in Tables 2 and 3 depend on it, and it is set by the user rather than derived from target hardware.

assumptions (5)

domain assumption Memory accesses along a mispredicted path update the cache and these updates are not rolled back when the speculation is squashed.
Section 2 states 'the cache state is not fully rolled back' after speculative execution.
domain assumption Every conditional branch in the program can be mispredicted by an attacker.
Section 2: 'We assume that all conditional branches in a program are potentially vulnerable.'
domain assumption A memory address is a secret if it is an out-of-bound access along a speculative path.
Section 4.1: 'we consider that any out-of-bound memory access along a speculative path points to a secret.'
domain assumption The cache under analysis uses LRU replacement.
Section 4.2: 'we instantiate KLEESPECTRE for the least recently used (LRU) replacement policy.'
domain assumption The attacker observes the cache state only at program termination (access-based model).
Section 4.2 and Section 6 model the access-based attack that probes the cache at termination; trace-based observation is mentioned but not modeled in the main check.

how reviews work

0 comments

Cite this review

Pith. "Pith review of KLEESPECTRE: Detecting Information Leakage through Speculative Cache Attacks via Symbolic Execution." pith.science (2026). https://pith.science/paper/7TWF7PPU

@misc{pith2026190900647,
  author       = {Pith},
  title        = {Pith review of: KLEESPECTRE: Detecting Information Leakage through Speculative Cache Attacks via Symbolic Execution},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/7TWF7PPU}},
  note         = {Machine review of arXiv:1909.00647}
}

read the original abstract

Spectre attacks disclosed in early 2018 expose data leakage scenarios via cache side channels. Specifically, speculatively executed paths due to branch mis-prediction may bring secret data into the cache which are then exposed via cache side channels even after the speculative execution is squashed. Symbolic execution is a well-known test generation method to cover program paths at the level of the application software. In this paper, we extend symbolic execution with modelingof cache and speculative execution. Our tool KLEESPECTRE, built on top of the KLEE symbolic execution engine, can thus provide a testing engine to check for the data leakage through cache side-channel as shown via Spectre attacks. Our symbolic cache model can verify whether the sensitive data leakage due to speculative execution can be observed by an attacker at a given program point. Our experiments show that KLEESPECTREcan effectively detect data leakage along speculatively executed paths and our cache model can further make the leakage detection much more precise.

Figures

Figures reproduced from arXiv: 1909.00647 by the authors.

**Figure 1.** The example code, and its normal execution paths along with the execution paths with branch speculation. (a) example code where b1 and b2 capture branch instructions. A, B and C indicate the corresponding basic blocks. (b) Execution paths explored by classic symbolic execution. pT #, pF # represent normal paths that go along the true or false leg of a branch. (c) Symbolic execution tree explored by KLEESPECTRE . spT… view at source ↗

**Figure 2.** Partial speculative execution paths of example code. m# represents a memory access on a path. The memory access in red color brings in a sensitive cache state. Cache modeling in KLEESPECTRE : KLEESPECTRE computes the set of memory access sequences that are potentially [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗

**Figure 3.** The detection result of KLEESPECTRE with cache model enabled. #-way represents a cache setting with #-way set associative cache. greater than array1_size can bring in potentially sensitive data. This is because array1[idx] can point outside of array1[] when the branch at line 8 is mis-predicted. The sensitive data can subsequently be leaked to the cache state by accessing array2[] at line 9. The question remains wh… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

29 extracted references · 27 canonical work pages

[1]

Intel Xeon Gold 6126 Processor

2017. Intel Xeon Gold 6126 Processor. https://ark.intel.com/ products/120483/Intel-Xeon-Gold-6126-Processor-19-25M- Cache-2-60-GHz- . (2017)

work page 2017
[2]

www.uclibc.org

2018. www.uclibc.org. (2018)

work page 2018
[3]

Onur Acıiçmez, Billy Bob Brumley, and Philipp Grabher. 2010. New Results on Instruction Cache Attacks. In Cryptographic Hardware and Embedded Systems, CHES 2010, Stefan Mangard and François-Xavier Standaert (Eds.). Springer Berlin Heidelberg, 110–124

work page 2010
[4]

Robert Brotzman, Shen Liu, Danfeng Zhang, Gang Tan, and Mahmut Kandemir. 2019. CaSym: Cache aware symbolic execution for side channel detection and mitigation. In CaSym: Cache Aware Symbolic Execution for Side Channel Detection and Mitigation. IEEE, 0

work page 2019
[5]

Cristian Cadar, Daniel Dunbar, Dawson R Engler, et al. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Com- plex Systems Programs.. In OSDI, V ol. 8. 209–224

work page 2008
[6]

Claudio Canella, Jo Van Bulck, Michael Schwarz, Moritz Lipp, Ben- jamin von Berg, Philipp Ortner, Frank Piessens, Dmitry Evtyushkin, and Daniel Gruss. 2018. A Systematic Evaluation of Transient Execu- tion Attacks and Defenses. arXiv. org e-Print archive(2018)

work page 2018
[7]

Chandler Carruth. 2018. Speculative Load Hardening. https: //docs.google.com/document/d/1wwcfv3UV9ZnZVcGiGuoITT_ 61e_Ko3TmoCS3uXLcJR0. (2018)

work page 2018
[8]

Sudipta Chattopadhyay and Abhik Roychoudhury. 2018. Symbolic verification of cache side-channel freedom. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 37, 11 (2018), 2812–2823

work page 2018

Show all 29 references

[9]

Microsoft community. 2018. C++ Developer Guidance for Speculative Execution Side Channels. https://docs.microsoft.com/en-us/cpp/ security/developer-guidance-speculative-execution. (2018)

2018
[10]

Goran Doychev, Boris Köpf, Laurent Mauborgne, and Jan Reineke
[11]

Dmitry Evtyushkin, Ryan Riley, Nael CSE Abu-Ghazaleh, ECE, and Dmitry Ponomarev. 2018. BranchScope: A New Side-Channel Attack on Directional Branch Predictor. SIGPLAN Not. 53, 2 (March 2018), 693–707. https://doi.org/10.1145/3296957.3173204

2018
[12]

Vijay Ganesh and David L Dill. 2007. A decision procedure for bit- vectors and arrays. In International Conference on Computer Aided Verification. Springer, 519–531

2007
[13]

José González and Antonio González. 1997. Speculative execution via address prediction and data prefetching. In International conference on supercomputing. Citeseer, 196–203

1997
[14]

Marco Guarnieri, Boris Köpf, José F Morales, Jan Reineke, and Andrés Sánchez. 2018. SPECTECTOR: Principled Detection of Speculative Information Flows. arXiv preprint arXiv:1812.08639 (2018)

2018 arXiv
[15]

Trevor Hansen, Peter Schachte, and Harald Søndergaard. 2009. State joining and splitting for the symbolic execution of binaries. In Interna- tional Workshop on Runtime Verification. Springer, 76–92

2009
[16]

James C. King. 1976. Symbolic Execution and Program Testing. Com- mun. ACM 19 (1976). Issue 7

1976
[17]

Paul Kocher. [n. d.]. Spectre Mitigations in Microsoft’s C/C++ Compiler. https://www.paulkocher.com/doc/ MicrosoftCompilerSpectreMitigation.html. ([n. d.])
[18]

Paul Kocher, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. 2018. Spectre Attacks: Exploiting Specu- lative Execution. ArXiv e-prints (Jan. 2018). arXiv:1801.01203

2018 arXiv
[19]

V olodymyr Kuznetsov, Johannes Kinder, Stefan Bucur, and George Candea. 2012. Efficient state merging in symbolic execution. In Acm Sigplan Notices, V ol. 47. ACM, 193–204

2012
[20]

Fangfei Liu, Yuval Yarom, Qian Ge, Gernot Heiser, and Ruby B Lee
[21]

Oleksii Oleksenko, Bohdan Trach, Tobias Reiher, Mark Silberstein, and Christof Fetzer. 2018. You Shall Not Bypass: Employing data dependencies to prevent Bounds Check Bypass . Technical Report arXiv:1805.08506, https://arxiv.org/abs/1805.08506. arxiv

2018 arXiv
[22]

In 2015 IEEE Symposium on Security and Privacy

Last-level cache side-channel attacks are practical. In 2015 IEEE Symposium on Security and Privacy. IEEE, 605–622

2015
[23]

Colin Percival. 2005. Cache missing for fun and profit. In Proc. of BSDCan 2005

2005
[24]

Dag Arne Osvik, Adi Shamir, and Eran Tromer. 2006. Cache Attacks and Countermeasures: The Case of AES. In Topics in Cryptology – CT-RSA 2006, David Pointcheval (Ed.). Springer Berlin Heidelberg, 1–20
[25]

Guanhua Wang, Sudipta Chattopadhyay, Ivan Gotovchits, Tulika Mitra, and Abhik Roychoudhury. 2018. oo7: Low-overhead defense against spectre attacks via binary analysis. arXiv preprint arXiv:1807.05843 (2018)

2018 arXiv
[26]

Jan Reineke, Daniel Grund, Christoph Berg, and Reinhard Wilhelm
[29]

Meng Wu and Chao Wang. 2019. Abstract interpretation under specula- tive execution. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 802– 815

2019
[2007]

Real-Time Systems 37, 2 (2007), 99–122

Timing predictability of cache replacement policies. Real-Time Systems 37, 2 (2007), 99–122

2007
[2015]

ACM Transactions on Information and System Security (TISSEC) 18, 1 (2015), 4

Cacheaudit: A tool for the static analysis of cache side channels. ACM Transactions on Information and System Security (TISSEC) 18, 1 (2015), 4

2015

Pith tools

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

[1] [1]

Intel Xeon Gold 6126 Processor

2017. Intel Xeon Gold 6126 Processor. https://ark.intel.com/ products/120483/Intel-Xeon-Gold-6126-Processor-19-25M- Cache-2-60-GHz- . (2017)

work page 2017

[2] [2]

www.uclibc.org

2018. www.uclibc.org. (2018)

work page 2018

[3] [3]

Onur Acıiçmez, Billy Bob Brumley, and Philipp Grabher. 2010. New Results on Instruction Cache Attacks. In Cryptographic Hardware and Embedded Systems, CHES 2010, Stefan Mangard and François-Xavier Standaert (Eds.). Springer Berlin Heidelberg, 110–124

work page 2010

[4] [4]

Robert Brotzman, Shen Liu, Danfeng Zhang, Gang Tan, and Mahmut Kandemir. 2019. CaSym: Cache aware symbolic execution for side channel detection and mitigation. In CaSym: Cache Aware Symbolic Execution for Side Channel Detection and Mitigation. IEEE, 0

work page 2019

[5] [5]

Cristian Cadar, Daniel Dunbar, Dawson R Engler, et al. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Com- plex Systems Programs.. In OSDI, V ol. 8. 209–224

work page 2008

[6] [6]

Claudio Canella, Jo Van Bulck, Michael Schwarz, Moritz Lipp, Ben- jamin von Berg, Philipp Ortner, Frank Piessens, Dmitry Evtyushkin, and Daniel Gruss. 2018. A Systematic Evaluation of Transient Execu- tion Attacks and Defenses. arXiv. org e-Print archive(2018)

work page 2018

[7] [7]

Chandler Carruth. 2018. Speculative Load Hardening. https: //docs.google.com/document/d/1wwcfv3UV9ZnZVcGiGuoITT_ 61e_Ko3TmoCS3uXLcJR0. (2018)

work page 2018

[8] [8]

Sudipta Chattopadhyay and Abhik Roychoudhury. 2018. Symbolic verification of cache side-channel freedom. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 37, 11 (2018), 2812–2823

work page 2018