Quantitative Verification of Masked Arithmetic Programs Against Side-Channel Attacks

DOI10.1007/978-3-030-17462-0_9MaRDI QIDQ6091332zbMATH OpenOpenAlexFDO

Authors

Publication date 24 November 2023

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

Copyright license Creative Commons Attribution 4.0 International

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

Mathematics Subject Classification ID

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

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.

Recommendations

• \textsc{SCInfer}: refinement-based verification of software countermeasures against side-channel attacks
• Automated verification of correctness for masked arithmetic programs
• Synthesis of masking countermeasures against side channel attacks
• Formal verification of side-channel countermeasures via elementary circuit transformations
• Security evaluation against side-channel analysis at compilation time

Cited in

(6)

• Masking proofs are tight and how to exploit it in security evaluations
• On the computational soundness of cryptographically masked flows
• Masking against Side-Channel Attacks: A Formal Security Proof
• scientific article; zbMATH DE number 7378548 (Why is no real title available?)
• Formal verification of arithmetic masking in hardware and software
• Automated verification of correctness for masked arithmetic programs

This page was built for publication: Quantitative Verification of Masked Arithmetic Programs Against Side-Channel Attacks

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6091332)