TY - GEN
T1 - Formal Analysis of Access Control Mechanism of 5G Core Network
AU - Akon, Mujtahid
AU - Yang, Tianchang
AU - Dong, Yilu
AU - Hussain, Syed Rafiul
N1 - Publisher Copyright:
© 2023 Copyright held by the owner/author(s).
PY - 2021/11/21
Y1 - 2021/11/21
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85179847739&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85179847739&partnerID=8YFLogxK
U2 - 10.1145/3576915.3623113
DO - 10.1145/3576915.3623113
M3 - Conference contribution
AN - SCOPUS:85179847739
T3 - CCS 2023 - Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security
SP - 666
EP - 680
BT - CCS 2023 - Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security
PB - Association for Computing Machinery, Inc
T2 - 30th ACM SIGSAC Conference on Computer and Communications Security, CCS 2023
Y2 - 26 November 2023 through 30 November 2023
ER -