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.


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.

Related paper: LTEInspector: A Systematic Approach for Adversarial Testing of 4G LTE
Media: Wired, Washington Post, TechCrunch, MSN News, The Register, Threat Post, The Verge, 80+ outlets.


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


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
News: TechCrunch, Xiaomi, Deep Security News, My Digi Tech, Android Police, and 40+ outlets.
Award: Distinguished Paper Award, ACSAC’19.
❍ 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.


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.

Related paper: PatrIoT: Policy Assisted Resilient Programmable IoT System


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.

Related papers:
DetAnom: Detecting Anomalous Database Transaction by Insiders
A System for Profiling and Monitoring Database Access Patterns by Application Programs for Anomaly Detection
DBSAFE – An Anomaly Detection System to Protect Databases from Exfiltration Attempts

Building Countermeasures and Clean-slate Architectures

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.

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.

Related paper: Analyzing the Attack Landscape of Zigbee-enabled IoT System sand Reinstating Users’ Privacy

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.

Related paper: Insecure Connection Bootstrapping in Cellular Networks: The Root of All Evil

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.

Related paper: Protecting the 4G and 5G Cellular Paging Protocols against Security and Privacy Attacks

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

Related papers:
Privacy Attacks to the 4G and 5G Cellular Paging Protocols Using Side Channel Information
Protecting the 4G and 5G Cellular Paging Protocols against Security and Privacy Attacks

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.

Related papers:
SeamBlue: Seamless Bluetooth Low Energy Connection Migration for Unmodified IoT Devices
Secure Seamless Bluetooth Low Energy Connection Migration for Unmodified IoT Devices
Award: Best Paper Award Nomination, ACM SIGBED EWSN’17.

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.

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