Research

NLP for Security Analysis

Natural Language Processing (NLP) techniques offer a powerful toolkit for enhancing principled security analysis of complex systems and networks. We are exploring how NLP can be used to parse vast amounts of textual data, such as protocol and system specifications (e.g., RFC), and logs, to extract structured and formal representations of the systems/networks that are amenable for formal analysis or dynamic testing.

HERMES

In this paper, we present Hermes, an end-to-end framework to automatically generate formal representations from natural language cellular specifications. We first develop a neural constituency parser, NEUTREX, to process transition-relevant texts and extract transition components (i.e., states, conditions, and actions). We also design a domain-specific language to translate these transition components to logical formulas by leveraging dependency parse trees. Finally, we compile these logical formulas to generate transitions and create the formal model as finite state machines. To demonstrate the effectiveness of Hermes, we evaluate it on 4G NAS, 5G NAS, and 5G RRC specifications and obtain an overall accuracy of 81-87%, which is a substantial improvement over the state-of-the-art. Our security analysis of the extracted models uncovers 3 new vulnerabilities and identifies 19 previous attacks in 4G and 5G specifications, and 7 deviations in commercial 4G basebands.

Related paper: Hermes: Unlocking Security Analysis of Cellular Network Protocols by Synthesizing Finite State Machines from Natural Language Specifications
Tool: https://github.com/synsec-den/hermes-spec-to-fsm
Award: GSMA Mobile Security Hall of Fame
Vulnerabilities: CVD-2023-0071: 3 new vulnerabilities in the NAS and RRC layers of 5G networks

Formal Analysis of System/Protocol Design

Securing a complex system/network is a non-trivial task and requires analyzing the design-specifications/standards because vulnerabilities in the design are likely to trickle down to implementations/deployments. One key observation is that a systematic analysis of a system’s specification is albeit the basic building block, but is currently missing and not streamlined from the ground up. In this project, we design and implement frameworks for systematically investigating the design specifications of different systems/protocols in the context of security (e.g., secrecy and authenticity) and user privacy (observational equivalence, side-channel analysis). Some of the previous and ongoing projects in this direction are briefly discussed below.

5GCVerif

We present 5GCVerif, a model-based testing framework designed to formally analyze the access control framework of the 5G Core. With its modular design, 5GCVerif employs various abstraction techniques to craft an abstract model that captures the intricate details of the 5G Core’s access control mechanism. This approach offers customizability and extensibility in constructing the abstract model and addresses the state explosion problem in model checking. 5GCVerif also sidesteps the challenge of exhaustively generating models for all possible core network configurations by restricting the model checker to explore policy violations only within the valid network configurations. Using 5GCVerif, we evaluated 55 security properties, leading to the discovery of five new vulnerabilities in 5G Core’s access control mechanism. The uncovered vulnerabilities can result in multiple attacks including unauthorized entry to sensitive information, illegitimate access to services, and denial-of-services.

Related paper: Formal Analysis of Access Control Mechanism of 5G Core Network
Tool: https://github.com/SyNSec-den/5GCVerif
Award: GSMA Mobile Security Hall of Fame.
Vulnerabilities: CVD-2023-0069: 6 new vulnerabilities in the NAS and RRC layers of 5G networks.

LTEInspector

Cellular protocol models generally contain a number of participants (e.g., cellular device, base station, and core network) and run intertwined sub-protocols (e.g., attach, detach, and paging). This turns the verification task into an instance of the parameterized verification problem, which is undecidable. In addition, the use of cryptographic algorithms further contributes to the complexity of developing an automated verification framework. This observation has led us to develop LTEInspector which employs a property-driven adversarial model-based testing philosophy and aims for soundness instead of completeness. To keep the analysis tractable, we lazily combine a symbolic model checker (for reasoning trace properties or temporal ordering of different events/actions) and a cryptographic protocol verifier (for reasoning cryptographic constructs, e.g., encryption, integrity protections) in the symbolic attacker model using counter-example guided abstract refinement (CEGAR) principle. With LTEInspector, we were able to uncover 10 new attacks in the NAS (Non-Access Stratum) layer procedures of the 4G network. The combination of symbolic model checking and a cryptographic protocol verifier has introduced a novel automated reasoning technique for cellular network protocols. The uncovered design flaws and operational slip-ups identified by LTEInspector also resulted in changes in the existing 4G standards and deployed operational networks.

