Cryptographic implementations are often vulnerable to side-channel attacks, which exploit the physical emanations of the underlying component to retrieve the manipulated secrets. The most widely used countermeasure today is masking, which aims to randomize the manipulated data. VeriSiCC project aims to build new methods to automatically verify and generate proven masked cryptographic implementations. This project relies on the multidisciplinarity of its consortium, ranging from researchers specializing in formal methods and side-channel attacks to end-users, to design innovative software tools with the support of SMEs. These tools will allow industrial people to develop safe and effective protected implementations by reaching a high level of certification and certification bodies (represented in the consortium by ANSSI) to quickly and accurately verify implementations submitted to evaluations.
This first seminar aims to bring together experts in the field of formal verification and side-channel countermeasures to get an overview of the state-of-the-art on this topic and to identify new challenges.
Session chair: Thomas Roche
From Trivial Composition to Full Verification and an Application to Masking in Hardware
François-Xavier Standaert and Gaëtan Cassiers, Université Catholique de Louvain
In this talk, we will first introduce trivial composition with Probe Isolating Non-Interference (PINI) as a simple(r) way to ensure masked implementations secure at high orders. We will then discuss the application of trivial composition to improve the literature on masked hardware implementations for which a recent work by Moos et al. (CHES 2019) showed that most solutions published so far exhibit (local or composability) flaws at high security orders. We will finally describe a tool enabling the formal verification of masked hardware implementations at any order, that leverages trivial composition and can be used for the automated analysis of HDL codes.
Session chair: Jean-Sébastien Coron
Masking against Noisy Leakage: Models, Constructions and Proofs
Sebastian Faust, Technische Universität Darmstadt
Currently, side-channel evaluations of cryptographic implementations are done using two main approaches. The first one consists in performing practical side-channel measurements during the execution of a cryptographic algorithm on a specific device. The corresponding side-channel traces are then used to perform a leakage assessment and a side channel attack is eventually performed if leakages are identified. The second one consists in applying the same methodology by using simulated side-channel leakages instead of real side-channel measurements. Such a simulation is done in accordance with theoretical side-channel leakage models which are expected to fit with what are observed in the real world. In this talk, we will discuss the limitations of these two approaches and what could be done to improve the confidence level of the security of an implementation. We will also expose some further research topics which seem to be left aside.
Session chair: Benjamin Grégoire
Constant-Time Programming: Formal Verification & Secure Compilation
Vincent Laporte, INRIA
Side-channel attacks have been a very effective attack vector against cryptographic implementations. Side channels exist whenever several distrustful parties share some component of an execution environment, e.g., memory cache, branch predictor… These channels lead to attacks as soon as sensitive and otherwise protected data leaks through these channels. Software-based countermeasures can protect implementations against these attacks: constant-time programming ensures that only public information may leak through these channels. In this talk we first describe how these side-channel attacks and the corresponding security property can be formally defined. Then we show how the security of a program can be (semi-)automatically verified. Finally we study how compilers may break this security property and how to prove the opposite: that a compiler will preserve the security across the compilation.
Session chair: Aurélien Greuet
VerMI: Verification Tool for Masked Implementations
Svetla Nikova and Victor Arribas, COSIC, KULeuven
Masking is a widely used countermeasure against Side-Channel Attacks, nonetheless, the implementation of these countermeasures is challenging. Experimental security evaluation requires special equipment, a considerable amount of time, and extensive technical knowledge. Therefore, to automate and to speed up this process, a formal verification can be performed to asses the security of a design. In this work we present VerMI, a verification tool in the form of a logic simulator that checks the properties defined in Threshold Implementations to address the security of a hardware implementation for meaningful orders of security. The tool is designed so that any masking scheme can be evaluated. It accepts combinational and sequential logic and is able to analyze an entire cipher in short time. With the tool we have managed to spot a flaw in the round-based KECCAK implementation by Gross et al., published in DSD 2017.