TY - GEN
T1 - Discovering emergency call pitfalls for cellular networks with formal methods
AU - Hou, Kaiyu
AU - Li, You
AU - Yu, Yinbo
AU - Chen, Yan
AU - Zhou, Hai
N1 - Publisher Copyright:
© 2021 Owner/Author.
PY - 2021/6/24
Y1 - 2021/6/24
N2 - 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.
AB - 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.
KW - cellular network protocol
KW - emergency call
KW - formal methods
KW - protocol formal verification
KW - protocol specification
UR - http://www.scopus.com/inward/record.url?scp=85110137271&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85110137271&partnerID=8YFLogxK
U2 - 10.1145/3458864.3466625
DO - 10.1145/3458864.3466625
M3 - Conference contribution
AN - SCOPUS:85110137271
T3 - MobiSys 2021 - Proceedings of the 19th Annual International Conference on Mobile Systems, Applications, and Services
SP - 296
EP - 309
BT - MobiSys 2021 - Proceedings of the 19th Annual International Conference on Mobile Systems, Applications, and Services
PB - Association for Computing Machinery, Inc
T2 - 19th ACM International Conference on Mobile Systems, Applications, and Services, MobiSys 2021
Y2 - 24 June 2021 through 2 July 2021
ER -