TY - GEN
T1 - 5Greasoner
T2 - 26th ACM SIGSAC Conference on Computer and Communications Security, CCS 2019
AU - Hussain, Syed Rafiul
AU - Echeverria, Mitziu
AU - Karim, Imtiaz
AU - Chowdhury, Omar
AU - Bertino, Elisa
N1 - Funding Information:
We thank the anonymous reviewers for their suggestions. This work is supported by NSF grants CNS-1657124 and CNS-1719369, Intel, and a grant by Purdue Research Foundation.
Publisher Copyright:
© 2019 Association for Computing Machinery.
PY - 2019/11/6
Y1 - 2019/11/6
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85075929999&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85075929999&partnerID=8YFLogxK
U2 - 10.1145/3319535.3354263
DO - 10.1145/3319535.3354263
M3 - Conference contribution
AN - SCOPUS:85075929999
T3 - Proceedings of the ACM Conference on Computer and Communications Security
SP - 669
EP - 684
BT - CCS 2019 - Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security
PB - Association for Computing Machinery
Y2 - 11 November 2019 through 15 November 2019
ER -