Research and Projects

LLM-based protocol analysis [Usenix Security 2024, AACL 2023]:

CellularLint: A Systematic Approach to Identify Inconsistent Behavior in Cellular Network Specifications (Usenix Security 2024)

In recent years, there has been a growing focus on scrutinizing the security of cellular networks, often attributing security vulnerabilities to issues in the underlying protocol design descriptions. These protocol design specifications, typically extensive documents that are thousands of pages long, can harbor inaccuracies, underspecifications, implicit assumptions, and internal inconsistencies. In light of the evolving landscape, we introduce CellularLint–a semi-automatic framework for inconsistency detection within the standards of 4G and 5G, capitalizing on a suite of natural language processing techniques. Our proposed method uses a revamped few-shot learning mechanism on domain-adapted large language models. Pre-trained on a vast corpus of cellular network protocols, this method enables CellularLint to simultaneously detect inconsistencies at various levels of semantics and practical use cases. In doing so, CellularLint significantly advances the automated analysis of protocol specifications in a scalable fashion. In our investigation, we focused on the Non-Access-Stratum (NAS) and the security specifications of 4G and 5G networks, ultimately uncovering 157 inconsistencies with 82.67% accuracy. After verification of these inconsistencies on 3 open-source implementations and 17 commercial devices, we confirm that they indeed have a substantial impact on design decisions, potentially leading to concerns related to privacy, integrity, availability, and interoperability.

Software Artifacts: https://cellularlint.github.io/

SPEC5G: A Dataset for 5G Cellular Network Protocol Analysis (AACL 2023)

5G is the 5th generation cellular network protocol. It is the state-of-the-art global wireless standard that enables an advanced kind of network designed to connect virtually everyone and everything with increased speed and reduced latency. Therefore, its development, analysis, and security are critical. However, all approaches to the 5G protocol development and security analysis, e.g., property extraction, protocol summarization, and semantic analysis of the protocol specifications and implementations are completely manual. To reduce such manual effort, in this paper, we curate SPEC5G the first-ever public 5G dataset for NLP research. The dataset contains 3,547,586 sentences with 134M words, from 13094 cellular network specifications and 13 online websites. By leveraging large-scale pre-trained language models that have achieved state-of-the-art results on NLP tasks, we use this dataset for security-related text classification and summarization. Security-related text classification can be used to extract relevant security-related properties for protocol testing. On the other hand, summarization can help developers and practitioners understand the high level of the protocol, which is itself a daunting task. Our results show the value of our 5G-centric dataset in 5G protocol analysis automation. We believe that SPEC5G will enable a new research direction into automatic analyses for the 5G cellular network protocol and numerous related downstream tasks. Our data and code are publicly available.

Software Artifacts: https://github.com/Imtiazkarimik23/SPEC5G

Secure protocol design and defense [Usenix Security 2025A, Usenix Security 2025B, arXiv 2024]:

TIMESAFE: Timing Interruption Monitoring and Security Assessment for Fronthaul Environments (arXiv 2024)

5G and beyond cellular systems embrace the disaggregation of Radio Access Network (RAN) components, exemplified by the evolution of the fronthual (FH) connection between cellular baseband and radio unit equipment. Crucially, synchronization over the FH is pivotal for reliable 5G services. In recent years, there has been a push to move these links to an Ethernet-based packet network topology, leveraging existing standards and ongoing research for Time-Sensitive Networking (TSN). However, TSN standards, such as Precision Time Protocol (PTP), focus on performance with little to no concern for security. This increases the exposure of the open FH to security risks. Attacks targeting synchronization mechanisms pose significant threats, potentially disrupting 5G networks and impairing connectivity.

In this paper, we demonstrate the impact of successful spoofing and replay attacks against PTP synchronization. We show how a spoofing attack is able to cause a production-ready O-RAN and 5G-compliant private cellular base station to catastrophically fail within 2 seconds of the attack, necessitating manual intervention to restore full network operations. To counter this, we design a Machine Learning (ML)-based monitoring solution capable of detecting various malicious attacks with over 97.5% accuracy.

