Control-Plane Protocol Verification in 4G/3G Cellular Networks

WiNG Lab @ UCLA ; MSSN Lab @ Purdue




What's New


Research Overview

This project investigates the control-plane design and operations of 3G/4G cellular networks. For a given networked system, its control-plane design largely stipulates its reliability, performance, function correctness and security. There is no exception for cellular networks. The control-plane protocols in 3G/4G mobile networks communicate with each other, and provide a rich set of control utilities, such as radio resource control, mobility support, connectivity management, to name a few. However, the problem of verifying the correctness of control-plane protocols in 3G/4G mobile networks remains largely unaddressed to date. In this project, we seek to design software tools for such protocol verifications, identify the problematic control-plane designs and operations, quantify their real-world impacts, and infer their root causes.


Research Progress

Debugging Control-Plane Protocols via Domain-Specific Protocol Verification  (SIGCOMM'14, TON'15)

We have designed and implemented CNetVerifier, a domain-specific model checking tool for control-plane diagnosis in cellular networks.  The goal is to uncover design flaws, as well as operational slips. It works through two-phase diagnosis procedures. During the first phase of screening, we follow standards specifications to model each control-plane protocol as finite-state machines, running at the mobile device and the network infrastructure. We further define common usage scenarios  by considering factors of mobility, access and traffic demand.  Given a set of desirable properties, we can identify candidate instances that violate such properties in the given scenario.  During the second phase for (in)validation, such potential instances are further (in)validated at the operational network. It is done via a phone-based validation method we have devised. This way, we are able to circumvent the closed infrastructure via protocol modeling and phone-based experiments. 

    • Our study so far yields new findings on protocol correctness. We discovered two new classes of problematic interactions among signaling protocols: (1) necessary but problematic cooperation, and (2) independent but coupled operations. They also result in user-perceived performance penalties in the form of temporary out of service, long call setup time, stuck in an old network. We further propose new designs via layer extension, domain separation, and cross-system coordination to fix such instances.

  • Category Instances Type Protocols Dimensions Root Causes
    Necessary but problematic cooperations S1: User device is temporarily ?out-of-service? during 3G-to-4G switching. Design SM/ESM, GMM/EMM Cross-system (3G, 4G) Cross-system states are shared but unprotected between 3G and 4G; States are deleted during inter-system switching.
    S2: User device is temporarily ?out-of-service? during the attach procedure. Design EMM, 4G-RRC Cross-layer MME assumes reliable transfer of signals by RRC; RRC cannot ensure it.
    S3: User device gets stuck in 3G. Design 3G-RRC, CM, SM Cross-domain; Cross-system RRC state change policy is inconsistent for intersystem switching.
    Independent but coupled operations S4: Outgoing call/Internet access is delayed. Design CM/MM, SM/GMM Cross-layer Location update does not need to be, but is served with higher priority than outgoing call/data requests.
    S5: PS rate declines (e.g., 96.1% in US-II) during ongoing CS service. Operation 3G-RRC, CM, SM Cross-domain 3G-RRC configures the shared channel with a single modulation scheme for both data and voice.
    S6: User device is temporarily ?out-of-service? after 3G?4G switching. Operation MM, EMM Cross-system Information and action on location update failure in 3G are exposed to 4G.



  • Improper Interplays of Control-Plane Operations for Voice Calls and Data Access (MobiCom'13)

    In 4G LTE networks, both voice calls and data access are killer network services. As the LTE network migrates towards an all IP based, packet-switched (PS) design by following the Internet paradigm, providing mobile data access is readily achieved. However, offering carrier-grade voice services with guaranteed performance becomes less obvious.  The 4G LTE network uses two voice solutions. One is VoLTE, which is based on packet-switched (PS) Internet voice, and the other is CSFB (CS Fallback,  which uses the legacy voice solution in 3G networks and switches a 4G user back to 3G to access circuit-switched voice services). In this study, we examine how voice calls via CSFB affect data service in 4G LTE networks. To our surprise, we found that voice calls and data access interfere with each other.  On one hand, voice calls may incur throughput drop (up to 83.4%), transmission halt for seconds, lost 4G connectivity, and application aborts for data sessions. One the other hand, users may miss incoming calls upon turning on data access. It turns out that, though the 3G and 4G systems are designed and operated independently, they do interact with each other via the mobile phone, which runs dual protocol stacks. Improper design of protocols lead to unexpected interference that results in deadlocks and loops in the protocol finite-state operations.   


    • Publications

      • [1] How Voice Calls Affect Data in Operational LTE Networks,
        Guan-Hua Tu, Chunyi Peng, Hongyi Wang, Chi-Yu Li, Songwu Lu,
        MobiCom'13, Miami, Florida, Sep. 2013. [PDF] [slide]

      • [2] Control-Plane Protocol Interactions in Cellular Networks,
        Guan-Hua Tu, Yuanjie Li, Chunyi Peng, Chi-Yu Li, Hongyi Wang, Songwu Lu,
        SIGCOMM'14, Chicago, Illinois, Aug. 2014. [PDF]. [slide]

      • [3] Detecting Problematic Control-Plane Protocol Interactions in Mobile Networks
        Guan-Hua Tu, Yuanjie Li, Chunyi Peng, Chiyu Li, Songwu Lu,
        IEEE Transactions on Networking (TON), Vol. 24, No. 2, pp: 1209-1222, April 2016. [PDF]

      • [4] A First Look at Unstable Mobility Management in Cellular Networks
        Yuanjie Li, Jiaqi Xu, Chunyi Peng, Songwu Lu,
        (HotMobile'16 ), Florida, Feb 2016. [PDF] [Slide]

      • [5] iCellular: Define Your Own Cellular Network Access on Commodity Smartphones
        Yuanjie Li, Haotian Deng, Chunyi Peng, Guan-Hua Tu, Jiayao Li, Zengwen Yuan, Songwu Lu
        (NSDI'16 ), Santa Clara, CA, March 2016. [PDF] [Slide] [More details]

      • [6] Understanding and Diagnosing Real-World Femtocell Performance Problems
        Chunyi Peng, Yuanjie Li, Zhuoran Li, Jie Zhao and Jiaqi Xu
        (INFOCOM'16 ), San Francisco, CA, April 2016. [PDF] [Slide]

      • [7] Instability in Distributed Mobility Management: Revisiting Configuration Management in 3G/4G Mobile Networks
        Yuanjie Li, Haotian Deng, Jiayao Li, Chunyi Peng and Songwu Lu,
        (SIGMETRICS'16), Antibes Juan-Les-Pins, France, June 2016.

      • [8] Demystify Undesired Handoff in Cellular Networks
        Chunyi Peng and Yuanjie Li
        (ICCCN'16), Hawaii, Aug 2016. [PDF] [Slide]

      • [9] CAP on Mobility Control for 4G LTE Networks (Invited Paper)
        Yuanjie Li, Zengwen Yuan, Chunyi Peng and Songwu Lu
        (Hotwireless'16), New York, USA, Oct. 2016. [PDF]

      • [10] MobileInsight: Extracting and Analyzing Cellular Network Information on Smartphones
        Yuanjie Li, Chunyi Peng, Zengwen Yuan, Jiayao Li, Haotian Deng and Tao Wang
        (MobiCom'16), New York, USA, Oct. 2016. [PDF] (Best Community Paper Award )

      • [11] Towards Automated Intelligence in 5G Systems
        Haotian Deng, Qianru Li, Yuanjie Li, Songwu Lu, Chunyi Peng, Taqi Raza,Zhaowei Tan, Zengwen Yuan, Zhehui Zhang (alphabetical order) (ICCCN'17) (Invited Paper), 2017. [PDF]

      • [12] A Machine Learning Based Approach to Mobile Network Analysis
        Zengwen Yuan, Yuanjie Li, Chunyi Peng, Songwu Lu, Haotian Deng, Zhaowei Tan and Taqi Raza (ICCCN'18) (Invited Paper), 2017. [PDF]

      • [13] Resolving Policy Conflicts in Multi-Carrier Cellular Access
        Zengwen Yuan, Qianru Li, Yuanjie Li, Songwu Lu, Chunyi Peng, and George Varghese
        (MobiCom'18), 2018. [PDF]


      Team Members

      • Songwu Lu (Faculty, UCLA)
      • Chunyi Peng (Faculty, Purdue)
      • Chi-Yu Li (Postdoctoc (2014-2015), UCLA)
      • Guan-Hua Tu (PhD (2015), Postdoc (2015-2016), UCLA)
      • Yuanjie Li (PhD (2017), Postdoc (2017-2018), UCLA)
      • Haotian Deng (PhD Student, Purdue)

      Acknowledgement

      We gratefully acknowledge research support from NSF under grants CNS-1421440 (--> CNS-1748630) and CNS-1423576, as well as the departmental support from Purdue and OSU.


      Copyright © 2015 - 2019, MSSN Lab, Purdue.
      Copyright © 2015 - 2018, WiNG Lab, UCLA.
      All rights reserved.

      Updated on Sep 1, 2019.