5GReasoner

Since the instantiation of the LTEInspector framework considers only a single layer (i.e., NAS) of the protocol stack and does not model packet payload, LTEInspector may miss out on interesting cross-layer and payload-dependent protocol behavior. To mitigate these limitations, we have designed the 5GReasoner framework with a different protocol modeling discipline for 5G networks. Since directly capturing all packet payloads impedes the scalability of our analysis, I capture only those packet payloads that impact the security- and privacy-specific behavior of the NAS and RRC (Radio Resource Control) layer protocols. To address the state-explosion problem of the model checking step due to payloads, we have employed behavior-specific predicate abstractions. 5GReasoner revealed 11 new exploitable protocol design weaknesses/flaws. The uncovered vulnerabilities and potential countermeasures have been acknowledged by GSMA and will be readjusted in Release 16.

Related paper: 5GReasoner: A Property-Directed Security and Privacy Analysis Framework for 5G Cellular Protocol
Tool: https://github.com/relentless-warrior/5GReasoner
News: Wired, TechCrunch, Forbes, MIT Technology Review, Yahoo Finance, 70+ outlets.
Award: GSMA Mobile Security Hall of Fame.
Vulnerabilities: CVD-2019-0029: 11 new vulnerabilities in the NAS and RRC layers of 5G networks.

Side-Channel Analysis

Though the coarse-grained behavior abstraction used in LTEInspector and 5GReasoner facilitates efficient reasoning but is unable to identify side-channel attack vectors that require to capture the low-level details of the massive cellular systems with fine-grained protocol-behavior abstraction. This will, however, trigger the state-space explosion problem which would make the analysis intractable. In this work, we, therefore, tried to identify side-channel attack surfaces in a particular sub-protocol of the 4G and 5G networks by leveraging insights drawn from a systematic approach and by exploiting sophisticated probabilistic reasoning techniques. We uncovered that the fixed nature of paging occasions (exact time periods when the cellular device wakes up and polls for paging message) and timing side-channel can be exploited by an adversary to associate a victim’s soft-identity (e.g., phone number, Twitter handle, Facebook ID) with victim device’s paging occasion through an attack dubbed ToRPEDO. We have also uncovered that ToRPEDO enables an adversary to infer a victim’s coarse-grained location information, inject fabricated emergency alert messages, and opens the gateway to retrieve a victim device’s persistent identity (i.e., IMSI) with a brute-force IMSI-Cracking attack. With the further investigation on 4G paging protocol deployments, we also identified an implementation oversight in more than 15 network providers in the USA, Europe, and Asia which enables an adversary to perform PIERCER attack for associating a victim’s phone number with its IMSI; subsequently allowing targeted user location tracking.

Related paper: Privacy Attacks to the 4G and 5G Cellular Paging Protocols Using Side Channel Information
News: Wired, Washington Post, TechCrunch, MSN News, Threat Post, The Verge, and 80+ outlets.
Award: Distinguished Paper Award Honorable Mention, NDSS’19, GSMA Mobile Security Hall of Fame.
Vulnerabilities: CVD-2018-0014: Static paging occasion of 4G and 5G networks, IMSI exposure through paging with IMSI, and IMSI-Cracking in 4G and 5G networks.

Systematic Evaluation of Implementations

Implementations often deviate from the design because of specification ambiguities, missing security and privacy requirements, unsafe practices and oversights stemming from inadequate input sanitization and simplification/optimization of complex protocol interactions. It is, therefore, pivotal to verify and monitor if protocol/system implementations faithfully adhere to the design specifications and the security and privacy requirements.

BLEDiff

In this work, we have developed 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 non-compliant 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 identify diverse deviations automatically. We evaluate BLEDiff with 25 different commercial devices and demonstrate it can uncover 13 different deviant behaviors with 10 exploitable attacks.

Related papers:
BLEDiff: Scalable and Property-Agnostic Noncompliance Checking for BLE Implementations
Tool: https://github.com/BLEDiff/BLEDiff
News:
Vulnerabilities:
❍ CVE-2022-45190 , HWPSIRT-2022-56262, CVE-2022-45189, HWPSIRT-2022-13244, CVE-2022-40480, CVE-2022-41768 , CVE-2022-45192 , HWPSIRT-2022-96208, CVE-2022-45191.
❍ Vulnerability disclosure report: https://blediff.github.io/

DIKEUE

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

