基于分段的WiFi分片与省电模式形式化验证

IEEE 802.11系列标准，更为人熟知的名字是WiFi，是一个被数十亿用户广泛使用的协议。以往关于WiFi形式化验证的工作大多集中在四次握手和其他安全方面。然而，近期研究发现了WiFi功能方面的严重漏洞，这些漏洞可能导致数十亿设备的信息泄露。目前尚不存在能够对WiFi协议功能方面进行推理的形式化分析方法。在本文中，我们率先着手填补这一空白，并对WiFi协议的功能方面，更具体地说，是分片和省电模式过程，进行了广泛的形式化分析。为实现这一目标，我们设计了一种新颖的基于分段的形式化验证流程，并在Tamarin中引入了一个实用的威胁模型（即MAC欺骗），以推理攻击者的各种能力。最终，我们验证了从WiFi协议规范中提取的68个属性，从验证中发现了3个漏洞，验证了3个已知攻击，并发现了2个新问题。这些漏洞和问题影响了17个测试案例中的14个商用设备，显示了这些问题的普遍性和影响。除此之外，我们还表明所提出的对策确实足以解决这些问题。我们希望我们的结果和分析能帮助供应商采纳这些对策，并激励对WiFi协议功能方面验证的进一步研究。