面向常数时间密码实现的高效验证

时序侧信道攻击利用依赖于秘密的执行时间完全或部分恢复密码实现的秘密，对软件安全构成严重威胁。常数时间编程规范是一种有效的基于软件的对抗时序侧信道攻击的措施，但开发常数时间实现被证明具有挑战性且容易出错。当前的验证方法/工具在实际应用于生产软件时存在可扩展性和精度问题。在本文中，我们提出了一种基于污点分析与自组合程序安全性验证新颖协同的实用验证方法。具体来说，我们首先使用基于IFDS的轻量级污点分析来证明大量潜在的（时序）侧信道源实际上不会泄露秘密。然后，我们采用精确的污点分析和安全性验证方法来确定剩余潜在侧信道源是否真的能泄露秘密。这些方法包括原始程序及其布尔抽象的污点导向半叉积的新颖构造，以及程序的污点导向自组合。我们的方法实现为一个跨平台的完全自动化工具CT-Prover。实验证实了其在验证现代密码库和SSL/TLS库中的实际基准测试时的效率和有效性。特别是，CT-Prover发现了开源SSL库（如Mbed SSL、BearSSL）中新的、已确认的漏洞，并显著优于现有最先进工具。