More Web Proxy on the site http://driver.im/

research-article

Open access

Discovering emergency call pitfalls for cellular networks with formal methods

Authors:

Hai ZhouAuthors Info & Claims

MobiSys '21: Proceedings of the 19th Annual International Conference on Mobile Systems, Applications, and Services

Pages 296 - 309

https://doi.org/10.1145/3458864.3466625

Published: 24 June 2021 Publication History

All formats PDF

Abstract

Availability and security problems in cellular emergency call systems can cost people their lives, yet this topic has not been thoroughly researched. Based on our proposed Seed-Assisted Specification method, we start to investigate this topic by looking closely into one emergency call failure case in China. Using what we learned from the case as prior knowledge, we build a formal model of emergency call systems with proper granularity. By running model checking, four public-unaware scenarios where emergency calls cannot be correctly routed are discovered. Additionally, we extract configurations of two major U.S. carriers and incorporate them as model constraints into the model. Based on the augmented model, we find two new attacks leveraging the privileges of emergency calls. Finally, we present a solution with marginal overhead to resolve issues we can foresee.

References

[1]

3GPP. 2001. Formal Analysis of the 3G Authentication Protocol. Technical Report (TR) 33.902. 3rd Generation Partnership Project (3GPP). Version 4.0.0.

[2]

3GPP. 2019. Public Warning System (PWS) requirements. Technical Specification (TS) 22.268. 3rd Generation Partnership Project (3GPP). Version 16.3.0.

[3]

3GPP. 2020. Access to the 3GPP Evolved Packet Core (EPC) via non-3GPP access networks; Stage 3. Technical Specification (TS) 24.302. 3rd Generation Partnership Project (3GPP). Version 16.4.0.

[4]

3GPP. 2020. Characteristics of the Universal Subscriber Identity Module (USIM) application. Technical Specification (TS) 31.102. 3rd Generation Partnership Project (3GPP). Version 16.4.0.

[5]

3GPP. 2020. Evolved Universal Terrestrial Radio Access (E-UTRA); Radio Resource Control (RRC); Protocol specification. Technical Specification (TS) 36.331. 3rd Generation Partnership Project (3GPP). Version 16.1.1.

[6]

3GPP. 2020. IP Multimedia Subsystem (IMS) emergency sessions. Technical Specification (TS) 23.167. 3rd Generation Partnership Project (3GPP). Version 16.2.0.

[7]

3GPP. 2020. Mobile radio interface Layer 3 specification; Core network protocols; Stage 3. Technical Specification (TS) 24.008. 3rd Generation Partnership Project (3GPP). Version 16.5.0.

[8]

3GPP. 2020. Non-Access-Stratum (NAS) protocol for 5G System (5GS); Stage 3. Technical Specification (TS) 24.501. 3rd Generation Partnership Project (3GPP). Version 16.5.1.

[9]

3GPP. 2020. Non-Access-Stratum (NAS) protocol for Evolved Packet System (EPS); Stage 3. Technical Specification (TS) 24.301. 3rd Generation Partnership Project (3GPP). Version 16.5.1.

[10]

3GPP. 2020. Service aspects; Service principles. Technical Specification (TS) 22.101. 3rd Generation Partnership Project (3GPP). Version 17.2.0.

[11]

3GPP2. 2008. 3rd Generation Partnership Project 2. http://www.3gpp2.org.

[12]

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 SIGSAC Conference on Computer and Communications Security (CCS). ACM, 205--216.

Digital Library

[13]

David Basin, Cas Cremers, Jannik Dreier, and Ralf Sasse. 2017. Symbolically analyzing security protocols using tamarin. ACM SIGLOG News 4, 4 (2017), 19--30.

Digital Library

[14]

David Basin, Jannik Dreier, Lucca Hirschi, Saša 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). ACM, 1383--1396.

Digital Library

[15]

Bruno Blanchet. 2016. Modeling and verifying security protocols with the applied pi calculus and ProVerif. Foundations and Trends in Privacy and Security 1, 1--2 (2016), 1--135.

Digital Library

[16]

Elgin M Brunner and Manuel Suter. 2008. International CIIP handbook 2008/2009: An inventory of 25 national and 7 international critical information infrastructure protection policies. Center for Security Studies (CSS), ETH Zurich.

