Paper Info
Title
Maskverif: Automated Verification Of Higher-Order Masking In Presence Of Physical Defaults
Abstract
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.
Year
DOI
Venue
2019
10.1007/978-3-030-29959-0_15
COMPUTER SECURITY - ESORICS 2019, PT I
Keywords
DocType
Volume
Side-channel attacks, Masking countermeasure, Physical defaults, Glitches, Automated verification, Composability, maskVerif
Conference
11735
ISSN
Citations 
PageRank 
0302-9743
3
0.39
References 
Authors
0
6
Name
Order
Citations
PageRank
Gilles Barthe12337152.36
Sonia Belaïd2916.59
Gaëtan Cassiers362.14
Pierre-Alain Fouque41762107.22
Benjamin Grégoire581748.93
François-Xavier Standaert63070193.51