Dissertation
Applying automated reasoning to analyze and protect cellular network protocols
University of Iowa
Doctor of Philosophy (PhD), University of Iowa
Autumn 2023
DOI: 10.25820/etd.006921
Abstract
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.
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.
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.
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.
Details
- Title: Subtitle
- Applying automated reasoning to analyze and protect cellular network protocols
- Creators
- Mitziu Echeverria
- Contributors
- Kasturi R. Varadarajan (Advisor)Omar Haider Chowdhury (Committee Member)Cesare Tinelli (Committee Member)Rishab Nithyanand (Committee Member)Syed Rafiul Hussain (Committee Member)
- Resource Type
- Dissertation
- Degree Awarded
- Doctor of Philosophy (PhD), University of Iowa
- Degree in
- Computer Science
- Date degree season
- Autumn 2023
- Publisher
- University of Iowa
- DOI
- 10.25820/etd.006921
- Number of pages
- xv, 147 pages
- Copyright
- Copyright 2023 Mitziu Echeverria
- Grant note
- DARPA funded this work
- Language
- English
- Date submitted
- 12/03/2023
- Description illustrations
- Illustrations, tables, graphs, charts
- Description bibliographic
- Includes bibliographical references (pages 132-145).
- Public Abstract (ETD)
Cellular networks are vital in modern infrastructure, supporting global communication, safety-critical applications, and IoT applications. For instance, New York City’s transit system relies on cellular networks to manage traffic signals. However, their importance also makes them attractive targets for cyberattacks, posing significant risks. Despite their critical role, cellular networks fail to provide the necessary security and privacy requirements, emphasizing an urgent need for enhanced security posture.
This thesis addresses these challenges by presenting a comprehensive approach to improving cellular network security. The 5GReasoner framework is introduced, utilizing symbolic model checkers and cryptographic protocol verification to formally analyze the 5G NR protocol. This analysis uncovers 11 new vulnerabilities and design weaknesses across two layers. To defend against potential network attacks, PHOENIX, an attack-agnostic defense mechanism, leverages runtime verification from the perspective of cellular devices.
Additionally, the integration of embedded SIM (eSIM) in cellular networks is explored. While eSIM offers new applications and greater flexibility, it also introduces potential vulnerabilities. Our formal analysis of the eSIM Machine-to-Machine Remote SIM Provisioning protocol reveals 31 critical race condition bugs. In response, we developed a formally verified synchronization mechanism to protect the eSIM protocol.
These findings have directly influenced the security of cellular networks. Newer cellular devices now incorporate changes based on 5GReasoner findings. Government agencies and industry leaders consider deploying PHOENIX for real-world protection against attacks, including safeguarding vulnerable devices and government officials. Lastly, our eSIM analysis uncovered critical bugs and received recognition from the relevant standard body for its innovative approach.
- Academic Unit
- Computer Science
- Record Identifier
- 9984546648402771
Metrics
2 File views/ downloads
23 Record Views