从 Dragondoom 到 Dragonstar：WPA3 Dragonfly 握手的侧信道攻击与经过形式化验证的实现
From Dragondoom to Dragonstar: Side-channel Attacks and Formally Verified Implementation of WPA3 Dragonfly Handshake
AI总结：
针对 WPA3 Dragonfly 握手实现，论文提出 Dragondoom 侧信道攻击恢复密码，并给出基于 HACL* 形式化验证的 Dragonstar 实现，以低改动和相当性能消除泄漏。
摘要：
众所周知，保障 Wi-Fi 通信安全非常重要。因此，Wi-Fi 联盟于 2018 年发布了 WPA3，并带来一项独特的安全特性：它利用密码认证密钥交换（PAKE）协议保护用户密码，使其免受离线字典攻击。遗憾的是，该协议发布后不久，就有若干针对其实现的攻击被披露；作为回应，协议以尽力而为的方式进行了更新。本文表明，所提出的缓解措施并不充分，尤其是对于这样一种即使经验丰富的开发者也难以实现的复杂协议而言。事实上，我们提出了 Dragondoom，这是一组强度各异的侧信道漏洞，使攻击者能够在广泛部署的 Wi-Fi 守护进程中恢复用户密码，例如在默认设置下的 hostap。我们的发现同时针对两种密码转换方法，即默认的概率式 hunting-and-pecking，以及其新近标准化的、基于 SSWU 的确定性替代方案。我们在实践中通过微架构机制成功利用了这些泄漏，并克服了 Flush+Reload 空间分辨率有限的问题。就所需测量次数而言，我们的攻击优于以往工作。随后，出于终结 Dragonfly 实现中“打补丁式应急修复”循环的需要，我们提出 Dragonstar，这是一种 Dragonfly 实现，利用经过形式化验证的底层数学运算实现，从而消除所有相关泄漏向量。我们的实现依赖 HACL*，这是一个经过形式化验证、可保证秘密独立性的密码库。我们对 Dragonstar 进行设计，使其集成到 hostap 时只需对现有项目进行最小修改。实验表明，基于 HACL* 的 hostap 在性能上可与基于 OpenSSL 的实现相比，这意味着 Dragonstar 既高效，又被证明无泄漏。
英文摘要：
It is universally acknowledged that Wi-Fi communications are important to secure. Thus, the Wi-Fi Alliance published WPA3 in 2018 with a distinctive security feature: it leverages a Password-Authenticated Key Exchange (PAKE) protocol to protect users' passwords from offline dictionary attacks. Unfortunately, soon after its release, several attacks were reported against its implementations, in response to which the protocol was updated in a best-effort manner. In this paper, we show that the proposed mitigations are not enough, especially for a complex protocol to implement even for savvy developers. Indeed, we present **Dragondoom**, a collection of side-channel vulnerabilities of varying strength allowing attackers to recover users' passwords in widely deployed Wi-Fi daemons, such as hostap in its default settings. Our findings target both password conversion methods, namely the default probabilistic hunting-and-pecking and its newly standardized deterministic alternative based on SSWU. We successfully exploit our leakage in practice through microarchitectural mechanisms, and overcome the limited spatial resolution of Flush+Reload. Our attacks outperform previous works in terms of required measurements. Then, driven by the need to end the spiral of patch-and-hack in Dragonfly implementations, we propose **Dragonstar**, an implementation of Dragonfly leveraging a formally verified implementation of the underlying mathematical operations, thereby removing all the related leakage vector. Our implementation relies on HACL*, a formally verified crypto library guaranteeing secret-independence. We design Dragonstar, so that its integration within hostap requires minimal modifications to the existing project. Our experiments show that the performance of HACL*-based hostap is comparable to OpenSSL-based, implying that Dragonstar is both efficient and proved to be leakage-free.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
