Iodine: Verifying Constant-Time Execution of Hardware
This addresses security vulnerabilities in cryptographic hardware for developers and users, though it is incremental as it builds on existing verification methods.
The paper tackled the problem of timing side channels in hardware by presenting Iodine, a clock-precise approach to verify constant-time execution, which successfully verified open-source designs in seconds and discovered two constant-time violations in a floating-point unit and an RSA encryption module.
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. In this paper, we present Iodine: a clock precise, constant-time approach to eliminating timing side channels in hardware. Iodine succeeds in verifying various open source hardware designs in seconds and with little developer effort. Iodine also discovered two constant-time violations: one in a floating-point unit and another one in an RSA encryption module.