Related papers:
Noncompliance as Deviant Behavior: An Automated Black-box Noncompliance Checker for 4G LTE Cellular Devices (CCS’21)
Tool: https://github.com/SyNSec-den/DIKEUE
News: College of Engineering, Penn State
Vulnerabilities:
❍ CVD-2021-0050: 11 new vulnerabilities in the 4G control plane protocol implementations of 14 different cellular devices.
❍ CVE-2021-25471 (Samsung), CVE-2021-25480 (Samsung), CVE-2021-40148 (MediaTek): Vulnerabilities in the baseband implementations of Samsung and MediaTek cellular modems.

ATFuzzer

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.

Related papers:
Opening Pandora’s Box through ATFuzzer: Dynamic Analysis of AT Interface for Android Smartphones
ATFuzzer: Dynamic Analysis Framework of AT Interface for Android Smartphones
Tool: https://github.com/Imtiazkarimik23/ATFuzzer
News: TechCrunch, Xiaomi, Deep Security News, My Digi Tech, Android Police, and 40+ outlets.
Award: Distinguished Paper Award, ACSAC’19.
Vulnerabilities:
❍ CVE-2019-16400: Samsung phones accept AT commands over Bluetooth resulting in several Denial of Service (DoS) attacks.
❍ CVE-2019-16401: Samsung phones accept AT commands over Bluetooth resulting in exposure of sensitive information, such as IMSI, IMEI, call status, and Internet service status.

Runtime-Monitoring of Systems

Even if we make sure a system’s design and implementation are compliant with the given security and privacy policies, in the runtime the system could be compromised through the weakest links or the unforeseen system interactions. Exploiting those the adversary could affect the correct operations of the system and induce safety, security, and privacy violations. It is, therefore, critical that we develop runtime-monitoring techniques that observe the system in runtime and check if the system’s behavior deviates from the correct/benign operations.

PatrIoT

Programmable IoT systems facilitate a user to install trigger-action rules to enable automation of customized tasks with heterogeneous IoT devices. Our key observation is that interactions of these trigger-action rules obtained from third-party sources may induce unexpected/unsafe behavior of the system and allow unrestricted access to devices and their sensitive data. This led us to design a runtime-monitoring framework dubbed PatrIoT that checks user-defined policies against the execution history of the system. PatrIoT efficiently monitors the behavior of a programmable IoT system at runtime and suppresses contemplated actions that violate a given declarative policy. Policies in PatrIoT are specified in effectively propositional, past metric temporal logic and capture the system’s expected temporal invariants whose violation can break its desired security, privacy, and safety guarantees. Our framework complements the existing work by supporting rich expressive policies capturing both the logical relation between different events and actions and the explicit time difference between two events. PatrIoT has been instantiated for not only an industrial IoT system (EVA ICS) but also for two home representative automation platforms: one proprietary (SmartThings) and another open-source (OpenHAB). Our empirical evaluation shows that, while imposing only a moderate runtime overhead, PatrIoT can effectively detect policy violations.

DetAnom

In this work, we have designed a runtime-monitoring system dubbed DetAnom to identify malicious database transactions issued by an application program. For this, we leveraged the intuition of concolic-execution technique to create a control-flow profile of the application program. The profile succinctly represents the application’s normal behavior in terms of its interaction (i.e., submission of SQL queries) with the database. For each query issued by an application, DetAnom creates a signature and also captures the corresponding preconditions that the application program must satisfy. During runtime, when the application issues a query, the corresponding signature and constraints are checked against the current context of the application. If there is a mismatch, the query is considered anomalous.

Building Clean-slate Architectures and Countermeasures

Systematic protocol analysis helps in identifying the root causes of vulnerabilities, and in designing efficient mitigation techniques and secure solutions that address the fundamental limitations of a protocol/system and fills the gap in the state-of-the-art. In what follows, we discuss some of the previous works that develop high-assurance countermeasures, defenses and clean-slate architectures.

Building a Privacy-Preserving Smart Camera System

