Final Exam - Applying Automated Reasoning to Analyze and Protect Cellular Network Protocols

Mitziu Echeverria - from linkedin.com/in/mitziu-echeverria-06a0528a

PhD Candidate: Mitziu Echeverria


Cellular networks, particularly with the evolution of 5G technology, have become a critical part of our modern infrastructure, supporting global communication, safety-critical applications, and numerous Internet-of-Things (IoT) applications. This is exemplified by New York City's transit system, which relies on cellular networks for managing thousands of interconnected traffic signals. However, this dependency also poses significant risks. These networks are vulnerable targets in cyber conflicts, and their compromise could lead to severe implications. Despite their critical role, cellular networks fail to provide the necessary security and privacy requirements, emphasizing an urgent need for enhanced security posture.

In response to these challenges, this thesis presents a comprehensive approach to bolster the security framework of cellular networks. This thesis introduces the 5GReasoner framework, utilizing symbolic model checkers and a cryptographic protocol verifier to formally analyze the 5G NR protocol, identifying 11 new vulnerabilities and design weaknesses on two layers. After this, we present PHOENIX, an attack-agnostic defense that leverages runtime verification to detect and counteract potential cellular network attacks and misconfigurations from a cellular device's perspective. Lastly, we analyze the recent integration of embedded-SIM (eSIM) in the cellular network ecosystem, which replaces physical SIM cards with digitalized versions sent over the air. While this paradigm change introduces new applications, it also potentially introduces new vulnerabilities. To understand this, we formally analyze the eSIM Machine-to-Machine Remote SIM Provisioning protocol to understand its potential dangers in the IoT world. This analysis uncovers 31 critical race condition bugs; in response, we develop a formally verified synchronization mechanism to defend against them.

The findings presented in this thesis have directly impacted the cellular network ecosystem's current security and privacy posture. Newer standard-derived cellular devices have changes stemming from our 5GReasoner findings. Government agencies, as well as world-leading industry companies, have recognized the potential for deploying PHOENIX in real-world deployments to protect numerous vulnerable devices, as well as protect government officials from these critical and stealthy attacks. Lastly, our eSIM analysis revealed critical bugs in existing systems, and our approach was praised by the standard body behind it, calling it novel compared to what is known to the corresponding panel.

Advisor: Kasturi Varadarajan

To join via Zoom, click here shortly before final exam time

Individuals with disabilities are encouraged to attend all University of Iowa–sponsored events. If you are a person with a disability who requires a reasonable accommodation in order to participate in this program, please contact in advance at