Paper 2020/1294

Coco: Co-Design and Co-Verification of Masked Software Implementations on CPUs

Barbara Gigerl, Vedad Hadzic, Robert Primas, Stefan Mangard, and Roderick Bloem


The protection of cryptographic implementations against power analysis attacks is of critical importance for many applications in embedded systems. The typical approach of protecting against these attacks is to implement algorithmic countermeasures, like masking. However, implementing these countermeasures in a secure and correct manner is challenging. Masking schemes require the independent processing of secret shares, which is a property that is often violated by CPU microarchitectures in practice. In order to write leakage-free code, the typical approach in practice is to iteratively explore instruction sequences and to empirically verify whether there is leakage caused by the hardware for this instruction sequence or not. Clearly, this approach is neither efficient, nor does it lead to rigorous security statements. In this paper, we overcome the current situation and present the first approach for co-design and co-verification of masked software implementations on CPUs. First, we present Coco, a tool that allows us to provide security proofs at the gate-level for the execution of a masked software implementation on a concrete CPU. Using Coco , we analyze the popular 32-bit RISC-V Ibex core, identify all design aspects that violate the security of our tested masked software implementations and perform corrections, mostly in hardware. The resulting secured Ibex core has an area overhead around 10%, the runtime of software on this core is largely unaffected, and the formal verification with Coco of an, e.g., first-order masked Keccak S-box running on the secured Ibex core takes around 156 seconds. To demonstrate the effectiveness of our suggested design modifications, we perform practical leakage assessments using an FPGA evaluation board.

Available format(s)
Publication info
Published elsewhere. MINOR revision.30th USENIX Security Symposium (USENIX Security '21)
verificationmaskingblock ciphersimplementationside-channel analysisglitchespower analysis
Contact author(s)
barbara gigerl @ iaik tugraz at
vedad hadzic @ iaik tugraz at
robert primas @ iaik tugraz at
stefan mangard @ iaik tugraz at
roderick bloem @ iaik tugraz at
2021-06-08: last of 3 revisions
2020-10-19: received
See all versions
Short URL
Creative Commons Attribution


      author = {Barbara Gigerl and Vedad Hadzic and Robert Primas and Stefan Mangard and Roderick Bloem},
      title = {Coco: Co-Design and Co-Verification of Masked Software Implementations on CPUs},
      howpublished = {Cryptology ePrint Archive, Paper 2020/1294},
      year = {2020},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.