University of Surrey

Test tubes in the lab Research in the ATI Dance Research

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

Barthe, G, Belaïd, S, Dupressoir, FSP, Fouque, P-A, Grégoire, B, Strub, P-Y and Zucchini, R (2016) Strong Non-Interference and Type-Directed Higher-Order Masking In: 2016 23rd ACM Conference on Computer and Communications Security, 2016-10-24 - 2016-10-28, Hofburg Palace, Vienna, Austria.

Full text not available from this repository.


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.

Item Type: Conference or Workshop Item (Conference Paper)
Subjects : Computing
Divisions : Surrey research (other units)
Authors :
Barthe, G
Belaïd, S
Fouque, P-A
Grégoire, B
Strub, P-Y
Zucchini, R
Date : 24 October 2016
Funders : Office of Naval Research
DOI : 10.1145/2976749.2978427
Copyright Disclaimer : © 2016 Copyright held by the owner/author(s). Publication rights licensed to ACM.
Contributors :
Uncontrolled Keywords : Security and privacy, Formal methods and theory of security, Logic and verification, Formal security models, Security in hardware, Hardware attacks and countermeasures, Side-channel analysis and countermeasures, Embedded systems security
Depositing User : Symplectic Elements
Date Deposited : 17 May 2017 13:58
Last Modified : 23 Jan 2020 19:00

Actions (login required)

View Item View Item


Downloads per month over past year

Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800