16 citations · 16 across the 2 of their papers we have counts for
4 papers
Solver-Aided Constant-Time Circuit Verification
Rami Gokhan Kici, Klaus v. Gleissenthall, Deian Stefan +1
We present Xenon, a solver-aided method for formally verifying that Verilog hardware executes in constant-time. Xenon scales to realistic hardware designs by drastically reducing t…
Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Marco Vassena, Craig Disselkoen, Klaus V. Gleissenthall +5
We introduce BLADE, a new approach to automatically and efficiently eliminate speculative leaks from cryptographic code. BLADE is built on the insight that to stop leaks via specul…
Iodine: Verifying Constant-Time Execution of Hardware
Klaus v. Gleissenthall, Rami Gökhan Kıcı, Deian Stefan +1
To be secure, cryptographic algorithms crucially rely on the underlying hardware to avoid inadvertent leakage of secrets through timing side channels. Unfortunately, such timing ch…
Constant-Time Foundations for the New Spectre Era
Sunjay Cauligi, Craig Disselkoen, Klaus v. Gleissenthall +4
The constant-time discipline is a software-based countermeasure used for protecting high assurance cryptographic implementations against timing side-channel attacks. Constant-time…