Applying automated reasoning to analyze and protect cellular network protocols
Creators: name: Echeverria, Mitziu
Publisher: name: University of Iowa
Year: 2023
Subjects: 5G
Automated Reasoning
Cellular Networks
Mobile Security
Security and Privacy

description: Cellular networks have become a critical part of our infrastructure, and our dependence on them has grown as our society has become more interconnected. Due to the 5G technology, cellular networks have and will become an even more integral part of our everyday life. Because of 5G’s speed, low latency, and broad coverage, novel Internet-of-Things (IoT) safety-critical applications are emerging. For instance, New York City now relies on cellular networks to coordinate its highly complex transit system of 14,000 interconnected signalized intersections. This dependence on cellular networks comes with a significant risk, as an adversary with the required capabilities could essentially shut down New York City. To make matters worse, critical infrastructures like cellular networks have become a common target for attackers during national or international conflicts. Therefore, it is clear that cellular networks must provide various security and privacy guarantees to play such an essential role in our society. Unfortunately, as this thesis will show cellular networks have often failed to meet the expected security and privacy requirements, and improving their security posture is paramount.
description: In order to improve the unsatisfactory security and privacy status quo of the cellular network ecosystem, the community has focused mainly on identifying vulnerabilities in the hope that their proposed changes make it into the next version of the 3GPP standard specification, which guides virtually all commercial implementations. To discover vulnerabilities, the community has leveraged both manual and systematic approaches. However, due to the complexity of the system, both types of analyses often fail to scale, resulting in a focused or unsound analysis. Finding vulnerabilities is only half the story, and developing defenses is critical. Nevertheless, the majority of the community has ignored this second half of the story. Unfortunately, the proposed defenses have at least one of the critical limitations: Failing to support backward compatibility; Require expensive and specialized equipment; Fail to generalize to other attacks or variants. To make matters worse, the community has vastly focused on the main protocol stack (e.g., 5G) while leaving subprotocols integral to the ecosystem’s security yet to be explored. The eSIM protocol is one such critical subprotocol, which digitalizes physical SIM cards and allows for over-the-air provisioning. eSIM provisioning protocols are highly critical, as the primary critical assumption main protocol stack protocols make is that the credentials inside of the SIM card are secure. If at any point this assumption were to fail, all the existing security and privacy guarantees would become non-existent.
description: In this dissertation, we show how to overcome the challenges that have severely impaired previous work for both vulnerability discovery and defense development and improve the ecosystem’s security and privacy posture. Concretely, we systematically identify design weaknesses and propose attack-agnostic defenses for the 4G LTE and 5G NR main protocol stacks, as well as for the eSIM Machine-to-Machine Remote SIM Provisioning (M2M RSP) subprotocol, which allows for digital SIM card provisioning for IoT devices. To discover vulnerabilities and overcome the system’s complexity, which hinders a rich analysis, we devise and apply various types of abstraction that stem from domain knowledge. Using this abstraction, we develop the 5GReasoner framework, a systematic model-based testing framework. 5GReasoner combines symbolic model checkers and a cryptographic protocol verifier in a lazy fashion. Thanks to the abstractions we developed, 5GReasoner is the first framework to reason about two protocol layers, resulting in 11 new vulnerabilities and 5 design weaknesses inherited from previous generations. To develop a defense, we opt for designing an attack-agnostic defense and utilize the insight that vulnerabilities in cellular can be interpreted as violations of temporal properties to design PHOENIX. PHOENIX is the first attack-agnostic defense with the required scalability to be considered viable. To achieve this, PHOENIX relies on temporal formulas to identify the presence of attacks, or misconfigurations, from the vantage point of a cellular device by relying on runtime monitors. To verify the critical assumption that SIM cards are secure, even in the eSIM world, we explore both vulnerability identification and defense development for the eSIM M2M RSP protocol. Unlike the existing but minimal work, we are the first to conduct a rich and in-depth formal analysis of this protocol. We are the first to highlight the implicit assumption that parallelism is required in the system. Harnessing this insight, we focus on identifying potential concurrency bugs, which leads to a compositional analysis of this asynchronous system and discover 31 race conditions with serious implications. To develop a defense against these race conditions, we design, formally verify, and empirically analyze a proposed defense. We show that our fine-grained synchronization mechanism is scalable while providing the required security guarantees.
description: Our work has influenced ongoing research and has directly impacted today’s world. The corresponding standard bodies acknowledged the findings discovered by 5GReasoner, and the standard specification has changes that stem directly from our findings. PHOENIX proved to be an effective solution and gathered the attention of DARPA and Qualcomm. DARPA funded this work and envisioned applying PHOENIX to protect cellular devices used by high-profile users, such as government officials. In addition to this, we carried out various conversations with Qualcomm, as they envisioned implementing PHOENIX to protect their Cellular Vehicle-to-Everything (CV2X) connectivity platform. Finally, our ongoing work and eSIM findings have led us to be once again indicted in the GSMA Research Acknowledgement list, and we are in ongoing conversations with their expert panel to discuss our proposed locking mechanism, as well as make the atomicity guarantees explicit as this is the root of concurrency issues we discovered.