Cryptology ePrint Archive: Report 2020/603

Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification

Gilles Barthe and Marc Gourjon and Benjamin Gregoire and Maximilian Orlt and Clara Paglialonga and Lars Porth

Abstract: We propose a new approach for building efficient, provably secure, and practically hardened assembly implementations of masked algorithms. Our approach is based on a Domain Specific Language in which users can write efficient assembly implementations and fine-grained leakage models. The latter are then used as a basis for formal verification, allowing for the first time formal guarantees for a broad range of leakage effects not addressed by prior work. The practical benefits of our approach are demonstrated through a case study of the PRESENT S-Box: we develop a highly optimized and provably secure masked implementation, and show through practical evaluation based on TVLA that our implementation is practically resilient. Our approach significantly narrows the gap between formal verification of masking and practical security.

Category / Keywords: Side-channel resilience, Higher-order masking, Probing security, Verification, Domain-Specific-Languages

Date: received 21 May 2020, last revised 8 Jun 2020

Contact author: gjbarthe at gmail com,marc gourjon@tuhh de,clara paglialonga@gmail com,maximilian orlt@crisp-da de,lars porth@stud tu-darmstadt de,benjamin gregoire@inria fr

Available format(s): PDF | BibTeX Citation

Version: 20200608:165706 (All versions of this report)

Short URL: ia.cr/2020/603


[ Cryptology ePrint archive ]