Tight Private Circuits: Achieving Probing Security with the Least Refreshing.

Masking is a common countermeasure to secure implementations against side-channel attacks. In 2003, Ishai, Sahai, and Wagner introduced a formal security model, named -probing model, which is now widely used to theoretically reason on the security of masked implementations. While many works have provided security proofs for small masked components, called gadgets , within this model, no formal method allowed to securely compose gadgets with a tight number of shares (namely, ) until recently. In 2016, Barthe et al. filled this gap with maskComp, a tool checking the security of masking schemes composed of several gadgets. This tool can achieve provable security with tight number of shares by inserting mask-refreshing gadgets at carefully selected locations. However the method is not tight in the sense that there exists some compositions of gadgets for which it cannot exhibit a flaw nor prove the security. As a result, it is overconservative and might insert more refresh gadgets than actually needed to ensure -probing security. In this paper, we exhibit the first tool, referred to as tightPROVE, able to clearly state whether a shared circuit composed of standard gadgets (addition, multiplication, and refresh) is -probing secure or not. Given such a composition, our tool either produces a probing-security proof (valid at any order) or exhibits a security flaw that directly implies a probing attack at a given order. Compared to maskComp, tightPROVE can drastically reduce the number of required refresh gadgets to get a probing security proof, and thus the randomness requirement for some secure shared circuits. We apply our method to a recent AES implementation secured with higher-order masking in bitslice and we show that we can save all the refresh gadgets involved in the s-box layer, which results in an significant performance gain.