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.

翻译：普遍认为Wi-Fi通信的安全性至关重要。因此，Wi-Fi联盟于2018年发布了WPA3，其独特的安全特性在于利用密码认证密钥交换（PAKE）协议来保护用户密码免受离线字典攻击。然而，在协议发布后不久，便有多起针对其实现的攻击被报道。为此，协议以尽力而为的方式进行更新。本文表明，所提出的缓解措施并不足够，尤其是对于复杂协议而言，即使经验丰富的开发者也可能难以正确实现。我们提出了**Dragondoom**，这是一系列强度各异的侧信道漏洞集合，攻击者可借此恢复广泛部署的Wi-Fi守护程序（如默认设置下的hostap）中的用户密码。我们的发现针对两种密码转换方法：默认的概率性“狩猎-啄食”方法及其新标准化的基于SSWU的确定性替代方案。我们通过微架构机制成功在实际场景中利用这些信息泄露，并克服了Flush+Reload方法空间分辨率有限的限制。与先前工作相比，我们的攻击在所需测量次数上更具优势。为终止Dragonfly实现中“打补丁-再攻击”的恶性循环，我们提出**Dragonstar**——一种利用形式化验证底层数学运算的Dragonfly实现，从而消除所有相关的信息泄露向量。我们的实现基于HACL*（一个保证密钥独立性的形式化验证加密库）。Dragonstar的设计使其集成至hostap时仅需对现有项目进行最小修改。实验表明，基于HACL*的hostap性能与基于OpenSSL的版本相当，这意味着Dragonstar既高效又经证明无信息泄露。