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

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.

References

1. Dare Abodunrin, Yoan Miche, and Silke Holtmanns. 2015. Some dangers from 2g networks legacy support and a possible mitigation. In 2015 IEEE Conference on Communications and Network Security (CNS). IEEE, 585--593.
2. Iosif Androulidakis. 2011. Intercepting Mobile Phone Calls and Short Messages Using a GSM Tester. In 18th Conference on Computer Networks, Ustron, Poland, Andrzej Kwiecie'n, Piotr Gaj, and Piotr Stera (Eds.). 281--288.
3. Myrto Arapinis, Loretta Mancini, Eike Ritter, Mark Ryan, Nico Golde, Kevin Redon, and Ravishankar Borgaonkar. 2012. New privacy issues in mobile telephony: fix and verification. In Proceedings of the 2012 ACM conference on Computer and communications security. ACM, 205--216.
4. Myrto Arapinis, Loretta Ilaria Mancini, Eike Ritter, and Mark Ryan. 2014. Privacy through Pseudonymity in Mobile Telephony Systems. In NDSS.
5. Clark Barrett, Roberto Sebastiani, Sanjit Seshia, and Cesare Tinelli. 2009. Satisfiability Modulo Theories. In Handbook of Satisfiability,, Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh (Eds.). Vol. 185. IOS Press, Chapter 26, 825--885.
6. David Basin, Jannik Dreier, Lucca Hirschi, Savsa Radomirovic, Ralf Sasse, and Vincent Stettler. 2018. A Formal Analysis of 5G Authentication. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (CCS '18). ACM, New York, NY, USA, 1383--1396. https://doi.org/10.1145/3243734.3243846
7. Bruno Blanchet. 2001. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In Proceedings of the 14th IEEE Workshop on Computer Security Foundations (CSFW '01). IEEE Computer Society, 82--.
8. Bruno Blanchet. 2009. Automatic Verification of Correspondences for Security Protocols. Journal of Computer Security, Vol. 17, 4 (July 2009), 363--434.
9. Ravishankar Borgaonkar and Swapnil Udar. 2014. Understanding imsi privacy. In Vortrag auf der Konferenz Black Hat.
10. Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. 2014. The nuXmv Symbolic Model Checker. In CAV. 334--342.
11. Adrien Champion, Alain Mebsout, Christoph Sticksel, and Cesare Tinelli. 2016. The Kind 2 model checker. In International Conference on Computer Aided Verification. Springer, 510--517.
12. Chlosta, Merlin, David Rupprecht, Thorsten Holz, and Christina Pöpper. 2019. LTE Security Disabled-Misconfiguration in Commercial Networks.
13. Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2000. Counterexample-guided abstraction refinement. In International Conference on Computer Aided Verification. Springer, 154--169.
14. Cas Cremers and Martin Dehnel-Wild. 2019. Component-Based Formal Analysis of 5G-AKA: Channel Assumptions and Session Confusion. (2019).
15. Adrian Dabrowski, Nicola Pianta, Thomas Klepp, Martin Mulazzani, and Edgar Weippl. 2014. IMSI-catch Me if You Can: IMSI-catcher-catchers. In Proceedings of the 30th Annual Computer Security Applications Conference (ACSAC '14). 246--255.
16. Danny Dolev and Andrew C. Yao. 1981. On the Security of Public Key Protocols. Technical Report.
17. E.Rescorla. [n.d.]. The Transport Layer Security (TLS) Protocol Version 1.3. [Online]. Available: https://tools.ietf.org/pdf/draft-ietf-tls-tls13--28.pdf. Network Working Group, Internet Engineering Task Force (IETF), RFC 8446 ( [n.,d.]).
18. Daniel Fett, Ralf Küsters, and Guido Schmitz. 2016. A Comprehensive Formal Security Analysis of OAuth 2.0. In Proceedings of the 23rd ACM SIGSAC Conference on Computer and Communications Security (CCS 2016). ACM, 1204--1215.
19. Nicholas Halbwachs, Paul Caspi, Pascal Raymond, and Daniel Pilaud. 1991. The synchronous data flow programming language LUSTRE. Proc. IEEE, Vol. 79, 9 (1991), 1305--1320.
20. Syed Rafiul Hussain, Omar Chowdhury, Shagufta Mehnaz, and Elisa Bertino. 2018. LTEInspector: A Systematic Approach for Adversarial Testing of 4G LTE. In 25th Annual Network and Distributed System Security Symposium, NDSS, San Diego, CA, USA, February 18--21.
21. Syed Rafiul Hussain, Mitziu Echeverria, Omar Chowdhury, Ninghui Li, and Elisa Bertino. 2019 a. Privacy Attacks to the 4G and 5G Cellular Paging Protocols Using Side Channel Information. In 26th Annual Network and Distributed System Security Symposium, NDSS, San Diego, CA, USA, February 24--27, 2019.
22. Syed Rafiul Hussain, Mitziu Echeverria, Ankush Singla, Omar Chowdhury, and Elisa Bertino. 2019 b. Insecure connection bootstrapping in cellular networks: the root of all evil. In Proceedings of the 12th Conference on Security and Privacy in Wireless and Mobile Networks. ACM, 1--11.
23. Roger Piqueras Jover. 2016. LTE security, protocol exploits and location tracking experimentation with low-cost software radio. CoRR, Vol. abs/1607.05171 (2016). arxiv: 1607.05171 http://arxiv.org/abs/1607.05171
24. Mohammed Shafiul Alam Khan and Chris J Mitchell. 2017. Trashing IMSI Catchers in Mobile Networks. In Proceedings of the 10th ACM Conference on Security and Privacy in Wireless and Mobile Networks. 207--218.
25. Byengdo Kim, Sangwook Bae, and Yongdae Kim. 2018. GUTI Reallocation Demystified: Cellular Location Tracking with Changing Temporary Identifier. In 25th Annual Network and Distributed System Security Symposium, NDSS, San Diego, CA, USA, February 18--21.
26. Hongil Kim, Dongkwan Kim, Minhee Kwon, Hyungseok Han, Yeongjin Jang, Dongsu Han, Taesoo Kim, and Yongdae Kim. 2015. Breaking and Fixing VoLTE: Exploiting Hidden Data Channels and Mis-implementations. In Proceedings of the 22Nd ACM SIGSAC Conference on Computer and Communications Security (CCS '15). ACM, New York, NY, USA, 328--339.
27. Hongil Kim, Jiho Lee, Lee Eunkyu, and Yongdae Kim. 2019. Touching the Untouchables: Dynamic Security Analysis of the LTE Control Plane. In Proceedings of the IEEE Symposium on Security & Privacy (SP). IEEE.
28. Kathrian Kohls, David Rupprecht, Thorsten Holz, and Christina Pöpper. 2019. Lost Traffic Encryption: Fingerprinting LTE/4G Traffic on Layer Two.
29. Denis Foo Kune, John Koelndorfer, and Yongdae Kim. 2012. Location Leaks on the GSM Air Interface. In NDSS.
30. Kenneth L McMillan. 1993. The SMV system. In Symbolic Model Checking. Springer, 61--85.
31. Ulrike Meyer and Susanne Wetzel. 2004. A Man-in-the-Middle Attack on UMTS. In Proceedings of the 3rd ACM Workshop on Wireless Security (WiSe '04). ACM, 90--97.
32. Benoit Michau and Christophe Devine. [n.d.]. How to not break LTE crypto.
33. Shinjo Park, Altaf Shaik, Ravishankar Borgaonkar, Andrew Martin, and Jean-Pierre Seifert. 2017. White-Stingray: Evaluating IMSI Catchers Detection Applications. In 11th USENIX Workshop on Offensive Technologies (WOOT '17). USENIX Association, Vancouver, BC. https://www.usenix.org/conference/woot17/workshop-program/presentation/park
34. Roger Piqueras Jover. 2013. Security Attacks Against the Availability of LTE Mobility Networks: Overview and Research Directions. In Wireless Personal Multimedia Communications (WPMC), 2013 16th International Symposium on.
35. Muhammad Taqi Raza, Fatima Muhammad Anwar, and Songwu Lu. 2017. Exposing LTE Security Weaknesses at Protocol Inter-Layer, and Inter-Radio Interactions. In International Conference on Security and Privacy in Communication Systems. Springer, 312--338.
36. David Rupprecht, Kai Jansen, and Christina Pöpper. 2016. Putting $$LTE$$ Security Functions to the Test: A Framework to Evaluate Implementation Correctness. In 10th $$USENIX$$ Workshop on Offensive Technologies ($$WOOT$$ 16).
37. David Rupprecht, Katharina Kohls, Thorsten Holz, and Christina Pöpper. 2019. Breaking LTE on Layer Two. In IEEE Symposium on Security & Privacy (SP). IEEE.
38. Altaf Shaik, Ravishankar Borgaonkar, Shinjo Park, and Jean-Pierre Seifert. 2018. On the Impact of Rogue Base Stations in 4G/LTE Self Organizing Networks. In Proceedings of the 11th ACM Conference on Security & Privacy in Wireless and Mobile Networks (WiSec '18). ACM, New York, NY, USA, 75--86. https://doi.org/10.1145/3212480.3212497
39. Altaf Shaik, Ravishankar Borgaonkar, Shinjo Park, and Jean-Pierre Seifert. 2019. New Vulnerabilities in 4G and 5G Cellular Access Network Protocols: Exposing Device Capabilities. In Proceedings of the 12th Conference on Security and Privacy in Wireless and Mobile Networks (WiSec '19). ACM, New York, NY, USA, 221--231. https://doi.org/10.1145/3317549.3319728
40. Altaf Shaik, Jean-Pierre Seifert, Ravishankar Borgaonkar, N. Asokan, and Valtteri Niemi. 2016. Practical Attacks Against Privacy and Availability in 4G/LTE Mobile Communication Systems. In 23nd Annual Network and Distributed System Security Symposium, NDSS, San Diego, CA, USA, February 21--24.
41. Guan-Hua Tu, Yuanjie Li, Chunyi Peng, Chi-Yu Li, Hongyi Wang, and Songwu Lu. 2014. Control-plane Protocol Interactions in Cellular Networks. In Proceedings of the 2014 ACM Conference on SIGCOMM. ACM, 223--234.
42. Hojoon Yang, Sangwook Bae, Mincheol Son, Hongil Kim, Song Min Kim, and Yongdae Kim. 2019. Hiding in Plain Signal: Physical Signal Overshadowing Attack on LTE. In 28th USENIX Security Symposium (USENIX Security 19). USENIX Association, Santa Clara, CA, 55--72. https://www.usenix.org/conference/usenixsecurity19/presentation/yang-hojoon

Index Terms

• Security and privacy

  • Formal methods and theory of security

    • Formal security models

  • Network security

    • Mobile and wireless security

    • Security protocols