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.

翻译：掩码是一种广泛使用的针对功率侧信道攻击的有效对策，用于实现密码算法。令人惊讶的是，很少有形式化验证技术解决一个基本问题，即掩码程序与原始（未掩码）密码算法是否功能等价。本文研究了特征为2的伽罗瓦域上掩码算术程序的该问题。我们提出了一种基于项重写的自动化方法，并辅以随机测试和SMT求解。整体方法是可靠的，并且在实践中满足的特定条件下是完备的。我们将该方法实现为一个新工具FISCHER，并在各种基准测试上进行了广泛实验。结果证实了该方法的高效性、有效性和可扩展性。几乎所有基准测试首次通过项重写系统即可完成证明。特别地，FISCHER检测到EUROCRYPT 2017中发表的一个掩码实现中的新缺陷。