Gotta Detect ’Em All: Fake Base Station and Multi-Step Attack Detection in Cellular Networks (Usenix Security 2025A)

Fake base stations (FBSes) pose a significant security threat by impersonating legitimate base stations (BSes). Though efforts have been made to defeat this threat, up to this day, the presence of FBSes and the multi-step attacks (MSAs) stemming from them can lead to unauthorized surveillance, interception of sensitive information, and disruption of network services. Therefore, detecting these malicious entities is crucial to ensure the security and reliability of cellular networks. Traditional detection methods often rely on additional hardware, predefined rules, signal scanning, changes to protocol specifications, or cryptographic mechanisms that have limitations and incur huge infrastructure costs in accurately identifying FBSes. In this paper, we develop FBSDetector–an effective and efficient detection solution that can reliably detect FBSes and MSAs from layer-3 network traces using machine learning (ML) at the user equipment (UE) side. To develop FBSDetector, we create FBSAD and MSAD, the first-ever high-quality and large-scale datasets incorporating instances of FBSes and 21 MSAs. These datasets capture the network traces in different real-world cellular network scenarios (including mobility and different attacker capabilities) incorporating legitimate BSes and FBSes. Our novel ML framework, specifically designed to detect FBSes in a multi-level approach for packet classification using stateful LSTM with attention and trace level classification and MSAs using graph learning, can effectively detect FBSes with an accuracy of 96% and a false positive rate of 2.96%, and recognize MSAs with an accuracy of 86% and a false positive rate of 3.28%. We deploy FBSDetector as a real-world solution to protect end-users through a mobile app and validate it in real-world environments. Compared to the existing heuristic-based solutions that fail to detect FBSes, FBSDetector can detect FBSes in the wild in real time.

Media Coverage: Platforms for Advanced Wireless Research

AKMA+: Security and Privacy-Enhanced and Standard-Compatible AKMA for 5G Communication (Usenix Security 2025B)

The Authentication and Key Management for Applications (AKMA) protocol is a fundamental building block for security and privacy of 5G cellular networks. Therefore, it is critical that the protocol is free of vulnerabilities that can be exploited by attackers. Unfortunately, based on a detailed analysis of AKMA, we show that AKMA has several vulnerabilities that may lead to security and privacy breaches.

We define AKMA+, an enhanced protocol for 5G communication that protects against security and privacy breaches while maintaining compatibility with existing standards. AKMA+ includes countermeasures for protecting communication between the user equipment (UE) and application functions (AFs) from attackers, including those within the home public land mobile network. These countermeasures ensure mutual authentication between the UE and the AKMA anchor function without altering the protocol flow. We also address vulnerabilities related to subscriber and AKMA key identifiers that could be exploited in linkability attacks. By obfuscating this data, AKMA+ prevents attackers from associating a target UE with its past application access.

We employ formal verification to demonstrate that AKMA+ achieves key security and privacy objectives. We conduct extensive experiments demonstrating that AKMA+ incurs acceptable computational overhead, bandwidth costs, and UE battery consumption.

Protocol noncompliance checking [IEEE S&P 2023, CCS 2021]:

BLEDiff: Scalable and Property-Agnostic Noncompliance Checking for BLE Implementations (IEEE S&P 2023)

In this work, we develop an automated, scalable, property-agnostic, and black-box protocol noncompliance checking framework called BLEDiff that can analyze and uncover noncompliant behavior in the Bluetooth Low Energy (BLE) protocol implementations. To overcome the enormous manual effort of extracting BLE protocol reference behavioral abstraction and security properties from a large and complex BLE specification, BLEDiff takes advantage of having access to multiple BLE devices and leverages the concept of differential testing to automatically identify deviant noncompliant behavior. In this regard, BLEDiff first automatically extracts the protocol FSM of a BLE implementation using the active automata learning approach. To improve the scalability of active automata learning for the large and complex BLE protocol, BLEDiff explores the idea of using a divide and conquer approach. BLEDiff essentially divides the BLE protocol into multiple sub-protocols, identifies their dependencies and extracts the FSM of each sub-protocol separately, and finally composes them to create the large protocol FSM. These FSMs are then pair-wise tested to automatically identify diverse deviations. We evaluate BLEDiff with 25 different commercial devices and demonstrate it can uncover 13 different deviant behaviors with 10 exploitable attacks.

