Short Paper: Mechanized Proofs of Masking Security

Abstract

Among the many threats that side channels pose to the security of computer systems, those that exploit physical access are among the most insidious. A general countermeasure against these attacks is masking, a form of secret sharing applied to sensitive data. While these techniques are effective and widespread, implementing them correctly typically involves complex informal reasoning, where even subtle mistakes can invalidate the security guarantees they potentially offer. We present our vision and initial work to provide rigorous formal assurances and sound reasoning principles for circuit designers by developing a mechanization framework for masked circuits that can be used to reason about the security of gadgets and their composition. Our work is done on top of the EasyCrypt proof assistant.