Project VeriSiCC

Verification of Side-Channel Countermeasures

2018-2021

FUI project funded by


About

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. Namely, the following tools are to be developed:

  • 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.

News!


  • September, 25th 2019
  • VeriSiCC Seminar at Sorbonne Université Campus Pierre et Marie Curie, Paris
    Visit and register for free!

    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


  • September, 25th 2019
  • VeriSiCC Seminar at Sorbonne Université Campus Pierre et Marie Curie, Paris
    Visit and register for free!

    Contact

    Project Coordinator

    CryptoExperts

    41 boulevard des Capucines

    75002 Paris

    France