Software Artifacts: https://github.com/BLEDiff/BLEDiff

Media Coverage: Security advisory STMicroelectronics

Bug Reports CVDs/CVEs:

Google/Android Security bug bounty reward of $10,000 USD
Huawei Security bug bounty and acknowledgments: HWPSIRT-2022-56262, HWPSIRT-2022-13244, HWPSIRT-2022-96208
Security advisory from STMicroelectronics (TN1436-ST-PSIRT)
High and medium-severity CVE's assigned to some of the implementation issues we found in different BLE implementations: CVE-2022-40480, CVE-2022-41768, CVE-2022-45190, CVE-2022-45192, CVE-2022-45191

Noncompliance as Deviant Behavior: An Automated Black-box Noncompliance Checker for 4G LTE Cellular Devices (CCS 2021)

The work focuses on developing an automated black-box testing approach called DIKEUE that checks 4G Long Term Evolution (LTE) control-plane protocol implementations in commercial-off-the-shelf (COTS) cellular devices (also, User Equipments or UEs) for noncompliance with the standard. Unlike prior noncompliance checking approaches which rely on property-guided testing, DIKEUE adopts a property-agnostic, differential testing approach, which leverages the existence of many different control-plane protocol implementations in COTS UEs. DIKEUE uses deviant behavior observed during differential analysis of pairwise COTS UEs as a proxy for identifying noncompliance instances. For deviant behavior identification, DIKEUE first uses black-box automata learning, specialized for 4G LTE control-plane protocols, to extract input-output finite state machine (FSM) for a given UE. It then reduces the identification of deviant behavior in two extracted FSMs as a model checking problem. We applied DIKEUE in checking noncompliance in 14 COTS UEs from 5 vendors and identified 15 new deviant behavior as well as 2 previous implementation issues. Among them, 11 are exploitable whereas 3 can cause potential interoperability issues.

Software Artifacts: https://github.com/SyNSec-den/DIKEUE

Media Coverage: College of Engineering (PenState), Qualcomm Product Security Bulletins, Android Security Acknowledgements, MediaTek Product Security Acknowledgements

Bug Reports CVDs/CVEs:

Inducted to GSMA Mobile Security Research Acknowledgements (formerly Hall of Fame) [GSMA CVD-2021-0050]
Google Bug Bounty Reward, Samsung Bug Bounty Reward, MediaTek Security Acknowledgements, Qualcomm Security Bulletins
High-severity CVE's assigned to some of the implementation issues we found in different UE implementations: CVE-2021-25471, CVE-2021-25480, CVE-2021-40148, CVE-2021-30344, SVE-2021-22327, SVE-2021-22324, CVE-2022-25685, CVE-2022-22091

Systematic implementation analysis [ICDCS 2021, ACSAC 2019, Intel SWPC 2020]:

ProChecker: An Automated Security and Privacy Analysis Framework for 4G LTE Protocol Implementations (ICDCS 2021):

