(A) study on systematic security analysis of cellular network control plane procedures

Abstract

The control plane procedures of cellular networks play a critical role in tasks such as network registration, tracking the location of user devices, and data session management, providing fast and reliable data communication, as well as voice-centric services. In the standards of cellular network technology, the control plane provides functions of mutual authentication and key agreement procedure to ensure the confidentiality and integrity of wireless communication between devices and the network. In particular, long-term evolution (LTE), is widely deployed by commercial mobile network operators to provide significantly improved security features as compared to earlier networks (e.g., the use of stronger encryption and integrity protection algorithms, the mandatory use of integrity protection in control plane procedures). However, despite these efforts to improve security and privacy, previous studies have manually uncovered vulnerabilities in control plane procedures. These vulnerabilities could be exploited by an active adversary to perform user impersonations, location tracking, and denial of service attack. As cellular networks are widely used for numerous safety-critical applications such as nation-wide emergency notification, autonomous vehicles, and railway communication, users could face a significant threat to their safety if adversaries exploit the existing vulnerabilities to disrupt the confidentiality, integrity protection, or availability of the network system. Therefore, it is crucial to identify potential security and privacy threats in both specifications and actual implementations of network components to prevent such threats in advance. In this dissertation, we present a systematic approach to analyzing both the protocol specifications and its implementations of commercial network components. First, we analyzed the standard control plane procedures by formally specifying the protocol models and verifying their secrecy and authentication properties under a reasonable adversary model. Given the attack traces from the formal verification process, we empirically evaluated their validity and potential security implications in our own practical testing framework. Second, we present a dynamic security testing methodology to effectively inspect bad practices of implementations and configurations of commercial network components. To this end, we implemented a semi-automatic testing framework with a simple decision tree logic to classify problematic cases based on open-source LTE baseband and control traffic monitoring tools. We also demonstrate all of the resultant attacks by exploiting the vulnerabilities we found in the operational networks while strictly following ethics requirements.