Research and Projects
Implementation Analysis:
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.
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.
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 finitestate 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 closedsource and two of the most popular open-source 4G LTE controlplane 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.
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
Formal Analysis of Protocol Standards:
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.
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