[17]

Cisco. 2016. MME Administration Guide, Emergency Bearer Services. https://www.cisco.com/c/en/us/td/docs/wireless/asr_5000/21-5_N5-8/MME/21-5-MME-Admin/21-5-MME-Admin_chapter_010010.html. Accessed on Jan. 5, 2021.

[18]

Cisco. 2016. MME Administration Guide, Local Emergency Numbers List. https://www.cisco.com/c/en/us/td/docs/wireless/asr_5000/21/MME/b_21_MME_Admin/b_21_MME_Admin_chapter_011111.pdf. Accessed on Jan. 5, 2021.

[19]

Piergiuseppe Bettassa Copet, Guido Marchetto, Riccardo Sisto, and Luciana Costa. 2017. Formal verification of LTE-UMTS and LTE-LTE handover procedures. Computer Standards & Interfaces 50 (2017), 92--106.

Digital Library

[20]

Cas Cremers and Martin Dehnel-Wild. 2019. Component-Based Formal Analysis of 5G-AKA: Channel Assumptions and Session Confusion. In Proceedings of the 26th Network and Distributed Systems Security (NDSS) Symposium.

[21]

Haotian Deng, Weicheng Wang, and Chunyi Peng. 2018. CEIVE: Combating Caller ID Spoofing on 4G Mobile Phones Via Callee-Only Inference and Verification. In Proceedings of the 24th Annual International Conference on Mobile Computing and Networking (MobiCom).

Digital Library

[22]

European Central Bank. 2004. Standards for Securities Clearing and Settlement in the European Union. Technical Report. CESR.

[23]

Federal Communications Commission, USA. 2002. Revision of the Commission's Rules to Ensure Compatibility with Enhanced 911 Emergency Calling Ssystems. 17 FCC Rcd 19012 (25).

[24]

Federal Communications Commission, USA. 2015. Wireless E911 Location Accuracy Requirements. 30 FCC Rcd 2990 (4).

[25]

Federal Communications Commission, USA. 2019. 800 MHz Cellular Service. https://www.fcc.gov/wireless/bureau-divisions/mobility-division/800-mhz-cellular-service. Accessed on Jan. 5, 2021.

[26]

Federal Communications Commission, USA. 2020. Caller ID Spoofing. https://www.fcc.gov/consumers/guides/spoofing-and-caller-id. Accessed on Jan. 5, 2021.

[27]

Nico Golde, Kévin Redon, and Jean-Pierre Seifert. 2013. Let me answer that for you: Exploiting broadcast information in cellular networks. In Presented as part of the 22nd USENIX Security Symposium (USENIX Security). 33--48.

[28]

Google. 2020. Android Open Source Project. https://source.android.com. Accessed on Jan. 5, 2021.

[29]

Mordechai Guri, Yisroel Mirsky, and Yuval Elovici. 2017. 9-1-1 DDoS: attacks, analysis and mitigation. In 2017 IEEE European Symposium on Security and Privacy (EuroS&P). IEEE, 218--232.

[30]

Lin Huang. 2016. LTE REDIRECTION: Forcing Targeted LTE Cellphone into Unsafe Network. In the 7th Annual HITB Security Conference (HITBSecConf). https://goo.gl/Y2FtG4

[31]

Huawei. 2019. CloudEC V600R019C00 Feature Guide, Emergency Call. https://support.huawei.com/enterprise/en/doc/EDOC1100059085/e0804ebc/emergency-call. Accessed on Jan. 5, 2021.

[32]

Syed Hussain, Omar Chowdhury, Shagufta Mehnaz, and Elisa Bertino. 2018. LTEInspector: A systematic approach for adversarial testing of 4G LTE. In Proceedings of the 25th Network and Distributed Systems Security (NDSS) Symposium.

[33]

Syed Rafiul Hussain, Mitziu Echeverria, Omar Chowdhury, Ninghui Li, and Elisa Bertino. 2019. Privacy Attacks to the 4G and 5G Cellular Paging Protocols Using Side Channel Information. In Proceedings of the 26th Network and Distributed Systems Security (NDSS) Symposium.

