Paper 2026/809

Formal Verification, Integration and Physical Evaluation of Prime-Field Masking on Silicon

Abstract

The resistance of provably secure masked circuits to physical attacks depends in part on the underlying algebraic group and recombination function. Masking over finite fields of odd prime order has been demonstrated, both in theory and in practice, to provide increased natural resistance to side-channel and fault attacks. Its instantiation with a simple additive encoding and implementation-friendly prime modulus was suggested to lead to favorable tradeoffs between security and performance in prior works. To most efficiently leverage these advantages, a family of lightweight Tweakable Block Ciphers (TBCs) called Feistel for Prime Masking (FPM) has been introduced by Grassi et al. at Eurocrypt'24, together with a first hardware-oriented instance called small-pSquare. Yet, barriers for the use and further development of prime-field masking continue to exist and include the lack of automated verification tools compatible with arithmetic over Fp, as well as efficient methods for constant-time generation of uniformly distributed randomness over the field. In this work we tackle these barriers and present our findings from formally verifying, securely integrating and physically evaluating higher-order masked implementations of small-pSquare as an exemplary case study. Our integration includes the tape-out of an Application-Specific Integrated Circuit (ASIC) manufactured in 65 nm technology and a custom Printed Circuit Board (PCB). We demonstrate how to securely verify prime-field masked circuits with existing tools such as SILVER, MATCHI and PROLEAD and certify the glitch+transition robustness of our concrete implementations. Along the way we discover and solve a 0-issue originating from incomplete modulo reductions which is present in public source codes of masked prime-field ciphers but has never been discussed. We also introduce Privium, a Bivium-inspired primitive, to efficiently produce random values uniformly distributed over Fp without the need for rejection sampling. We then describe our efficient serialized pipelined small-pSquare architecture enabling an attractive tradeoff between area and latency and compare its pre- and post-layout implementation figures. Finally, we experimentally demonstrate the strong leakage resistance of our formally verified circuits on real silicon.