  Masking is a widely-used effective countermeasure against power side-channel
attacks for implementing cryptographic algorithms. Surprisingly, few formal
verification techniques have addressed a fundamental question, i.e., whether
the masked program and the original (unmasked) cryptographic algorithm are
functional equivalent. In this paper, we study this problem for masked
arithmetic programs over Galois fields of characteristic 2. We propose an
automated approach based on term rewriting, aided by random testing and SMT
solving. The overall approach is sound, and complete under certain conditions
which do meet in practice. We implement the approach as a new tool FISCHER and
carry out extensive experiments on various benchmarks. The results confirm the
effectiveness, efficiency and scalability of our approach. Almost all the
benchmarks can be proved for the first time by the term rewriting system
solely. In particular, FISCHER detects a new flaw in a masked implementation
published in EUROCRYPT 2017.
