VWAnalyzer: A Systematic Security Analysis Framework for the Voice over WiFi Protocol.

In this paper, we evaluate the security of the Voice over WiFi (VoWiFi) protocol by proposing the VWANALYZER framework. We model five critical procedures of the VoWiFi protocol and deploy a model-based testing approach to uncover potential design flaws. Since the standards of the VoWiFi protocol contain underspecifications that can lead to vulnerable scenarios, VWANALYZER explicitly deals with them. Unlike prior approaches that do not consider the underspecifications, VWANALYZER adopts a systematic approach that constructs diverse and viable scenarios based on the underspecifications and substantially reduces the number of possible scenarios. Then the scenarios are verified against security properties. VWANALYZER automatically generates 960 viable scenarios to be analyzed among 10,368 scenarios (91% decrease) from the initial models. We demonstrate the effectiveness of VWANALYZER by verifying 38 properties and uncovering 3 new attacks. Notable among our findings is the denial-of-cellular-connectivity attack, due to insecure handover that disconnects the user through both VoWiFi and VoLTE. To ensure that the exposed attacks pose real threats and are indeed realizable in practice, we have validated the attacks in a real-world testbed. We also report several implementations issues that were uncovered during the testbed evaluation.