Cellular protocol implementations must comply with the specifications, and the security and privacy requirements. These implementations, however, often deviate from the security and privacy requirements due to under specifications in cellular standards, inherent protocol complexities, and design flaws inducing logical vulnerabilities. Detecting such logical vulnerabilities in the complex and stateful 4G LTE protocol is challenging due to operational dependencies on internal-states, and intertwined complex protocol interactions among multiple participants. In this paper, we address these challenges and develop ProChecker which— (1) extracts a precise semantic model as a finite state machine of the implementation by combining dynamic testing with static instrumentation, and (2) verifies the properties against the extracted model by combining a symbolic model checker and a cryptographic protocol verifier. We demonstrate the effectiveness of ProChecker by evaluating it on a closed source and two of the most popular open-source 4G LTE control plane protocol implementations with 62 properties. ProChecker unveiled 3 new protocol-specific logical attacks, 6 implementation issues, and detected 14 prior attacks. The impact of the attacks range from denial-of-service, broken integrity, encryption, and replay protection to privacy leakage. Our team has been inducted into the GSMA mobile security hall of fame (CVD-2021-0043) for uncovering these vulnerabilities and coordinating mitigations in the 4G/5G cellular protocol standards. This paper also received the best paper award nomination at ICDCS 2021.

Media Coverage: College of Engineering (PenState)

Bug Reports CVDs/CVEs:

Inducted to GSMA Mobile Security Research Hall of Fame [GSMA CVD-2021-0043]

Utilizing Symbolic Execution for Property-Guided Security and Privacy Testing in Communication Protocol Implementations (Intel SoftWare Practitioners Conference, Intel SWPC 2020):

Created a framework for property-guided security and privacy testing of communication protocol implementations. The framework utilizes symbolic execution with dynamic simulation to employ a hybrid approach to uncover both protocol and implementation vulnerabilities. Initially, it is deployed to the Link Manager (LM) layer of Intel's BR/EDR and BLE implementations.

Security and Privacy Analysis Framework for Communication Protocol Implementations

(Intel SoftWare Practitioners Conference, Intel SWPC 2020):

Proposed a framework to formally verify commercial communication protocol implementations. Part of the framework is a novel model extraction tool that can be applied to any communication protocol implementation to extract a semantic model of the implementation. The framework is deployed in Intel's 4G /5G implementation.

Opening Pandora’s Box through ATFuzzer: Dynamic Analysis of AT Interface for Android Smartphones (ACSAC 19):

In modern smartphones, the AT interface is an entry point for accessing the baseband processor (i.e., cellular modem) for performing cellular network-related actions (e.g., making phone calls). As part of the end-to-end investigation of cellular ecosystems, it is therefore critical to analyze the correctness and robustness of this interface. We have designed a grammar-guided evolutionary fuzzing framework dubbed ATFuzzer that mutates the production rules of the AT grammars (i.e., the symbolic representation of AT commands) instead of concrete AT command instance to efficiently navigate the input search space. Due to closed-source firmware, we leveraged the execution time of each AT command as a loose-indicator of code-coverage information. ATFuzzer has been able to uncover 4 erroneous AT grammars over Bluetooth and 13 AT grammars over USB. The vulnerabilities have been acknowledged by vendors with CVE-2019-16400 and CVE-2019-16401 and awarded Samsung Bug Bounty Reward. This paper also received the distinguished paper award at ACSAC 2019.

Software Artifacts: https://github.com/Imtiazkarimik23/ATFuzzer (120+ stars)

Media Coverage: TechCrunch, Xiaomi, Deep Security News, My Digi Tech, Android Police, and 40+ media outlets all over the world

Bug Reports CVDs/CVEs:

Samsung Bug Bounty Reward
CVE: CVE-2019-16401, CVE-2019-16400

Formal analysis of protocol standards [AsiaCCS 2024, AsiaCCS 2022, CCS 2019, VehicleSec 2024]:

Segment-Based Formal Verification of WiFi Fragmentation and Power Save Mode (ASIA CCS 2024):

The IEEE 802.11 family of standards, better known as WiFi, is a widely used protocol utilized by billions of users. Previous works on WiFi formal verification have mostly focused on the four-way handshake and other security aspects. However, recent works have uncovered severe vulnerabilities in functional aspects of WiFi, which can cause information leakage for billions of devices. No formal analysis method exists able to reason on the functional aspects of the WiFi protocol. In this paper, we take the first steps in addressing this gap and present an extensive formal analysis of the functional

