A new technical paper titled “Closing the Gap: Leakage Contracts for Processors with Transitions and Glitches” was published by researchers at Graz University of Technology.
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.”
Find the technical paper here. Published September 2024.
Citation: Closing the Gap: Leakage Contracts for Processors with Transitions and Glitches. (2024). IACR Transactions on Cryptographic Hardware and Embedded Systems, 2024(4), 110-132.
Authors: Johannes Haring, Vedad Hadžić1and, Roderick Bloem (Graz University of Technology).
Leave a Reply