Side-channels—through cache access patterns, timing differences, and speculative execution—can expose confidential information across traditional isolation barriers, thereby putting sensitive data at risk. While practitioners employ countermeasures like constant-time programming, history shows that clever attacks repeatedly circumvent these defenses.
In this talk, I will discuss how to use techniques from programming languages and formal verification to prove that a hardware design can be used securely without side-channel leaks. I will particularly focus on constructive leakage proofs via simulators—a new proof method for verifying that a hardware design does not leak more than intended. In constructive leakage proofs, the user provides an explicit description of what a hardware design is expected to leak. To show that this leakage description correctly captures all actual leakage, the user constructs a simulator—–another hardware design that faithfully replicates all attacker-observable behavior using only explicitly leaked secrets. Unlike existing proof methods, simulation-based proofs expose an executable proof object—–the simulator. As the simulator is just another hardware design, it can be written, executed, and debugged like any other program. This makes simulation-based proofs particularly well suited for hardware designers who may not be experts in formal verification.
We implement our method in a tool called Pantomime, and use it to write and verify AIMCore, a five-stage in-order processor, its leakage description, and simulator, as well as a side-channel-hardened version of the core. We used AIMCore’s leakage description to check for side-channel leaks in cryptographic libraries, which uncovered two new vulnerabilities in wolfSSL that have both been assigned CVEs.