Paper 2022/849

Formal Verification of Arithmetic Masking in Hardware and Software

Barbara Gigerl, Graz University of Technology
Robert Primas, Graz University of Technology
Stefan Mangard, Graz University of Technology, Lamarr Security Research

Masking is a popular secret-sharing technique that is used to protect cryptographic implementations against physical attacks like differential power analysis. So far, most research in this direction has focused on finding efficient Boolean masking schemes for well-known symmetric cryptographic algorithms like AES and Keccak. However, especially with the advent of post-quantum cryptography (PQC), arithmetic masking has received increasing attention from the research community. In practice, many PQC algorithms require a combination of arithmetic and Boolean masking, which makes the search for secure and efficient conversion algorithms between these domains (A2B/B2A) an interesting but very challenging research topic. While there already exist lots of tools that can help with the formal verification of 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 [CGV14]-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.

Available format(s)
Publication info
Published elsewhere. ACNS
maskingverificationarithmetic maskingformal verificationglitchesside-channel analysiscoco
Contact author(s)
barbara gigerl @ iaik tugraz at
robert primas @ iaik tugraz at
stefan mangard @ iaik tugraz at
2023-04-21: revised
2022-06-27: received
See all versions
Short URL
Creative Commons Attribution


      author = {Barbara Gigerl and Robert Primas and Stefan Mangard},
      title = {Formal Verification of Arithmetic Masking in Hardware and Software},
      howpublished = {Cryptology ePrint Archive, Paper 2022/849},
      year = {2022},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.