Title:

Computer-Aided Verification of Countermeasures against Physical Attacks

 

Abstract:

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 able 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 task and practical evaluations are expensive and time-consuming.

This talk introduces the formal verification framework VERICA which is capable of analyzing 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 revealed flaws in existing designs from the literature.

 

Speaker:

Dr. Jan Richter-Brockmann

Ruhr-Universität Bochum