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
    Check out the slides!

    Partners

    Related Communications & Tools



    The Last Mile: High-Assurance and High-Speed Cryptographic Implementations.

    Security and Privacy

    José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub.

    Machine-checked proofs for cryptographic standards: Indifferentiability of Sponge and secure high-assurance implementations of SHA-3.

    CCS

    José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub.

    maskVerif: Automated Verification of Higher-Order Masking in Presence of Physical Defaults.

    ESORICS

    Gilles Barthe, Sonia Belaïd, Gaëtan Cassiers, Pierre-Alain Fouque, Benjamin Grégoire, and François-Xavier Standaert.

    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.



    Formal Verification of Masked Implementation.

    Silm School INRIA, July 2019

    Benjamin Grégoire.

    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.


    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.

    Deliverables



    L1.1. State-of-the-Art of Formal Verification Techniques

    Leading Partner: University of Luxembourg

    Language: english

    L1.2. Definition of Needs

    Leading Partner: Idemia

    Language: french



    L2.1. Evaluation of Existing Methods

    Leading Partner: University of Luxembourg

    L2.2. Formal Methods Techniques for Verification.

    Leading Partner: CryptoExperts

    L2.3. Types System for Countermeasures

    Leading Partner: Inria

    L4.1. Description of Developed Tests for Characterisation

    Leading Partner: Idemia

    L0.1.1. Midterm Activity Report

    Leading Partner: CryptoExperts



    L3.3. Characterization Report

    Leading Partner: NinjaLab

    L4.3. Evaluation Report

    Leading Partner: NinjaLab

    L3.1. Software Tool for Countermeasures Verification

    Leading Partner: CRX

    L3.2. Software Tool for Countermeasures Generation

    Leading Partner: Inria

    L4.2. Tests Report for Characterization.

    Leading Partner: Idemia

    L0.1.2. Final Activity Report

    Leading Partner: CRX

    L0.2.1. Report on Dissemination Actions

    Leading Partner: ANSSI

    L0.2.2. Report on Standardization Actions (CC and ISO)

    Leading Partner: ANSSI

    Events


  • September, 25th 2019
  • VeriSiCC Seminar at Sorbonne Université Campus Pierre et Marie Curie, Paris
    Check out the slides!

    Contact

    Project Coordinator

    CryptoExperts

    41 boulevard des Capucines

    75002 Paris

    France