REVIEW 1 cited by
SPECTECTOR: Principled Detection of Speculative Information Flows
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Signed reviews
read the original abstract
Since the advent of SPECTRE, a number of countermeasures have been proposed and deployed. Rigorously reasoning about their effectiveness, however, requires a well-defined notion of security against speculative execution attacks, which has been missing until now. In this paper (1) we put forward speculative non-interference, the first semantic notion of security against speculative execution attacks, and (2) we develop SPECTECTOR, an algorithm based on symbolic execution to automatically prove speculative non-interference, or to detect violations. We implement SPECTECTOR in a tool, which we use to detect subtle leaks and optimizations opportunities in the way major compilers place SPECTRE countermeasures. A scalability analysis indicates that checking speculative non-interference does not exhibit fundamental bottlenecks beyond those inherited by symbolic execution.
Forward citations
Cited by 1 Pith paper
-
KLEESPECTRE: Detecting Information Leakage through Speculative Cache Attacks via Symbolic Execution
KLEESPECTRE detects Spectre variant 1 (bounds check bypass) leaks by symbolically executing mispredicted paths and checking whether the secret-dependent cache state survives to the end of execution.
Discussion (0). Continue with ORCID to comment.