Research and Projects

LLM-based protocol analysis [AACL 2023]:

1. 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/

2. 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

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

1. 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: 

2. 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: 

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

1. 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: 

2. 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.


3. 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.

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

ATFuzzer Architecture

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: 

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

1. 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

2. 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

3. 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: