IODINE: Verifying Constant-Time Execution of Hardware

Authors: 

Klaus v. Gleissenthall, Rami Gökhan Kıcı, Deian Stefan, and Ranjit Jhala, University of California, San Diego

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. 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.

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

BibTeX
@inproceedings {236334,
author = {Klaus v. Gleissenthall and Rami G{\"o}khan K{\i}c{\i} and Deian Stefan and Ranjit Jhala},
title = {{IODINE}: Verifying Constant-Time Execution of Hardware},
booktitle = {28th {USENIX} Security Symposium ({USENIX} Security 19)},
year = {2019},
isbn = {978-1-939133-06-9},
address = {Santa Clara, CA},
pages = {1411--1428},
url = {https://www.usenix.org/conference/usenixsecurity19/presentation/von-gleissenthall},
publisher = {{USENIX} Association},
month = aug,
}