Program Verification Techniques for Hardware-Level Vulnerabilities
The TLS termination proxy had been running cleanly for eight months when the security audit flagged it. No memory corruption. No undefined behavior.
valgrind --leak-check=fullcame back silent. Yet the timing oracle was sitting right there in the MAC validation path — amemcmp()that returned early on the first differing byte, leaking information about the secret key at roughly 400 nanoseconds per bit. The code was correct. The hardware behavior was the vulnerability.Hardware-level vulnerabilities live in the gap between what your source code says and what the CPU actually does. Closing that gap requires a different class of tools than the ones most engineers reach for.
Speculative Execution: The CPU Is Running Code You Didn’t Write
Modern out-of-order processors don’t execute your program linearly. A Skylake-class core maintains a 224-entry reorder buffer and a 97-entry scheduler window — it speculatively executes branches before the condition resolves, using predictor state to guess which path to take. When the guess is wrong, it rolls back the architectural state (registers, flags). What it cannot roll back is the cache state.
This is the Spectre primitive: a mispredicted branch causes the processor to speculatively load from a secret address. The data never reaches a register architecturally, but the load populates a cache line. An attacker with timing access then measures which cache line got loaded — and reads the secret one bit at a time.
// Vulnerable gadget — the CPU speculatively loads array1[x] and
// uses the result as an index into array2, encoding the secret
// into cache state before the bounds check resolves.
if (x < array1_size) {
y = array2[array1[x] * 512];
}
On a 3 GHz Skylake, the branch predictor resolves in 14–20 cycles. The speculative window runs 100–200 cycles deep. That’s enough time for three cache-miss loads — plenty of speculation to exfiltrate a byte.
