- Main
Verifying Constant-Time Execution of Hardware
- Kici, Rami Gokhan
- Advisor(s): Jhala, Ranjit
Abstract
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.
Main Content
Enter the password to open this PDF file:
-
-
-
-
-
-
-
-
-
-
-
-
-
-