CryptoDB
Closing the Gap: Leakage Contracts for Processors with Transitions and Glitches
| Authors: | |
|---|---|
| Download: | |
| Abstract: | Security verification of masked software implementations of cryptographic algorithms must account for microarchitectural side-effects of CPUs. Leakage contracts were proposed to provide a formal separation between hardware and software verification, ensuring interoperability and end-to-end security for independently verified components. However, previously proposed leakage contracts did not consider a class of ephemeral hardware effects called glitches, which leaves a considerable gap between security models and the capabilities of real-world attackers. We address this issue by extending the model for leakage contracts to account for glitches and transitions. We further present the first end-to-end verification tool for transient leakage contracts. Our hardware and software verification rely on the same contract as a single source of truth, facilitating fully machine-checked verification from the hardware gate level to the software. By allowing contracts to be written in the C programming language we make power contracts more accessible and intuitive for system-level engineers. To showcase the efficacy of our approach, we apply it to the RISC-V Ibex core. We show that it is possible to write a power contract for Ibex without any modifications to the hardware design. Using this contract, we prove end-to-end security between masked software and gate-level hardware. |
BibTeX
@article{tches-2024-34459,
title={Closing the Gap: Leakage Contracts for Processors with Transitions and Glitches},
journal={IACR Transactions on Cryptographic Hardware and Embedded Systems},
publisher={Ruhr-Universität Bochum},
volume={2024},
pages={110-132},
url={https://tches.iacr.org/index.php/TCHES/article/view/11785},
doi={10.46586/tches.v2024.i4.110-132},
author={Johannes Haring and Vedad Hadži´c and Roderick Bloem},
year=2024
}