To be secure, cryptographic algorithms crucially rely on the underlying hardware

to avoid inadvertent leakage of secrets through timing side channels.

Unfortunately, such timing channels are ubiquitous in modern hardware, due to

its labyrinthine fast-paths and optimizations. A promising way to avoid timing

vulnerabilities is to devise—and verify—conditions under which a hardware design

is free of timing variability, i.e., executes in constant-time. While there have

been significant strides in verifying constant time execution for software,

these efforts focus on sequential, cryptographic code. Unfortunately, this makes

them unsuitable for hardware designs which are inherently concurrent and

long-lived.

First, we present Iodine: a clock-precise, constant-time approach to eliminating

timing side channels in hardware. To realize Iodine, we first define a new

notion of constant-time execution that is suitable for concurrent and long lived

computations. Our definition is based on the notion of influence sets containing

all cycles whose inputs influenced the current computation. We then show how to

reduce the problem of verifying constant time execution to the standard problem

of verifying assertion validity.

Second, we present Xenon, which extends Iodine and scales to realistic hardware

designs by exploiting modularity in VERILOG code via a notion of module

summaries. Xenon drastically reduces the effort needed to localize the causes of

verification failure via a novel constant-time counterexamples which are used to

automatically synthesize minimal secrecy assumptions that enable constant-time

verification. We show how Xenon’s summaries and assumption synthesis enable the

verification of a variety of circuits including a highly modular AES-256

implementation where modularity cuts verification from six hours to under three

seconds, and ScarV, a timing channel hardened RISC-V micro-controller whose size

exceeds previously verified designs by an order of magnitude.

We find that Iodine and Xenon present a practical way to specify and verify the

absence of timing channels in hardware. They succeed in verifying various open

source hardware designs in seconds and with little developer effort thanks to

generated secrecy assumptions. They also discovered two constant-time

violations: one in a floating-point unit and another one in an RSA encryption

module.