Paper 2015/506

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

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

Abstract

Differential power analysis (DPA) is a side-channel attack in which an adversary retrieves cryptographic material by measuring and analyzing the power consumption of the device on which the cryptographic algorithm under attack executes. An effective countermeasure against DPA is to mask secrets by probabilistically encoding them over a set of shares, and to run masked algorithms that compute on these encodings. Masked algorithms are often expected to provide, at least, a certain level of probing security. Leveraging the deep connections between probabilistic information flow and probing security, we develop a precise, scalable, and fully automated methodology to verify the probing security of masked algorithms, and generate them from unprotected descriptions of the algorithm. Our methodology relies on several contributions of independent interest, including a stronger notion of probing security that supports compositional reasoning, and a type system for enforcing an expressive class of probing policies. Finally, we validate our methodology on examples that go significantly beyond the state-of-the-art.

Note: Extended version of the published article after major rewriting.

Metadata
Available format(s)
PDF
Publication info
Published elsewhere. Major revision. Proceedings of the 23rd ACM Conference on Computer and Communications Security
Keywords
secret-key cryptographymaskingcompositionformal methodscompilertype system
Contact author(s)
masking @ projects easycrypt info
History
2016-10-25: revised
2015-05-27: received
See all versions
Short URL
https://ia.cr/2015/506
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2015/506,
      author = {Gilles Barthe and Sonia Belaïd and François Dupressoir and Pierre-Alain Fouque and Benjamin Grégoire and Pierre-Yves Strub and Rébecca Zucchini},
      title = {Strong Non-Interference and Type-Directed Higher-Order Masking},
      howpublished = {Cryptology ePrint Archive, Paper 2015/506},
      year = {2015},
      note = {\url{https://eprint.iacr.org/2015/506}},
      url = {https://eprint.iacr.org/2015/506}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.