Paper 2020/603

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

Gilles Barthe, Marc Gourjon, Benjamin Gregoire, Maximilian Orlt, Clara Paglialonga, and Lars Porth


We propose a new approach for building efficient, provably secure, and practically hardened implementations of masked algorithms. Our approach is based on a Domain Specific Language in which users can write efficient assembly implementations and fine-grained leakage models. The latter are then used as a basis for formal verification, allowing for the first time formal guarantees for a broad range of device-specific leakage effects not addressed by prior work. The practical benefits of our approach are demonstrated through a case study of the PRESENT S-Box: we develop a highly optimized and provably secure masked implementation, and show through practical evaluation based on TVLA that our implementation is practically resilient. Our approach significantly narrows the gap between formal verification of masking and practical security.

Note: Adding further explanation and physical evaluation.

Available format(s)
Publication info
A minor revision of an IACR publication in TCHES 2021
Side-channel resilienceHigher-order maskingProbing securityVerificationDomain-Specific-Languages
Contact author(s)
gjbarthe @ gmail com
marc gourjon @ tuhh de
clara paglialonga @ gmail com
maximilian orlt @ crisp-da de
lars porth @ stud tu-darmstadt de
benjamin gregoire @ inria fr
2021-09-07: last of 3 revisions
2020-05-22: received
See all versions
Short URL
Creative Commons Attribution


      author = {Gilles Barthe and Marc Gourjon and Benjamin Gregoire and Maximilian Orlt and Clara Paglialonga and Lars Porth},
      title = {Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification},
      howpublished = {Cryptology ePrint Archive, Paper 2020/603},
      year = {2020},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.