Discovering emergency call pitfalls for cellular networks with formal methods

Kaiyu Hou, You Li, Yinbo Yu, Yan Chen, Hai Zhou

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationMobiSys 2021 - Proceedings of the 19th Annual International Conference on Mobile Systems, Applications, and Services
PublisherAssociation for Computing Machinery, Inc
Pages296-309
Number of pages14
ISBN (Electronic)9781450384438
DOIs
StatePublished - Jun 24 2021
Event19th ACM International Conference on Mobile Systems, Applications, and Services, MobiSys 2021 - Virtual, Online, United States
Duration: Jun 24 2021Jul 2 2021

Publication series

NameMobiSys 2021 - Proceedings of the 19th Annual International Conference on Mobile Systems, Applications, and Services

Conference

Conference19th ACM International Conference on Mobile Systems, Applications, and Services, MobiSys 2021
Country/TerritoryUnited States
CityVirtual, Online
Period6/24/217/2/21

Keywords

  • cellular network protocol
  • emergency call
  • formal methods
  • protocol formal verification
  • protocol specification

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Computer Science Applications

Fingerprint

Dive into the research topics of 'Discovering emergency call pitfalls for cellular networks with formal methods'. Together they form a unique fingerprint.

Cite this