Motivation
Side-channel attacks represent a major threat for embedded systems deployed in critical environments, including payment infrastructures and IoT platforms. Because these attacks rely on physical observations rather than algorithmic weaknesses, even cryptographically strong algorithms can become vulnerable when implemented on real hardware.
Masking is the most widely used countermeasures to protect implementations against such attacks. The principle is to split sensitive values into multiple random shares so that individual leakages do not reveal information about the secret. However, designing secure masked implementations is extremely challenging in practice. Small implementation mistakes or subtle interactions between components can introduce exploitable leakages and invalidate the intended security guarantees.
Previous work by the project partners has established strong foundations for the formal verification of masking countermeasures and the secure composition of masked gadgets. Their contributions include the development of EasyCrypt, a framework for formal cryptographic proofs, and Jasmin, a programming language designed for writing high-assurance and verifiable cryptographic implementations. They have also developed maskVerif, an automated verification tool for masked circuits, and introduced the Probe-Isolating Non-Interference (PINI) security notion, which has become a reference model for the secure composition of masked implementations.
Building on these advances, FORMASK aims to push the state of the art further by developing new methods for the functional verification of masked implementations, improving the automated verification of masking security properties, and enabling machine-checked security proofs for masked gadgets and cryptographic primitives.
Objectives
The FORMASK project is structured around three main scientific objectives:
- Functional verification of masked implementations: Develop techniques to formally verify the functional correctness of masked implementations. The project will first rely on equivalence proofs for small circuits, and then extend these approaches to entire implementations of cryptographic primitives through compositional verification techniques.
- Automated verification of masking security properties: Improve automated verification techniques for masked implementations by extending existing tools, in particular maskVerif, to enable efficient and scalable verification of the Probe-Isolating Non-Interference (PINI) property, a key notion for ensuring the security of large masked circuits.
- Formal security proofs for masked constructions: Develop new formal security proofs using EasyCrypt for core masked gadgets. These proofs will then be used to establish the security of larger constructions through composition, ultimately enabling the formal verification of entire cryptographic primitives.
