VERICA - Verification of Combined Attacks

Automated formal verification of security against simultaneous information leakage and tampering

Authors

  • Jan Richter-Brockmann Ruhr University Bochum, Horst Görtz Institute for IT Security, Bochum, Germany
  • Jakob Feldtkeller Ruhr University Bochum, Horst Görtz Institute for IT Security, Bochum, Germany
  • Pascal Sasdrich Ruhr University Bochum, Horst Görtz Institute for IT Security, Bochum, Germany
  • Tim Güneysu Ruhr University Bochum, Horst Görtz Institute for IT Security, Bochum, Germany; DFKI, Bremen, Germany

DOI:

https://doi.org/10.46586/tches.v2022.i4.255-284

Keywords:

SCA, FIA, Formal Verification, BDD, Symbolic Simulation, Combined Analysis

Abstract

Physical attacks, including passive Side-Channel Analysis and active Fault Injection Analysis, are considered among the most powerful threats against physical cryptographic implementations. These attacks are well known and research provides many specialized countermeasures to protect cryptographic implementations against them. Still, only a limited number of combined countermeasures, i.e., countermeasures that protect implementations against multiple attacks simultaneously, were proposed in the past. Due to increasing complexity and reciprocal effects, design of efficient and reliable combined countermeasures requires longstanding expertise in hardware design and security. With the help of formal security specifications and adversary models, automated verification can streamline development cycles, increase quality, and facilitate development of robust cryptographic implementations.
In this work, we revise and refine formal security notions for combined protection mechanisms and specifically embed them in the context of hardware implementations. Based on this, we present the first automated verification framework that can verify physical security properties of hardware circuits with respect to combined physical attacks. To this end, we conduct several case studies to demonstrate the capabilities and advantages of our framework, analyzing secure building blocks (gadgets), S-boxes build from Toffoli gates, and the ParTI scheme. For the first time, we reveal security flaws in analyzed structures due to reciprocal effects, highlighting the importance of continuously integrating security verification into modern design and development cycles.

Published

2022-08-31

Issue

Section

Articles

How to Cite

VERICA - Verification of Combined Attacks: Automated formal verification of security against simultaneous information leakage and tampering. (2022). IACR Transactions on Cryptographic Hardware and Embedded Systems, 2022(4), 255-284. https://doi.org/10.46586/tches.v2022.i4.255-284