[34]

Syed Rafiul Hussain, Mitziu Echeverria, Imtiaz Karim, Omar Chowdhury, and Elisa Bertino. 2019. 5GReasoner: A Property-Directed Security and Privacy Analysis Framework for 5G Cellular Network Protocol. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (CCS). ACM, 669--684.

Digital Library

[35]

ITU-T. 1998. ISDN user-network interface layer 3 specification for basic call control. ITU-T Recommendation. International Telecommunication Union. Q.931.

[36]

Kakaku BBS. 2017. I cannot make emergency calls such as 110 (in Japanese). https://bbs.kakaku.com/bbs/J0000024343/SortID=21105988/. Accessed on Jan. 5, 2021.

[37]

Leslie Lamport. 2002. Specifying systems: the TLA+ language and tools for hardware and software engineers. Addison-Wesley Longman Publishing Co., Inc.

Digital Library

[38]

Gyuhong Lee, Jihoon Lee, Jinsung Lee, Youngbin Im, Max Hollingsworth, Eric Wustrow, Dirk Grunwald, and Sangtae Ha. 2019. This is Your President Speaking: Spoofing Alerts in 4G LTE Networks. In Proceedings of the 17th Annual International Conference on Mobile Systems, Applications, and Services (MobiSys). ACM, 404--416.

Digital Library

[39]

Chi-Yu Li, Guan-Hua Tu, Chunyi Peng, Zengwen Yuan, Yuanjie Li, Songwu Lu, and Xinbing Wang. 2015. Insecurity of voice solution VoLTE in LTE mobile networks. In Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security (CCS). ACM, 316--327.

Digital Library

[40]

Yuanjie Li, Chunyi Peng, Zengwen Yuan, Jiayao Li, Haotian Deng, and Tao Wang. 2016. Mobileinsight: Extracting and analyzing cellular network information on smartphones. In Proceedings of the 22nd Annual International Conference on Mobile Computing and Networking (MobiCom). 202--215.

Digital Library

[41]

MediaTek. 2014. MTK Catcher. https://www.finetopix.com/showthread.php/40844-MTK-Catcher. Accessed on Jan. 5, 2021.

[42]

Ministry of Industry and Information Technology, China. 2005. Technical requirement of routing and implementation for inter-network emergency call service. YD/T 1406-2005.

[43]

Ministry of Industry and Information Technology, China. 2011. Technical requirement and testing methods for general function of mobile telecommunication terminal. YD/T 2307-2011.

[44]

Nation Emergency Number Association. 2018. 9-1-1 Statistics. https://www.nena.org/page/911Statistics. Accessed on Jan. 5, 2021.

[45]

National Instruments, Ettus Research. 2020. Universal Software Radio Peripheral (USRP) B210 SDR Kit (70 MHz - 6GHz). https://www.ettus.com/all-products/UB210-KIT/.

[46]

Andreea Ancuta Onofrei, Yacine Rebahi, and Thomas Magedanz. 2010. Preventing Distributed Denial-of-Service Attacks on the IMS Emergency Services Support through Adaptive Firewall Pinholing. The International Journal of Next Generation Network (IJNGN) 2, 1 (2010).

[47]

OpenAirInterface Software Alliance. 2020. Openairinterface 5G Wireless Implementation. https://www.openairinterface.org/.

[48]

Peter Pi, XiLing Gong, and Gmxp. 2018. Exploring Qualcomm Baseband via ModKit. In CanSecWest conference.

[49]

Qualcomm. 2020. QUALCOMM eXtensible Diagnostic Monitor (QxDM). https://www.qualcomm.com/documents/qxdm-professional-qualcomm-extensible-diagnostic-monitor.

[50]

Yacine Rebahi, Andreea Ancuta Onofrei, and Thomas Magedanz. 2009. Security in the Emergency Services Support for the IP Multimedia Subsystem (IMS). 5th International Week on Management of Networks and Services, Venice, Italy (2009).

[51]

Red Pocket Mobile. 2020. Red Pocket Global Internet Data Plans. https://www.redpocket.com/global.

[52]

