Quantitative Verification of Masked Arithmetic Programs Against Side-Channel Attacks

DOI10.1007/978-3-030-17462-0_9zbMATH Open1527.68129arXiv1901.09706OpenAlexW2912873165MaRDI QIDQ6091332

Author name not available (Why is that?)

Publication date: 24 November 2023

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Abstract: Power side-channel attacks, which can deduce secret data via statistical analysis, have become a serious threat. Masking is an effective countermeasure for reducing the statistical dependence between secret data and side-channel information. However, designing masking algorithms is an error-prone process. In this paper, we propose a hybrid approach combing type inference and model-counting to verify masked arithmetic programs against side-channel attacks. The type inference allows an efficient, lightweight procedure to determine most observable variables whereas model-counting accounts for completeness. In case that the program is not perfectly masked, we also provide a method to quantify the security level of the program. We implement our methods in a tool QMVerif and evaluate it on cryptographic benchmarks. The experimental results show the effectiveness and efficiency of our approach.

Full work available at URL: https://arxiv.org/abs/1901.09706

Mathematics Subject Classification ID

Cryptography (94A60) Data encryption (aspects in computer science) (68P25) Specification and verification (program logics, model checking, etc.) (68Q60)