Paper 2018/562

maskVerif: automated analysis of software and hardware higher-order masked implementations

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


Power and electromagnetic based side-channel attacks are serious threats against the security of cryptographic embedded devices. In order to mitigate these attacks, implementations use countermeasures, among which masking is currently the most investigated and deployed choice. Unfortunately, commonly studied forms of masking rely on underlying assumptions that are difficult to satisfy in practice. This is due to physical defaults, such as glitches or transitions, which can recombine the masked data in a way that concretely reduces an implementation’s security. We develop and implement an automated approach for verifying security of masked implementations in presence of physical defaults (glitches or transitions). Our approach helps to recover the main strengths of masking: rigorous foundations, composability guarantees, automated verification under more realistic assumptions. Our work follows the approach of (Barthe et al, EUROCRYPT 2015) and thus contributes to demonstrate the benefits of language-based approaches (specifically probabilistic information flow) for masking.

Available format(s)
Publication info
Published elsewhere. ESORICS 2019
Side-Channel AttacksMasking CountermeasurePhysical DefaultsGlitchesAutomated verificationComposabilitymaskVerif
Contact author(s)
sonia belaid @ cryptoexperts com
2019-07-08: last of 2 revisions
2018-06-04: received
See all versions
Short URL
Creative Commons Attribution


      author = {Gilles Barthe and Sonia Belaïd and Gaëtan Cassiers and Pierre-Alain Fouque and Benjamin Grégoire and François-Xavier Standaert},
      title = {maskVerif: automated analysis of software and hardware higher-order masked implementations},
      howpublished = {Cryptology ePrint Archive, Paper 2018/562},
      year = {2018},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.