David Rupprecht, Katharina Kohls, Thorsten Holz, and Christina Pöpper. 2019. Breaking LTE on layer two. In Proceedings of the 2019 IEEE Symposium on Security & Privacy (S & P).

[53]

Takuro Sato, Daniel M Kammen, Bin Duan, Martin Macuha, Zhenyu Zhou, Jun Wu, Muhammad Tariq, and Solomon Abebe Asfaw. 2015. Smart grid standards: specifications, requirements, and technologies. John Wiley & Sons.

[54]

Altaf Shaik, Ravishankar Borgaonkar, N Asokan, Valtteri Niemi, and Jean-Pierre Seifert. 2016. Practical attacks against privacy and availability in 4G/LTE mobile communication systems. In Proceedings of the 23rd Annual Network and Distributed System Security (NDSS) Symposium.

[55]

Jaeseung Song, Hyoungshick Kim, and Athanasios Gkelias. 2014. iVisher: Real-Time Detection of Caller ID Spoofing. ETRI Journal 36, 5 (2014), 865--875.

[56]

Sprint. 2019. What this means to you after April 30, 2019. https://www.sprint.com/en/support/account/oma-slot.html. Accessed on Jan. 5, 2021.

[57]

T. Taylor, H. Tschofenig, H. Schulzrinne, and M. Shanmugam. 2008. Security Threats and Requirements for Emergency Call Marking and Mapping. RFC 5069. IETF.

[58]

THE PAPER. 2019. Father fell to the ground with cerebral haemorrhage, mother's mobile phone can not make emergency calls. Meizu said: possible a system problem (in Chinese). https://www.thepaper.cn/newsDetail_forward_3749664. Accessed on Jan. 5, 2021.

[59]

Guan-Hua Tu, Yuanjie Li, Chunyi Peng, Chi-Yu Li, and Songwu Lu. 2016. Detecting problematic control-plane protocol interactions in mobile networks. IEEE/ACM Transactions on Networking 24, 2 (2016), 1209--1222.

Digital Library

[60]

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.

Digital Library

[61]

Verizon Wireless. 2019. CDMA Network Retirement. https://www.verizonwireless.com/support/knowledge-base-218813/. Accessed on Jan. 5, 2021.

[62]

Bob Williams. 2008. Intelligent transport systems standards. Artech House.

[63]

Yinbo Yu, You Li, Kaiyu Hou, Yan Chen, Hai Zhou, and Jianfeng Yang. 2019. CellScope: Automatically Specifying and Verifying Cellular Network Protocols. In Proceedings of the ACM SIGCOMM 2019 Conference Posters and Demos. ACM, 21--23.

Digital Library

[64]

Yuan Yu, Panagiotis Manolios, and Leslie Lamport. 1999. Model checking TLA+ specifications. In Advanced Research Working Conference on Correct Hardware Design and Verification Methods. Springer, 54--66.

Digital Library

Cited By

Hu YChen MYan HCheng CTu GLi CXie TPeng CXiao LTang JGanesan DLane NShi W(2024)Uncovering Problematic Designs Hindering Ubiquitous Cellular Emergency Services AccessProceedings of the 30th Annual International Conference on Mobile Computing and Networking10.1145/3636534.3690704(1455-1469)Online publication date: 4-Dec-2024
https://dl.acm.org/doi/10.1145/3636534.3690704
Chen MHu YTu GLi CWang SShi JXie THsu RXiao LPeng CTan ZLu S(2024)Taming the Insecurity of Cellular Emergency Services (9–1-1): From Vulnerabilities to Secure DesignsIEEE/ACM Transactions on Networking10.1109/TNET.2024.337929232:4(3076-3091)Online publication date: Aug-2024
https://doi.org/10.1109/TNET.2024.3379292
Yakar EKilinc H(2024)Exploring the Impact of Big Data Analytics on Emergency Calls within Telecommunication SystemsProcedia Computer Science10.1016/j.procs.2024.06.021238(240-247)Online publication date: 2024
https://doi.org/10.1016/j.procs.2024.06.021
Show More Cited By

Index Terms

Discovering emergency call pitfalls for cellular networks with formal methods
1. Networks
  1. Network protocols
    1. Protocol correctness
      1. Formal specifications
      2. Protocol testing and verification
  2. Network types
    1. Mobile networks
