Logo image
5GReasoner: A Property-Directed Security and Privacy Analysis Framework for 5G Cellular Network Protocol
Conference proceeding   Open access

5GReasoner: A Property-Directed Security and Privacy Analysis Framework for 5G Cellular Network Protocol

Syed Rafiul Hussain, Mitziu Echeverria, Imtiaz Karim, Omar Chowdhury and Elisa Bertino
Proceedings of the 2019 ACM SIGSAC Conference on computer and communications security, pp.669-684
CCS '19
11/06/2019
DOI: 10.1145/3319535.3354263
url
https://doi.org/10.1145/3319535.3354263View
Published (Version of record) Open Access

Abstract

The paper proposes 5GReasoner, a framework for property-guided formal verification of control-plane protocols spanning across multiple layers of the 5G protocol stack. The underlying analysis carried out by 5GReasoner can be viewed as an instance of the model checking problem with respect to an adversarial environment. Due to an effective use of behavior-specific abstraction in our manually extracted 5G protocol, 5GReasoner's analysis generalizes prior analyses of cellular protocols by reasoning about properties not only regarding packet payload but also multi-layer protocol interactions. We instantiated 5GReasoner with two model checkers and a cryptographic protocol verifier, lazily combining them through the use of abstraction-refinement principle. Our analysis of the extracted 5G protocol model covering 6 key control-layer protocols spanning across two layers of the 5G protocol stack with 5GReasoner has identified 11 design weaknesses resulting in attacks having both security and privacy implications. Our analysis also discovered 5 previous design weaknesses that 5G inherits from 4G, and can be exploited to violate its security and privacy guarantees.
5G attacks cellular network model checking vulnerabilities

Details

Metrics

Logo image