VeriSiCC Seminar 2019
Verification and Generation of Side-Channel Countermeasures
September, 25th 2019, Paris, France
VeriSiCC Seminar 2019 is a single-day seminar organized by all the partners of FUI25 VeriSiCC project and that will take place on Jussieu campus, Paris, France, on September, 25th 2019.
A few words
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.
Registration is free but mandatory.
Registration
Register HereConfirmed Speakers
Schedule
Session 1
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.
Coffee Break (30 min)
Session 2
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.
Lunch Break (1h30)
Lunch is not provided but there are many restaurants next to the universitySession 3
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.
Coffee Break (30 min)
Session 4
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.