Formal Verification of Arithmetic Masking in Hardware and Software

Barbara Gigerl*, Robert Primas, Stefan Mangard

*Korrespondierende/r Autor/-in für diese Arbeit

Publikation: Beitrag in Buch/Bericht/KonferenzbandBeitrag in einem KonferenzbandBegutachtung

Abstract

Masking is a popular countermeasure to protect cryptographic implementations against physical attacks like differential power analysis. So far, research focused on Boolean masking for symmetric algorithms like AES and Keccak. With the advent of post-quantum cryptography (PQC), arithmetic masking has received increasing attention because many PQC algorithms require a combination of arithmetic and Boolean masking and respective conversion algorithms (A2B/B2A), which represent an interesting but very challenging research topic. While there already exist formal verification concepts for Boolean masked implementations, the same cannot be said about arithmetic masking and accompanying mask conversion algorithms.

In this work, we demonstrate the first formal verification approach for (any-order) Boolean and arithmetic masking which can be applied to both hardware and software, while considering side-effects such as glitches and transitions. First, we show how a formal verification approach for Boolean masking can be used in the context of arithmetic masking such that we can verify A2B/B2A conversions for arbitrary masking orders. We investigate various conversion algorithms in hardware and software, and point out several new findings such as glitch-based issues for straightforward implementations of Coron et al.-A2B in hardware, transition-based leakage in Goubin-A2B in software, and more general implementation pitfalls when utilizing common optimization techniques in PQC. We provide the first formal analysis of table-based A2Bs from a probing security perspective and point out that they might not be easy to implement securely on processors that use of memory buffers or caches.
Originalspracheenglisch
TitelApplied Cryptography and Network Security
Untertitel21st International Conference, ACNS 2023, Kyoto, Japan, June 19–22, 2023, Proceedings, Part I
Redakteure/-innen M. Tibouchi, X. Wang
ErscheinungsortCham
Herausgeber (Verlag)Springer
Seiten3-32
Seitenumfang30
ISBN (elektronisch)978-3-031-33488-7
ISBN (Print)978-3-031-33487-0
DOIs
PublikationsstatusVeröffentlicht - 29 Mai 2023
Veranstaltung21st International Conference on Applied Cryptography and Network Security: ACNS 2023 - Kyoto, Japan
Dauer: 19 Juni 202322 Juni 2023

Publikationsreihe

NameLecture Notes in Computer Science
Band13905

Konferenz

Konferenz21st International Conference on Applied Cryptography and Network Security
KurztitelACNS 2023
Land/GebietJapan
OrtKyoto
Zeitraum19/06/2322/06/23

Fingerprint

Untersuchen Sie die Forschungsthemen von „Formal Verification of Arithmetic Masking in Hardware and Software“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren