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.
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. |
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.
Copyright © 2015 - 2019, MSSN Lab, Purdue. Copyright © 2015 - 2018, WiNG Lab, UCLA. All rights reserved. Updated on Sep 1, 2019.