Paper 2018/562

maskVerif: automated analysis of software and hardware higher-order masked implementations

Gilles Barthe and Sonia Belaïd and Pierre-Alain Fouque and Benjamin Grégoire

Abstract

Masking is a popular countermeasure for protecting both hardware and software implementations against differential power analysis. A main strength of software masking is that its security guarantees can be captured rigorously through formal models, such as the Threshold Probing Model (Ishai, Sahai, Wagner, CRYPTO 2003) and proved automatically using formal verification tools based on Fourier coefficients (Eldib, Wang and Schaumont, ACM TOSSEM 2014) or information flow analyses (Barthe et al., EUROCRYPT 2015). In 2018, Bloem et al. (EUROCRYPT 2018) and Faust et al. (CHES 2018) introduce two security models, respectively called Threshold Probing Model with Glitches, and Robust Threshold Probing Model, to formalize the security of masked hardware implementations. Moreover, Bloem et al. provide an automated tool for proving security in the Threshold Probing Model with Glitches. However, their method is based on the computations of Fourier coefficients, and thus computationally expensive and limited to low orders. In this paper, we develop new information flow-based techniques for proving security of hardware implementations in the models of (Bloem et al., EUROCRYPT 2018) and (Faust et al., CHES 2018). Our techniques improve over the algorithms of (Barthe et al., EUROCRYPT 2015) in terms of coverage and efficiency, allowing for verification at higher orders and minimizing the possibility of false negatives. We implement our methods in an extension of the maskVerif tool (Barthe et al. , EUROCRYPT 2015) that supports efficient verification of both software and hardware implementations. Our tool is able to analyze examples from the literature, including (Bloem et al., EUROCRYPT 2018), much faster and at higher orders, as well as implementations that follow Generalized Masking Scheme (Reparaz et al., CRYPTO 2015) and Domain Oriented Masking (Gross, Mangard, Korak, CHES 2017).