高阶屏蔽算术程序的混合形式化验证
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