2. Security and privacy
  1. Network security
    1. Mobile and wireless security

Recommendations

A Formal Framework for ASTRAL Intralevel Proof Obligations

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on how to formally prove the mathematical correctness of ASTRAL ...
A Synergistic Interweaving of Formal and Informal Methods
COMPSAC '03: Proceedings of the 27th Annual International Conference on Computer Software and Applications

In most studies of bridging between informal specifications,formal specifications are transformed frominformal specifications after completion of specificationof the whole system. Most of these formal specificationsare used for rigorous study of the ...
Formal methods: Importance, experience, and comparative analysis
Selected papers from the International Conference on Computer Science,Software Engineering, Information Technology, e-Business, and Applications, 2003

In this paper, we investigate the use of formal methods in the various phases of the life-cycle of developing communications protocols, software, and distributed systems. We identify important reasons and benefits for using formal methods. We also ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

MobiSys '21: Proceedings of the 19th Annual International Conference on Mobile Systems, Applications, and Services

June 2021

528 pages

ISBN:9781450384438

DOI:10.1145/3458864

General Chair:
Suman Banerjee
University of Wisconsin-Madison
,
Program Chairs:
Luca Mottola
Politecnico di Milano
,
Xia Zhou
Dartmouth College

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution-NonCommercial International 4.0 License.

Sponsors

SIGMOBILE: ACM Special Interest Group on Mobility of Systems, Users, Data and Computing

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 24 June 2021

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Conference

MobiSys '21

Sponsor:

SIGMOBILE

MobiSys '21: The 19th Annual International Conference on Mobile Systems, Applications, and Services

June 24 - July 2, 2021

Wisconsin, Virtual Event

Acceptance Rates

MobiSys '21 Paper Acceptance Rate 36 of 166 submissions, 22%;

Overall Acceptance Rate 274 of 1,679 submissions, 16%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
926
Total Downloads

Downloads (Last 12 months)265
Downloads (Last 6 weeks)18

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Hu YChen MYan HCheng CTu GLi CXie TPeng CXiao LTang JGanesan DLane NShi W(2024)Uncovering Problematic Designs Hindering Ubiquitous Cellular Emergency Services AccessProceedings of the 30th Annual International Conference on Mobile Computing and Networking10.1145/3636534.3690704(1455-1469)Online publication date: 4-Dec-2024
https://dl.acm.org/doi/10.1145/3636534.3690704
Chen MHu YTu GLi CWang SShi JXie THsu RXiao LPeng CTan ZLu S(2024)Taming the Insecurity of Cellular Emergency Services (9–1-1): From Vulnerabilities to Secure DesignsIEEE/ACM Transactions on Networking10.1109/TNET.2024.337929232:4(3076-3091)Online publication date: Aug-2024
https://doi.org/10.1109/TNET.2024.3379292
Yakar EKilinc H(2024)Exploring the Impact of Big Data Analytics on Emergency Calls within Telecommunication SystemsProcedia Computer Science10.1016/j.procs.2024.06.021238(240-247)Online publication date: 2024
https://doi.org/10.1016/j.procs.2024.06.021
Li YHou KHe YChen YZhou H(2024)Property Guided Secure Configuration Space SearchInformation Security10.1007/978-3-031-75764-8_8(140-160)Online publication date: 17-Oct-2024
https://doi.org/10.1007/978-3-031-75764-8_8
Wang XXu YLiu JWu GChen S(2023)Formal Modelling of the Multiple Trains Following Operation in Uncertain Environments2023 18th International Conference on Intelligent Systems and Knowledge Engineering (ISKE)10.1109/ISKE60036.2023.10481339(450-457)Online publication date: 17-Nov-2023
https://doi.org/10.1109/ISKE60036.2023.10481339
Zheke YJun NXurong LFangmeng Y(2023)Identify spatio-temporal properties of network traffic by model checkingThe Journal of Supercomputing10.1007/s11227-023-05388-979:16(18886-18909)Online publication date: 20-May-2023
https://dl.acm.org/doi/10.1007/s11227-023-05388-9

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

EPUB

View this article in ePub.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents