从龙之厄运到龙之星：侧信道攻击与WPA3 Dragonfly握手的形式验证实现
摘要：Wi-Fi通信的安全性是普遍认可的。因此，Wi-Fi联盟在2018年发布了WPA3，具有独特的安全功能：它利用密码认证密钥交换（PAKE）协议来保护用户的密码免受离线字典攻击。然而，发布后不久，就有多个攻击报告针对其实现，为此，该协议以尽力而为的方式进行了更新。 在本文中，我们展示了所提出的缓解措施是不够的，特别是对于即使对于精通开发的开发人员来说，实施起来也很复杂的协议。事实上，我们提出了Dragondoom，这是一个收集各种强度的侧信道漏洞，允许攻击者在广泛部署的Wi-Fi守护程序（如默认设置下的hostap）中恢复用户的密码。我们的发现针对密码转换方法，即默认的概率寻找和捕捉方法以及基于SSWU的新标准确定性替代方法。我们成功地利用了我们的泄露实践中的微架构机制，并克服了Flush+Reload的有限空间分辨率。就所需的测量次数而言，我们的攻击优于以前的研究。 然后，出于结束Dragonfly实现中的补丁和黑客的需求，我们提出了Dragonstar，它是Dragonfly的实现，利用底层数学操作的形式化验证实现，从而消除所有相关的泄漏向量。我们的实现依赖于HACL*，这是一个保证秘密独立性的形式验证的加密库。我们设计了Dragonstar，以便将其集成到hostap中，对现有项目的修改最小。我们的实验结果表明，基于HACL*的hostap的性能与基于OpenSSL的相当，这意味着Dragonstar既高效又经过泄漏测试。
作者：Daniel De Almeida Braga, Natalia Kulatova, Mohamed Sabt, Pierre-Alain Fouque, Karthikeyan Bhargavan
论文ID：2307.09243
分类：Cryptography and Security
分类简称：cs.CR
提交时间：2023-07-19