Analyzing Protocol/System Design
Securing cellular networks is a complex 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 cellular standards is albeit the basic building block, but is currently missing. In this project, we design and implement frameworks for systematically investigating 4G and 5G cellular protocol standards in the context of security and user privacy.
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 contribute 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 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.
Since the instantiation of 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 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 employ 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 the Release 16.
Though the coarse-grained behavior abstraction used in LTEInspector and 5GReasoner facilitates efficient reasoning, but is unable to identify side-channel attack vectors which requires 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 ncovered 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 further investigation on 4G paging protocol deployments, we also identified an implementation oversight in more than 15 network providers in 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.
Verifying Implementations and Monitoring Systems
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 firmwares, 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.
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 as anomalous.
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.
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 precomputationbased 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 core network and base station, when a device moves into 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 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 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 applicationlevel 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.