论文标题
一种混合方法，用于正式验证高阶掩盖算术程序
A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs
论文作者
论文摘要
能够通过侧通道信息破坏保密的侧通道攻击，对实施加密算法构成了日益严重的威胁。通过通过随机分组消除保密和功耗之间的统计依赖性，掩盖是对侧通道攻击的有效对策。但是，设计高效有效的蒙版实现是一项容易出错的任务。当前用于验证掩盖程序是否安全的技术在适用性和准确性上受到限制，尤其是在应用它们时。为了弥合这一差距，在本文中，我们首先提出了一个配备有效类型推理算法的声音类型系统，用于验证针对高阶攻击的蒙版算术程序。然后，我们提供基于模型和模型匹配的新型方法，这些方法能够精确地确定类型系统检测到的潜在泄漏可观察的集合是真实的还是简单的。我们在算术密码图的各种实现方面评估了我们的方法。实验证实，我们的方法在适用性，准确性和效率方面执行了最新的基线。
Side-channel attacks, which are capable of breaking secrecy via side-channel information, pose a growing threat to the implementation of cryptographic algorithms. Masking is an effective countermeasure against side-channel attacks by removing the statistical dependence between secrecy and power consumption via randomization. However, designing efficient and effective masked implementations turns out to be an error-prone task. Current techniques for verifying whether masked programs are secure are limited in their applicability and accuracy, especially when they are applied. To bridge this gap, in this article, we first propose a sound type system, equipped with an efficient type inference algorithm, for verifying masked arithmetic programs against higher-order attacks. We then give novel model-counting based and pattern-matching based methods which are able to precisely determine whether the potential leaky observable sets detected by the type system are genuine or simply spurious. We evaluate our approach on various implementations of arithmetic cryptographicprograms.The experiments confirm that our approach out performs the state-of-the-art base lines in terms of applicability, accuracy and efficiency.
