International audience

Side-channel attacks are a powerful class of attacks targeting cryptographic devices. Masking is a popular protection technique to thwart such attacks as it can be theoretically proven secure. However, correctly implementing masking schemes is a non-trivial task and error-prone. If several techniques have been proposed to formally verify masked implementations, they all come with limitations regarding expressiveness, scalability or accuracy. In this work, we propose a symbolic approach, based on a variant of the classical substitution method, for formally verifying arithmetic and boolean masked programs. This approach is more accurate and scalable than existing approaches thanks to a careful design and implementation of key heuristics, algorithms and data structures involved in the verification process. We present all the details of this approach and the open-source tool calledLeakageVerifwhich implements it as a python library, and which offers constructions for symbolic expressions and functions for their verification. We compareLeakageVerifto three existing state-of-the-art tools on a set of 46 masked programs, and we show that it has very good scalability and accuracy results while providing all the necessary constructs for describing algorithmic to assembly masking schemes. Finally, we also provide the set of 46 benchmarks, namedMaskedVerifBenchsand written for comparing the different verification tools, in the hope that they will be useful to the community for future comparisons.

Side-channel attacks are powerful attacks for retrieving secret data by exploiting physical measurements, such as power consumption or electromagnetic emissions. Masking is a popular countermeasure as it can be proven secure against an attacker model. In practice, software-masked implementations suffer from a security reduction due to a mismatch between the considered leakage sources in the security proof and the real ones, which depend on the microarchitecture. We propose ARMISTICE, a framework for formally verifying the absence of leakage in first-order masked implementations taking into account modeled microarchitectural sources of leakage. As a proof of concept, we present the modeling of an Arm Cortex-M3 core from its RTL description and leakage test vectors, as well as the modeling of the memory of an STM32F1 board, exclusively using leakage test vectors. We show that, with these models, ARMISTICE pinpoints vulnerable instructions in real-world masked implementations and helps the design of masked software implementations which are practically secure.

Side-channel attacks are amongst the major threats for embedded systems and IoT devices. Masking is one of the most used countermeasure against such attacks, but its application remains a difficult process. We propose a target-independent approach for applying a first-order Boolean masking countermeasure during compilation, on the static single assignment (SSA) form. Contrary to the state-of-the art automated approaches that require to simplify the control flow of the input program, our approach supports regular control-flow program structures. Moreover, our compiler is the first to automatically mask table lookups using a polynomial interpolation approach. We also present new optimizations to speedup the evaluation of polynomials: we reduce the number of terms of the polynomial, and we accelerate finite-field multiplication. We show that our approach is faster than the standard masked table approach with mask refresh after each access, with speedups up to ×2.4 in our experiments. Finally, using a formal verification approach, we show that the compiled machine code is secure, i.e., that all intermediate computations are statistically independent of the secrets.