屏蔽算术程序抗侧信道攻击的定量验证
Quantitative Verification of Masked Arithmetic Programs against Side-Channel Attacks
摘要：
功率侧信道攻击通过统计分析来推断秘密数据，已经成为一种严重的威胁。掩蔽是降低秘密数据与边信道信息之间统计相关性的有效对策。然而，设计掩蔽算法是一个容易出错的过程。在本文中，我们提出了一个混合的方法结合类型推断和模型计数来验证屏蔽算术程序对侧信道攻击。类型推断允许一个有效的，轻量级的过程来确定最可观察的变量，而模型计数帐户的完整性。在程序没有被完全屏蔽的情况下，我们还提供了一种方法来量化程序的安全级别。我们实现了我们的方法在一个工具QMVerif和评估它的密码基准。实验结果表明了该方法的有效性和效率。
英文摘要：
Power side-channel attacks, which can deduce secret data via statistical analysis, have become a serious threat. Masking is an effective countermeasure for reducing the statistical dependence between secret data and side-channel information. However, designing masking algorithms is an error-prone process. In this paper, we propose a hybrid approach combing type inference and model-counting to verify masked arithmetic programs against side-channel attacks. The type inference allows an efficient, lightweight procedure to determine most observable variables whereas model-counting accounts for completeness. In case that the program is not perfectly masked, we also provide a method to quantify the security level of the program. We implement our methods in a tool QMVerif and evaluate it on cryptographic benchmarks. The experimental results show the effectiveness and efficiency of our approach.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
