Power Contracts: Provably Complete Power Leakage Models for Processors

Roderick Bloem; Barbara Gigerl; Marc Gourjon; Vedad Hadžić; Stefan Mangard; Robert Primas

Paper 2022/565

Power Contracts: Provably Complete Power Leakage Models for Processors

Roderick Bloem

, Graz University of Technology

Barbara Gigerl

, Graz University of Technology

Marc Gourjon

, Hamburg University of Technology, NXP (Germany)

Vedad Hadžić

, Graz University of Technology

Stefan Mangard

, Graz University of Technology

Robert Primas

, Graz University of Technology

Abstract

The protection of cryptographic software implementations against power-analysis attacks is critical for applications in embedded systems. A commonly used algorithmic countermeasure against these attacks is masking, a secret-sharing scheme that splits a sensitive computation into computations on multiple random shares. In practice, the security of masking schemes relies on several assumptions that are often violated by microarchitectural side-effects of CPUs. Many past works address this problem by studying these leakage effects and building corresponding leakage models that can then be integrated into a software verification workflow. However, these models have only been derived empirically, putting in question the otherwise rigorous security statements made with verification. We solve this problem in two steps. First, we introduce a contract layer between the (CPU) hardware and the software that allows the specification of microarchitectural side-effects on masked software in an intuitive language. Second, we present a method for proving the correspondence between contracts and CPU netlists to ensure the completeness of the specified leakage models. Then, any further security proofs only need to happen between software and contract, which brings benefits such as reduced verification runtime, improved user experience, and the possibility of working with vendor-supplied contracts of CPUs whose design is not available on netlist-level due to IP restrictions. We apply our approach to the popular RISC-V IBEX core, provide a corresponding formally verified contract, and describe how this contract could be used to verify masked software implementations.

Note: The main difference between this version and the one published at CCS '22 is the inclusion of the contract code in the Appendix.

Metadata

Available format(s): PDF
Category: Foundations
Publication info: Published elsewhere. CCS '22
DOI: 10.1145/3548606.3560600
Keywords: Power side-channel Leakage model Verification Contract Domain-specific language Masking Probing security
Contact author(s): vedad hadzic @ iaik tugraz at
History: 2022-12-12: revised; 2022-05-10: received; See all versions
Short URL: https://ia.cr/2022/565
License: CC BY

BibTeX

@misc{cryptoeprint:2022/565,
      author = {Roderick Bloem and Barbara Gigerl and Marc Gourjon and Vedad Hadžić and Stefan Mangard and Robert Primas},
      title = {Power Contracts: Provably Complete Power Leakage Models for Processors},
      howpublished = {Cryptology ePrint Archive, Paper 2022/565},
      year = {2022},
      doi = {10.1145/3548606.3560600},
      note = {\url{https://eprint.iacr.org/2022/565}},
      url = {https://eprint.iacr.org/2022/565}
}