Out-of-order processors execute instructions speculatively: guessing a branch, running ahead, and discarding the results if the guess was wrong. Every verification method checked that discarded results never reached architectural state, and they never did. In January 2018 researchers showed that the discarded work still left footprints in the cache, and that an attacker could read secrets from those footprints by timing memory accesses (fact C3).
What does an escape in which every result was correct teach about verification?
Fact | Source |
|---|---|
Speculatively executed instructions whose results are discarded can still change microarchitectural state, such as which lines are in the cache | Kocher et al.; Lipp et al. (fact C3) |
An attacker can infer that state by timing accesses, and so read data the program was never allowed to see | Fact C3 |
Disclosed in January 2018, after being reported to vendors in June 2017 | Fact C3 |
Mitigations were first mostly software and microcode: KPTI for Meltdown; retpoline and microcode controls such as IBRS for Spectre variant 2; later processors added hardware changes | Fact C6 |
Every functional check in this course compares what the design computes with what it should compute. Here the computation was right. The leak was in a channel the specification never mentioned: timing, which depended on secret data through the cache. The instruction set defines results, not timing, so the ISS (lesson 15.5) agreed with the RTL at every instruction. A lock-step comparison, a scoreboard or a formal proof against the architectural specification would all pass.
Check | What it compares | Sees the leak? |
|---|---|---|
Lock-step ISS comparison | Architectural results per instruction | No: results are correct |
Formal equivalence to an architectural model | Architectural state | No: discarded state is not architectural |
Performance checks | Throughput and latency against targets | No: they measure speed, not whether timing depends on secrets |
Security property: observable timing independent of secrets | Information flow from secrets to timing | Yes, if someone states it |
This is the pool argument of the whole course in its starkest form: the bug was outside the pool of every technique used, because it was outside the specification. Lesson 2.1's point that verification checks against a specification has a hard edge: what the specification does not say cannot be checked.
Mitigations (documented, fact C6): operating systems isolated kernel page tables (KPTI), compilers changed indirect branches (retpoline), microcode added controls, and later processors changed hardware.
A new class of property (the course's reading): microarchitectural information flow became something processor teams must specify and verify, not assume.
Research into verifying it (the course's reading): information-flow tracking and formal non-interference checks applied to microarchitecture, as in lesson 15.2.
Question | Answer |
|---|---|
What failed? | Secret-dependent microarchitectural traces of speculative execution, readable by timing (documented) |
Where could it have been caught? | Only by a security property about timing or information flow, stated before verification (the course's reading) |
Why was it not caught? | Unspecified: the behaviour was outside every specification the checks used (the course's reading) |
What changed? | Software, microcode and later hardware mitigations; microarchitectural leakage became a verification concern (documented, then the course's reading) |
The ISS checks architectural results, which were correct; the leak was in timing, which the ISA does not define.
Unspecified: the behaviour was outside every specification the checks used.
Spectre and Meltdown leaked secrets while every architectural result was correct (documented).
No functional check could flag it: the leak was outside the specification.
State and verify properties about what must not be observable.