aspects of the WiFi protocol, more specifically, the fragmentation and the power-save-mode process. To achieve this, we design a novel segment-based formal verification process and introduce a practical threat model (i.e., MAC spoofing) in Tamarin to reason

about the various capabilities of the attacker. To this end, we verify 68 properties extracted from WiFi protocol specification, find 3 vulnerabilities from the verification, verify 3 known attacks, and discover 2 new issues. These vulnerabilities and issues affect 14 commercial devices out of 17 tested cases, showing the prevalence and impact of the issues. Apart from this, we show that the proposed countermeasures indeed are sufficient to address the issues. We hope our results and analysis will help vendors adopt the countermeasures and motivate further research into the verification of

the functional aspects of the WiFi protocol.

Software Artifacts: https://github.com/Zilinlin/FunctionalWifiModelTesting

VWANALYZER: A Systematic Security Analysis Framework for the Voice over WiFi Protocol (ASIA CCS 2022):

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 scenarios. Then the scenarios are verified against security properties. Notable among our findings is the denial-of-cellular-connectivity attack, due to insecure handover that disconnects the user through both VoWiFi and VoLTE.

Software Artifacts: https://github.com/vwanalyzer

5GReasoner: A Property-Directed Security and Privacy Analysis Framework for 5G Cellular Network Protocol (CCS 2019):

We proposed "5GReasoner" a framework for the property guided formal verification of control-plane protocols spanning across multiple layers of the 5G protocol stack. 5GReasoner has identified 11 design weaknesses in multiple 5G protocols resulting in attacks having both security and privacy implications. Our analysis also discovered 5 previous design weaknesses that 5G inherits from its 4G counterpart, and can be exploited to violate its security and privacy guarantees. Our team has been inducted into the GSMA mobile security hall of fame (CVD-2019-0029) for detecting and providing suggestions in mitigating the weakness in 5G cellular protocol standards.

Software Artifacts: https://github.com/relentless-warrior/5GReasoner (20+ stars)

Media Coverage: Wired, TechCrunch, Forbes, MIT Technology Review, Yahoo Finance, and 80+ media outlets all over the world

Bug Reports CVDs/CVEs:

Inducted to GSMA Mobile Security Research Hall of Fame [GSMA CVD-2019-0029]

Security Attacks to the Name Management Protocol in Vehicular Networks (VehicleSec 2024):

Trucks play a critical role in today’s transportation system, where minor disruptions can result in a major social impact. Intra Medium and Heavy Duty (MHD) communications broadly adopt SAE-J1939 recommended practices that utilize Name Management Protocol (NMP) to associate and manage source addresses with primary functions of controller applications. This paper exposes 19 vulnerabilities in the NMP, uses them to invent various logical attacks, in some cases leveraging and in all cases validating with formal methods, and discusses their impacts. These attacks can–➀ stealthily deny vehicle start-up by pre-playing recorded claims in monotonically descending order; ➁ successfully restrain critical vehicular device participation and institute a dead beef attack, causing reflash failure by performing a replay attack; ➂ cause stealthy address exhaustion, Thakaavath–exhaustion in Sanskrit, which rejects an address-capable controller application from network engagement by exhausting the usable address space via pre-playing claims in monotonically descending order; ➃ poison the controller application’s internally maintained source address-function association table after bypassing the imposter detection protection and execute a stealthy SA-NAME Table Poisoning Attack thereby disable radar and Anti Brake System (ABS), as well as obtain retarder braking torque dashboard warnings; ➄ cause Denial of Service (DoS) on claim messages by predicting the delay in an address reclaim and prohibiting the associated device from participating in the SAE-J1939 network; ➅ impersonate a working set master to alter the source addresses of controller applications to execute a Bot-Net attack; ➆ execute birthday attack, a brute-force collision attack to command an invalid or existing name, thereby causing undesired vehicle behavior. The impact of these attacks is validated by demonstrations on real trucks in operation in a practical setting and on bench setups with a real engine controller connected to a CAN bus.

Google Sites

Report abuse