Millions of consumers depend on smart camera systems to remotely monitor their homes and businesses. However, the architecture and design of popular commercial systems require users to relinquish control of their data to untrusted third parties, such as service providers (e.g., the cloud). Third parties therefore can (and in some instances have) access the video footage without the users’ knowledge or consent— violating the core tenet of user privacy. In this work, we design CaCTUs, a privacy-preserving smart Camera system Controlled Totally by Users. CaCTUs returns control to the user; the root of trust begins with the user and is maintained through a series of cryptographic protocols, designed to support popular features, such as sharing, deleting, and viewing videos live. We show that the system can support live streaming with a latency of 2 s at a frame rate of 10 fps and a resolution of 480 p. In so doing, we demonstrate that it is feasible to implement a performant smart-camera system that leverages the convenience of a cloud-based model while retaining the ability to control access to (private) data.

Reinstating Security and Privacy in ZigBee-enabled IoT Systems

Zigbee network security relies on symmetric cryptography based on a pre-shared secret. In the current Zigbee protocol, the network coordinator creates a network key while establishing a network. The coordinator then shares the network key securely, encrypted under the pre-shared secret, with devices joining the network to ensure the security of future communications among devices through the network key. The pre-shared secret, therefore, needs to be installed in millions or more devices prior to deployment and thus will be inevitably leaked, enabling attackers to compromise the confidentiality and integrity of the network. To improve the security of Zigbee networks, we propose a new certificate-less Zigbee joining protocol that leverages low-cost public-key primitives. The new protocol has two components. The first is to integrate Elliptic Curve Diffie-Hellman key exchange into the existing association request/response messages and to use this key both for link-to-link communication and for encryption of the network key for enhancing the privacy of user devices. The second is to improve the security of the installation code, a new joining method introduced in Zigbee 3.0 for enhanced security, by using public-key encryption. We analyze the security of our proposed protocol using the formal verification methods provided by ProVerif, and evaluate the efficiency and effectiveness of our solution with a prototype built with open source software and hardware stack. The new protocol does not introduce extra messages and the overhead is as lows as 3.8% on average for the join procedure.

Defense against fake base stations

Cellular devices currently do not have any mechanisms to authenticate a base station during the initial connection bootstrapping period. This lack of authentication has been shown to be exploitable by adversaries to install fake base stations which can lure unsuspecting devices to connect to them and then launch sophisticated attacks. This observation has led us to design a Public-Key Infrastructure (PKI) based authentication mechanism that leverages precomputation-based digital signature generation algorithms and employs several optimizations to address the trilemma of small signature size, efficient signature generation, and short verification time.

Defense against fake emergency alerts

After the establishment of secure connection and session keys with the core network and base station, when a device moves into an idle state, yet unprotected paging messages are broadcast by a base station in 4G and 5G networks to notify the device about incoming services (e.g., phone calls or SMS) and emergency (e.g., tsunami, earthquake, and amber) alerts. Taking this into consideration, we have designed PTESLA— a symmetric-key based broadcast authentication mechanism specifically tailored for 4G and 5G networks in order to protect the devices from unauthorized/fake paging messages.

Defense against side-channel attacks

We have also developed two countermeasures against ToRPEDOtype side-channel attacks that exploit the fixed/static paging occasion in 4G and 5G networks. While the first solution being geared towards backward compatibility carefully injects and blends noises with the actual paging messages, the second solution prescribes variable paging occasion based on the temporary identifier (TMSI).

Seamless connection migration in BLE-enabled IoT systems

In BLE-enabled IoT systems, a BLE device can communicate with only one gateway (e.g., a smartphone, or a BLE hub) at a time. When the peripheral goes out of range, it loses connectivity to the gateway, and cannot seamlessly communicate with another gateway without user interventions. To address this problem, we designed SeamBlue which enables seamless BLE connection migration for mobile IoT devices in a network of static or mobile BLE gateways deployed in airports, stadiums, and theme parks. we developed static program analysis-based approach to automatically identify the set of state variables defining BLE connection state to be migrated to the next gateway.

Securing the Insecure Link of Internet-of-Things Using Next-Generation Smart Gateways

Since low-cost IoT devices have limited computing resources and are often unable to guarantee sufficient security, it is imperative to ensure secure communication between IoT gateways and the cloud. In this work, we propose a flow-level adaptive mobile VPN solution specifically tailored for IoT ecosystems, called AdamVPN, which adapts its configuration dynamically at runtime in order to improve IoT gateway’s application-level throughput while conforming to the security and privacy guarantees simultaneously. Our deployment experiments in both Wi-Fi and cellular environments demonstrate that AdamVPN significantly improves throughput by 2.75x–3.0x for Wi-Fi and 1.8x–2.16x for cellular networks when compared to OpenVPN.