掩码算术程序正确性的自动验证
Automated Verification of Correctness for Masked Arithmetic Programs
AI总结：
本文针对特征为2的伽罗瓦域上掩码算术程序与原始密码算法的功能等价性问题，提出基于项重写并辅以随机测试和SMT求解的自动验证方法，实现为工具FISCHER，实验证明其有效、高效且可扩展，并发现EUROCRYPT 2017掩码实现中的新缺陷。
摘要：
掩码是一种广泛使用的有效对策，用于在实现密码算法时抵御功耗侧信道攻击。令人惊讶的是，很少有形式化验证技术解决一个基本问题，即掩码程序与原始（未掩码）密码算法是否功能等价。本文研究特征为2的伽罗瓦域上掩码算术程序的这一问题。我们提出一种基于项重写的自动化方法，并辅以随机测试和SMT求解。整体方法是可靠的，并且在实践中确实满足的某些条件下是完备的。我们将该方法实现为新工具FISCHER，并在各种基准上进行了大量实验。结果证实了我们方法的有效性、效率和可扩展性。几乎所有基准都可以首次仅由项重写系统证明。特别是，FISCHER在EUROCRYPT 2017发表的一个掩码实现中检测到一个新缺陷。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
