Project VeriSiCC

Verification of Side-Channel Countermeasures

2018-2021

FUI project funded by


Motivation

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 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,
  • certification bodies (represented in the consortium by ANSSI) to quickly and accurately verify implementations submitted to evaluations.

Main Objectives

The VERISICC project involves the development of the following tools:

  • Characterization method: a systematic method for characterizing the components (e.g., smart card) to determine a concrete leakage model.

  • Verification tool: an embedded code verification tool with countermeasures, implemented at the assembly level, based on a dedicated leakage model (from the characterization method), bringing security guarantees, less conservative than the existing tools and with competitive performances.

  • Generation tool: a code generation tool (assembly) with countermeasures also based on a dedicated leakage model and achieving a high security level and competitive performances.

Partners

Related Communications



Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations.

Journal of Cryptographic Engineering

Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub.

How to Securely Compute with Noisy Leakage in Quasilinear Complexity.

Asiacrypt

Dahmun Goudarzi, Antoine Joux, and Matthieu Rivain.

Tight Private Circuits: Achieving Probing Security with the Least Refreshing.

Asiacrypt

Sonia Belaïd, Dahmun Goudarzi, and Matthieu Rivain.



Secure Computation in the Presence of Noisy Leakage.

Invited talk at Journées C2, October 2018

Matthieu Rivain.

Tutorial: Formal Verification of Masked Implementations.

Tutorial at CHES conference, September 2018

Sonia Belaïd and Benjamin Grégoire.

Formal Verification of Side-Channel Countermeasures.

Cybersecurity school at Sophia Antipolis, June 2018

Sonia Belaïd.


Tools



tightPROVE

Automatic verification of d-probing security for a generic order d from a representation of a code based on standard operations.

Sonia Belaïd, Dahmun Goudarzi, Matthieu Rivain.

checkMasks

Automatic verification of d-probing security, d-non-interference, and d-strong non-interference for a specific order d from a pseudo-code.

Jean-Sébastien Coron.

maskComp

Automatic generation of countermeasures proven d-non-interferent for a generic order d from a C implementation.

Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub.

maskVerif

Automatic verification of d-probing security, d-non-interference, and d-strong non-interference for a specific order d with or without physical defaults (software transitions or glitches) from a Verilog implementation or a pseudo-code.

Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub.



Events

TBA.

Contact

Project Coordinator

CryptoExperts

41 boulevard des Capucines

75002 Paris

France