Formale Methoden und Software Engineering für sichere Systeme (FoMSESS), 2024
Physical attacks pose a serious threat to hardware implementations of cryptographic algorithms. More precisely, the power consumption acquired during a cryptographic operation on a target hardware device in general leaks information about the processed secret key material. Additionally, an adversary who is capable to inject faults in an ongoing encryption or decryption processes can utilize the faulty ciphertexts or plaintexts to extract information about the applied secret key.
Hence, over the last two decades a plethora of countermeasures have been proposed to thwart these attacks individually. However, powerful attackers could combine both attack vectors such that combined protection mechanisms are required. Even for experienced designers, the implementation of such countermeasures is an error-prone and tedious task and practical evaluations are expensive and time-consuming.
This talk introduces the formal verification framework VERICA which analyzes gate-level netlists of countermeasures against physical attacks. In order to understand how VERICA works, we first introduce power side-channel and fault-injection attacks, discuss how both attack vectors can be modeled, and present established countermeasures. Based on this background, we present novel modeling strategies for hardware circuits providing protection against combined attacks. Eventually, we give more insights into VERICA and present several case studies in which we also reveal flaws in existing designs from the literature.