[Resource Topic] 2023/732: VerifMSI: Practical Verification of Hardware and Software Masking Schemes Implementations

Welcome to the resource topic for 2023/732

VerifMSI: Practical Verification of Hardware and Software Masking Schemes Implementations

Authors: Quentin L. Meunier, Abdul Rahman Taleb


Side-Channel Attacks are powerful attacks which can recover secret information in a cryptographic device by analysing physical quantities such as power consumption. Masking is a common countermeasure to these attacks which can be applied in software and hardware, and consists in splitting the secrets in several parts. Masking schemes and their implementations are often not trivial, and require the use of automated tools to check for their correctness.
In this work, we propose a new practical tool named VerifMSI which extends an existing verification tool called LeakageVerif targeting software schemes. Compared to LeakageVerif, VerifMSI includes hardware constructs, namely gates and registers, what allows to take glitch propagation into account. Moreover, it includes a new representation of the inputs, making it possible to verify three existing security properties (Non-Interference, Strong Non-Interference, Probe Isolating Non-Interference) as well as a newly defined one called Relaxed Non-Interference, compared to the unique Threshold Probing Security verified in LeakageVerif. Finally, optimisations have been integrated in VerifMSI in order to speed up the verification.
We evaluate VerifMSI on a set of 9 benchmarks from the literature, focusing on the hardware descriptions, and show that it performs well both in terms of accuracy and scalability.

ePrint: https://eprint.iacr.org/2023/732

See all topics related to this paper.

Feel free to post resources that are related to this paper below.

Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.

For more information, see the rules for Resource Topics .