Project VeriSiCC

Verification of Side-Channel Countermeasures

2018-2022

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, 22th 2022
    • New VeriSiCC Seminar at Sorbonne Université Campus Pierre et Marie Curie, Paris
    Save the date!

    Partners

    Related Publications & Tools



    IronMask: Versatile Verification of Masking Security.

    S&P

    Sonia Belaïd, Darius Mercadier, Matthieu Rivain, and Abdul Rahman Taleb.

    Probing Security through Input-Output Separation and Revisited Quasilinear Masking.

    TCHES

    Dahmun Goudarzi, Thomas Prest, Matthieu Rivain, and Damien Vergnaud.

    Dynamic Random Probing Expansion with Quasi Linear Asymptotic Complexity.

    Asiacrypt

    Sonia Belaïd, Matthieu Rivain, Abdul Rahman Taleb, Damien Vergnaud.

    Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification.

    TCHES

    Gilles Barthe, Marc Gourjon, Benjamin Grégoire, Maximilian Orlt, Clara Paglialonga, Lars Porth.

    Secure Wire Shuffling in the Probing Model.

    Crypto

    Jean-Sébastien Coron, Lorenzo Spignoli.

    On the Power of Expansion: More Efficient Constructions in the Random Probing Model.

    Eurocrypt

    Sonia Belaïd, Matthieu Rivain, Abdul Rahman Taleb.

    Random Probing Security: Verification, Composition, Expansion and New Constructions.

    Crypto

    Sonia Belaïd, Jean-Sébastien Coron, Emmanuel Prouff, Matthieu Rivain, Abdul Rahman Taleb.

    Side-channel Masking with Pseudo-Random Generator.

    Eurocrypt

    Jean-Sébastien Coron, Aurélien Greuet, Rina Zeitoun.

    Tornado: Automatic Generation of Probing-Secure Masked Bitsliced Implementations.

    Eurocrypt

    Sonia Belaïd, Pierre-Evariste Dagand, Darius Mercadier, Matthieu Rivain, Raphaël Wintersdorff.

    Monomial Evaluation of Polynomial Functions Protected by Threshold Implementations – With an Illustration on AES –.

    WISTP

    Simon Landry, Yanis Linge, Emmanuel Prouff.

    Lower and Upper Bounds on the Randomness Complexity of Private Computations of AND.

    TCC

    Eyal Kushilevitz, Rafail Ostrovsky, Emmanuel Prouff, Adi Rosén, Adrian Thillard, Damien Vergnaud.

    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.



    IronMask

    Automatic verification of countermeasures in the (random) probing model.

    Sonia Belaïd, Darius Mercadier, Matthieu Rivain, Abdul Rahman Taleb.

    Random Probing Compiler

    Automatic generation of countermeasures in the random probing model.

    Sonia Belaïd, Jean-Sébastien Coron, Emmanuel Prouff, Matthieu Rivain, Abdul Rahman Taleb.

    VRAPS

    Automatic verification of countermeasures in the random probing model.

    Sonia Belaïd, Jean-Sébastien Coron, Emmanuel Prouff, Matthieu Rivain, Abdul Rahman Taleb.

    scverif

    Automatic verification of countermeasures in the probing model extended with device features.

    Gilles Barthe, Marc Gourjon, Benjamin Grégoire, Maximilian Orlt, Clara Paglialonga, Lars Porth.

    tornado

    Automatic generation of countermeasures proven d-register probing secure for a generic order d from a C implementation to an Assembly code.

    Sonia Belaïd, Pierre-Evariste Dagand, Darius Mercadier, Matthieu Rivain, Raphaël Wintersdorff.

    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.

    Technical 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

    Language: english

    L2.2. Formal Methods Techniques for Verification

    Leading Partner: CryptoExperts

    Language: english

    L2.3. Types System for Countermeasures

    Leading Partner: Inria

    L4.1. Description of Developed Tests for Characterisation

    Leading Partner: Idemia

    Language: english



    L3.1. Software Tool for Countermeasures Verification

    Leading Partner: CRX

  • maskVerif  
  • checkMasks  
  • Tornado  
  • VRAPS  
  • scverif  
  • IronMask  

    • L3.2. Software Tool for Countermeasures Generation

    Leading Partner: Inria

  • Tornado  
  • Random probing compiler  

    • L3.3. Characterization Report

    Leading Partner: NinjaLab

    L4.2. Tests Report for Characterization.

    Leading Partner: Idemia

    L4.3. Evaluation Report

    Leading Partner: NinjaLab

    Events


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





  • 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