maskVerif

Automatic tool for the verification of side-channel countermeasures




maskVerif is a tool that was first designed in 2015 to automatically and formally verify higher-order masking implementations. Operating on pseudo-code in SSA form, it returns either a security proof in some chosen leakage model, or a list of potential attacks.

In its latest version (available below), maskVerif is able to verify the following properties:

  • t-probing security
  • t-non-interference (t-NI)
  • t-strong non-interference (t-SNI)
in presence or in absence of glitches, or with transition without transition. It provides a small intermediate language for describing implementation but it can also take Verilog implementation as input.

Download It Here

Tool Versions



- 3 - Latest version of the tool

  • Hardware probing security, NI, SNI with/without glitches
  • Verilog implementation as a possible input
  • Software probing security, NI, SNI with/without transition
  • Practical optimizations to improve verification time

    • - 2 - Second version of the tool*

  • Verification of the non-interfering (NI) and strong non-interfering security property (SNI)

    • - 1 - First version of the tool*

  • Verification of the probing security property
  • Verification of the probing security in the presence of transitions leakage


    • *Versions are not yet backward compatible but we are working on it!
    # obs Tool Version SNI NI probing
    HW SW HW SW HW SW HW SW
    first-order verification
    Trichina AND - GF(2) 2 13 3 0.01s 0.01s 0.01s 0.01s 0.01s 0.01s
    ISW AND - GF(2) 1 13 3 0.01s 0.01s 0.01s 0.01s 0.01s 0.01s
    TI AND - GF(2) 3 21 3 0.01s 0.01s 0.01s 0.01s 0.01s 0.01s
    DOM AND - GF(2) 4 13 3 0.01s 0.01s 0.01s 0.01s 0.01s 0.01s
    DOM AND SNI - GF(2) 6 13 3 0.01s 0.01s 0.01s 0.01s 0.01s 0.01s
    PARA AND - GF(2) 6 16 3 0.01s 0.01s 0.01s 0.01s 0.01s 0.01s
    DOM Keccak S-box - GF(2)20763 0.01s 0.01s 0.01s 0.01s 0.01s 0.01s
    DOM AES S-box - GF(2)965713 0.02s 0.04s 0.02s 0.04s 0.06s 0.6s
    TI Fides-160 S-box - GF(2)1926 6573 0.2s 0.2s 0.3s 57s 0.3s 2.8s
    TI Fides-192 APNx - GF(2)12869 2813 2.3s 2.46s 2.25s infty 2.3s 3m49s
    Multiplication - GF(28)*131*** 0.01s **
    AES S-box (4) - GF(28)*631*** 0.01s **
    full AES (4) - GF(28)*17 2061*** 128s **
    second-order verification
    DOM AND - GF(2) 12 30 3 0.01s 0.01s 0.01s 0.01s 0.01s 0.01s
    DOM AND SNI - GF(2) 15 30 3 0.01s 0.01s 0.01s 0.01s 0.01s 0.01s
    PARA AND - GF(2) 15 30 3 0.01s 0.01s 0.01s 0.01s 0.01s 0.01s
    DOM Keccak S-box - GF(2)601653 0.01s 0.2s 0.07s 0.14s 0.03s 0.03s
    DOM AES S-box - GF(2)1681 2053 3s 3m9s 3s 3m9s 10.7s 15m45s
    RefreshZero2[1] *662*0.01s****
    Multiplication - GF(28)*4351*** 0.01s **
    AES S-box - GF(28)*7 1401*** 0.05s **
    AES S-box - GF(28)*1 188 1111*** 27m29s **
    AES Key Schedule - GF(28)*23 041 8661*** 340.7s **
    AES 2 rounds (4) - GF(28)*25 429 1461*** 21min35s **
    AES 4 rounds (4) - GF(28)*109 571 8061*** 11h9min29s **
    third-order verification
    DOM AND - GF(2) 20 54 3 0.01s 0.04s 0.02s 0.05s 0.02s 0.03s
    DOM AND SNI - GF(2) 24 54 3 0.04s 0.04s 0.03s 0.05s 0.03s 0.03s
    PARA AND NI - GF(2) 20 48 3 0.01s 0.01s 0.02s 0.03s 0.02s 0.02s
    PARA AND SNI - GF(2) 28 53 3 0.04s 0.05s 0.02s 0.04s 0.02s 0.02s
    DOM Keccak S-box - GF(2)1002903 0.01s 41s 3.6s 11.6s 0.49s 0.68s
    DOM AES S-box - GF(2)2962 0113 0.05s 0.05s 0.05s 0.05s 12m36s infty
    RefreshZero3[1] *5602*0.01s****
    Multiplication - GF(28)*24 8041*** 0.03s **
    AES S-box (4) - GF(28)*4 499 9501*** 3.89s **
    AES S-box (5) - GF(28)*4 499 9501*** 5.04s **
    fourth-order verification
    DOM AND - GF(2) 30 87 3 0.03s 0.34s 0.1s 0.15s 0.1s 0.1s
    PARA AND NI- GF(2) 35 75 3 0.01s 0.01s 0.15s 0.42s 0.18s 0.15s
    PARA AND SNI - GF(2) 40 85 3 0.34s 0.81s 0.17s 0.47s 0.16s 0.16s
    DOM Keccak S-box - GF(2)1504503 0.02s infty 4m 13m20 20s 41s
    RefreshZero4[1]*4 8452*0.01s****
    Multiplication - GF(28)*2 024 7851*** 1.14s **
    AES S-box - GF(28)*4 487 429 5601*** 6h8m39s **
    AES S-box (4) - GF(28)*2 277 036 6851*** 14m39s **
    fifth-order verification
    DOM Keccak S-box - GF(2)2106183 0.02s infty 1h6m infty 3m59s 14m6s
    RefreshZero5[1,2] *850 6682*0.01s****
    Multiplication - GF(28)*216 071 3941*** 45s **
    verification for orders > 5
    RefreshZero6[1,2]*13 983 8162*0.01s****
    RefreshZero10[1,2] *10122*18s****
    RefreshZero18[1,4] *7*10212*1 month****

    Publications



    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, 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

    Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model.

    Eurocrypt

    Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub

    Strong Non-Interference and Type-Directed Higher-Order Masking.

    ACM CCS

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

    Verified Proofs of Higher-Order Masking.

    Eurocrypt

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




    Related Talks



    Security of Masked Implementations.

    Invited talk at LatinCrypt conference

    Sonia Belaïd

    Tutorial: Formal Verification of Masked Implementations.

    Tutorial at CHES conference

    Sonia Belaïd and Benjamin Grégoire

    Advances in computer-aided cryptography.

    Invited talk at Eurocryot

    Gilles Barthe

    Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model.

    Paper presentation at Eurocrypt

    François-Xavier Standaert

    Verified Proofs of Higher-Order Masking.

    Paper presentation at Eurocrypt

    Sonia Belaïd



    On the road to building formally verified side-channel countermeasures.

    CrossFyre workshop (virtual)

    Sonia Belaïd

    Secure Masked Implementations with the Least Refreshing.

    Journée GT Méthodes Formelles pour la Sécurité, CNRS, Paris

    Sonia Belaïd

    Vérification d’implémentations masquées: du software au hardware.

    Journées Nationales 2018 Pré-GDR Sécurité Informatique, CNRS, Paris

    Benjamin Grégoire

    On the Security of Composed Masked Implementations with Least Refreshing.

    Séminaire CCA (Codage, Cryptologie, Algorithmes), INRIA, Paris

    Sonia Belaïd

    On the use of formal tools to improve the security of masked implementations.

    EIT Digital International Symposium, Université de Rennes 1

    Sonia Belaïd

    On the Use of Masking to Defeat Power-Analysis Attacks.

    Paris Crypto Day, ENS, Paris

    Sonia Belaïd



    Contact