Masking in fine-grained leakage models: construction, implementation and verification

We propose a new approach for building efficient, provably secure, and practically hardened 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 device-specific 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.

Schlagworte

Domain specific language

Higher-order masking

Probing security

Side-channel resilience

Verification

DDC Class

004: Informatik

530: Physik

600: Technik

Funding Organisations

Bundesministerium für Bildung und Forschung (BMBF)

More Funding Information

Clara Paglialonga and Maximilian Orlt are partially funded by the VeriSec project 16KIS0634 from the Federal Ministry of Education and Research (BMBF) and the Hessen State Ministry for Higher Education, Research and the Arts within their joint support of the National Research Center for Applied Cybersecurity ATHENE, and by the Emmy Noether Program FA 1320/1-1. Marc Gourjon is partially funded by the VeriSec project 16KIS0601K from BMBF.

Publication version

publishedVersion

Lizenz

https://creativecommons.org/licenses/by/4.0/

Name

TCHES2021_2_07.pdf

Size

1.69 MB

Format

Adobe PDF

Options

Masking in fine-grained leakage models: construction, implementation and verification