RRCshort=RRC,long=Radio Resource Control ZMQshort=ZMQ,long=ZeroMQ
LSTMshort=LSTM,long=Long Short-Term Memory LALshort=LAL,long=Listen-and-Learn
TSshort=TS,long=Technical Specifications NRshort=NR,long=New Radio
eMBBshort=eMBB,long=enhancing Mobile Broadband mMTCshort=mMTC,long=massive
Machine Type Communications O-RANshort=O-RAN,long=Open Radio Access Network
NASshort=NAS,long=Non-Access Stratum ASshort=AS,long=Access Stratum
UEshort=UE,long=User Equipment MITMshort=MITM,long=man-in-the-middle
OTAshort=OTA,long=over-the-air CNshort=CN,long=core network
gNBshort=gNB,long=gNodeB DoSshort=DoS,long=Deny of Service
BSshort=BS,long=Base Station NSAshort=NSA,long=Non Standard-Alone
SAshort=SA,long=Standard-Alone EPSshort=EPS,long=Evolved Packet System
eNBshort=eNB,long=evolved NodeBs AKAshort=AKA,long=authentication and key
agreement EC-AKAshort=EC-AKA,long=Ensured confidentiality Authentication and
Key agreement ASMEshort=ASME,long=Access Security Management Entity
UPshort=UP,long=User Plane KDFshort=KDF,long=key derivation function
IMSIshort=IMSI,long=international mobile subscriber identity
S-TMSIshort=S-TMSI,long=SAE Temporary Mobile Subscriber Identity

# Formal-Guided Fuzz Testing: Targeting Security Assurance from Specification
to Implementation for 5G and Beyond

Jingda Yang, Student Member, IEEE, Sudhanshu Arya, Member, IEEE, and Ying
Wang, Member, IEEE J. Yang, S. Arya, and Y. Wang are with the School of
Systems and Enterprises, Stevens Institute of Technology, Hoboken, NJ, USA
07030. The corresponding author is Y. Wang (ywang6@stevens.edu). This effort
was sponsored by the Defense Advanced Research Project Agency (DARPA) under
grant no. D22AP00144.

###### Abstract

Softwarization and virtualization in 5G and beyond necessitate thorough
testing to ensure the security of critical infrastructure and networks,
requiring the identification of vulnerabilities and unintended emergent
behaviors from protocol designs to their software stack implementation. Formal
methods demonstrate efficiency in abstracting specification models at the
protocol level, while fuzz testing provides comprehensive experimental
evaluations of system implementations. However, the state of art formal and
fuzz testing are both labor-intensive or computationally complex. To provide
an efficient and comprehensive solution, we propose a novel and first-of-its-
kind approach that connects the strengths and coverage of formal and fuzzing
methods to efficiently detect vulnerabilities across protocol logic and
implementation stacks in a hierarchical manner. We design and implement formal
verification to detect attack traces in critical protocols, which are used to
guide subsequent fuzz testing and incorporate feedback from fuzz testing to
broaden the scope of formal verification. This innovative approach
significantly improves efficiency and enables the auto-discovery of
vulnerabilities and unintended emergent behaviors from the 3GPP protocols to
software stacks. In this paper, we demonstrate this approach to the 5G Non-
Stand-Alone (NSA) security processes, which have more complicated designs and
higher risks due to the compatibility requirement to legacy and exiting 4G
networks compared to 5G Stand-Alone (SA) processes, with a focus on the Radio
Resource Control (RRC), Non-access Stratum (NAS) and Access Stratum (AS)
authentication process. Through formal analysis, we identify protocol-level
vulnerabilities related to user credentials disclosure and man-in-the-middle
(MITM) attack. Subsequently, we employ bit-level fuzzing to assess the
potential impacts and risks of identifier variation susceptible to integrity
vulnerabilities, followed by command-level mutation-based fuzzing, assuming
fixed identifier values, to evaluate the potential impacts and risks
associated with confidentiality vulnerabilities. Following this approach, we
discover one identifier leakage model, one DoS attack model, and two eavesdrop
attack models due to the absence of rudimentary MITM protection within the
protocol, despite the existence of a Transport Layer Security (TLS) solution
to this issue for over a decade. More remarkably, guided by the identified
formal analysis and attack models, we exploit $61$ vulnerabilities using fuzz
testing demonstrated on srsRAN platforms. These identified vulnerabilities
contribute to fortifying protocol-level assumptions and refining the search
space. Compared to state-of-the-art fuzz testing, our united formal and
fuzzing methodology enables auto-assurance by systematically discovering
vulnerabilities. It significantly reduces computational complexity,
transforming the non-practical exponential growth in computational cost into
linear growth. Our formal-guided fuzz testing system provides a robust and
self-reinforcing solution to the scalability challenges that often arise when
detecting vulnerabilities and unintended emergent behaviors in intricate,
large-scale 5G systems and their deployments in critical infrastructures and
verticals.

###### Index Terms:

NSA 5G, Formal Methods, Fuzz Testing, Self-reinforcing Solution,
Specifications

##  I Introduction

Verticals in 5G and next-generation infrastructure create a diverse and
intricate environment consisting of software, hardware, configurations,
instruments, data, users, and various stakeholders [1]. With system complexity
and its lack of security emphasis by domain scientists, the formed ecosystem
requires a comprehensive evaluation and validation for improved research and
transitional Critical Infrastructure (CI) security posture [2].

Despite two major state-of-the-art approaches, formal verification and fuzz
testing, being proposed to detect various vulnerabilities and unintended
emergent behaviors of the 5G network, limitations in large-scale systems and
stacks still exist. Formal verification can provide a high-level concept of
protocol and logical proof of security and vulnerability [3]. In contrast,
fuzz testing can offer a detailed and comprehensive experimental platform,
detecting potential vulnerabilities in the 5G code implementation platform
[4]. However, open issues and challenges of pick-and-choose fuzz testing and
formal analysis in various scenarios still exist [5, 6].

By unifying the fuzz testing with the formal analysis, it becomes possible to
initiate a reciprocal cycle between the two approaches, leading to the
identification of vulnerabilities across the entire search space. Formal
verification can offer valuable guidance and assumptions to fuzz testing,
while fuzz testing can broaden the scope of formal verification. The
unification should be complementary and enable mutual amplification. As a
result, vulnerability and unintended emergent behavior detection could be
extended with scalability when amplification occurs. With an objective to
improve the scalability, we propose an innovative heuristic approach by
integrating fuzz testing with formal analysis. The proposed technique
overcomes the limitations of the fuzz testing and the formal analysis and
thereby enables the model checkers to detect a wide range of vulnerabilities
in large complex 5G systems.

In the subsequent sections of this paper, we provide a concise overview of the
structure of our proposed comprehensive formal verification and fuzz testing
integrated vulnerability detection framework (Section III). Subsequently, we
elucidate the mechanism behind our proposed dependency-based protocol
abstraction and evaluation approach (Section IV), followed by presenting
examples of dependency analysis (Section IV-D). Furthermore, we apply the
dependency-based protocol abstraction and evaluation approach to the NSA 5G
communication establishment process (Section IV-A), where we present and
analyze the results of formal verification (Section V). Additionally, we
propose proven or novel solutions for each detected formal attack model.
Subsequently, leveraging the identified assumptions, we apply our proposed
fuzz testing framework to verify and analyze the implementation of the NSA 5G
communication establishment process (Section VII). Lastly, in Section IX, we
utilize intuitive visualizations to analyze the efficiency of different
fuzzing strategies across various fuzzing scopes.

##  II Related Work and Background

5G technologies are of rapidly increasing importance to the national and
regional infrastructure and offer unprecedented connectivity benefits.
However, these technologies also present an attack surface of unprecedented
size due to the complexity of both specifications and implementations of 5G
stacks. Previous researchers proposed vulnerability detection approaches[3, 7,
8], among which two categories have been intensively researched: formal
verification and fuzz testing.

Formal verification is the technology that transfers natural language-defined
protocols into symbolic logic language, which is feasible to establish the
validity of the given proposition through a finite process of mathematical
verification. Several formal analysis frameworks in the existing research are
proposed to determine which security guarantees are satisfied in 5G protocols
by applying formal methods and automated verification in the symbolic model,
like Tamarin[9], and 5G reasoner[10]. Hussian[3] et al. even proposed a cross-
layer formal verification framework, which combines model checkers and
cryptographic protocol verifies through the application of the abstraction-
refinement principle. Besides formal verification frameworks, different formal
strategies are introduced to prove the security assumption set, like [11]. For
example, the pre-authentication message sent unencrypted has been acknowledged
as the root cause of many known LTE and 5G protocol exploits[12, 13, 14].
Furthermore, Some registration and access control protocols, including AKA,
RRC, etc. have been applied formal methods in various framework[15, 10, 3].
When applied in the 5G security design, necessary lemmas are verified helping
lemmas, sanity-check lemmas, and the lemmas that check the relevant security
properties against the 5G protocols[15].

A Fuzz tester (or fuzzer) is a tool that iteratively and randomly generates
inputs to test the quality of a target program[16]. Compared to formal
analysis, fuzz testing has proved to be successful in discovering critical
security bugs in real software[16]. For example, [17] implemented a RRC fuzz
testing experiment for air interface protocols. Significant effort has been
devoted to devising new fuzzing techniques, strategies, and algorithms. Fuzz
testing has been used intensively for large-scale system cybersecurity
purposes, and multi-strategies are proposed to detect cyber vulnerabilities
efficiently. He et al. [18] proposed a state transition fuzzing framework that
can be applied to different types of message identifiers. To eliminate the
randomness and blindness of fuzzing, [19] introduced a vulnerability-oriented
fuzz (VulFuzz) testing framework to prioritize the fuzzing cases by security
vulnerability metrics.

Even though fuzz testing can detect more emergent and unexpected behaviors
than formal verification with less additional manual intervention, formal
verification is much more efficient than fuzz testing with manually
generalized representative mathematical expression. Leveraging the advantages
of formal verification and fuzz testing has become a popular topic. In [20],
extreme cases like buffer overflow or incorrect format are discussed, combined
with the advantages of protocol and mutation. Besides the extreme case, rule-
based fuzzing [21] focuses on covering all protocol-based cases. Under the
limited directions defined by formal verification, coverage-guided fuzz [22]
was proposed to test the security of cyber-physical systems. Furthermore, the
state-of-art vulnerability detection approach [23] proposed a possible
combination of formal verification and fuzz testing. When extended to the
long-time multi-time attacks, Ma et al. [24] proposed a state transaction
method to analyze serial attacks. Based on the formal verification, fuzz
testing can efficiently locate the high-risk area. However, there are still
significant gaps in highly relying on pre-assumptions of prior knowledge
awareness and focusing on the specific implementation of the targeted
protocols. Therefore, LZfuzz [25] was proposed to eliminate the requirements
for access to well-documented protocols and implementations while focusing on
plain-text fuzzing. And Osborne [26] et al. proposed a framework that can
apply fuzz testing with area limitations in real-world experiments to narrow
the fuzzing area. To address the challenges of computation power, without pre-
assuming to, but leveraging on the available prior domain knowledge, we
presented a multiple dimension multi-layer protocol-independent fuzzing
framework in [27], aiming for protocol vulnerabilities detection and
unintended emergent behaviors in fast-evolving 5G and NextG specifications and
large-scale open programmable 5G stacks. However, these manual formal guided
fuzz testing can not be automatically applied to detect cyber security
vulnerabilities. In this paper, our proposed framework generates a positive
feedback loop between formal verification and fuzz testing.

###  II-A Motivation

Although fuzzing is a fast technique to detect vulnerabilities and flaws, it
comes with the limitations of poor coverage which involves missing many errors
and thereby limits the performance of the security vulnerabilities testing.
Whereas, in formal verification methods, despite the use of abstract
mathematical representations of a system under test to verify or detect the
specified flaws or vulnerabilities in 5G systems, these methods inherently
suffer from scalability limitations. These limitations restrict their ability
to perform in more complicated and ever-larger systems due to the exponential
growth of the state space with the size of the system. This limitation puts
large complex systems out of the reach of the model checkers.

Aiming for security, usability, and reliability, the objective of this system
is to improve security assurance and resilience at both specification and
implementations levels by discovering and mitigating vulnerabilities and
unintended emergent behaviors with sufficient automation, scalability, and
usability. The presented approach could be applied to various fifth-generation
(5G) open programmable platforms[28, 29, 30] or other cognitivesoftware
defined communication systems[31].

###  II-B Contributions

In this paper, we propose a novel approach that connects the strengths and
coverage of formal and fuzzing methods to efficiently detect vulnerabilities
across protocol logic and implementation stacks in a hierarchical manner. The
main contributions are listed below.

  * $\bullet$

We design and implement formal verification for 5G authentication and
authorization specifications to detect attack traces and form attack models,
which are used to guide subsequent fuzz testing and incorporate feedback from
fuzz testing to broaden the scope of formal verification.

  * $\bullet$

We perform fundamental research towards the united and amplification of formal
method and fuzz testing targeting large-scale system assurance, which could
benefit the interdisciplinary research community in Program Languages and
Infrastructure Cybersecurity.

  * $\bullet$

We present a proof of concept system that increases the efficiency and enables
the auto-discovery of vulnerabilities and unintended emergent behaviors in 5G
specifications to software stacks, and illustrated the applicability and
extendability to a variety of specifications and implementations via a seven
steps United Formal&Fuzz Systematic Framework (UFSF).

  * $\bullet$

Our novel approach of protocol abstraction converts the natural language-based
specifications into non-ambiguous symbolic expressions, from which formal
analysis models could be auto-derived. It releases the formal analysis from
the labor-expertise-intensive process and leads toward the auto-formal
verification. A proof of concept is performed on the NSA 5G authentication
process by converting informal protocols into a dependency table, enabling
formal analysis that detects attack traces, thereby discovering $4$ attack
models.

  * $\bullet$

By leveraging UFSF from formal verification, our integrated solution of formal
guided fuzz testing further employs command-level and bit-level strategies to
detect exploitable vulnerabilities and unintended emergent behaviors
effectively. We successfully establish a connection among specification,
implemented systems, and real-life attack models, perform a thorough
examination of the complicated 5G NSA authentication and authorization
process, and exploit $53$ vulnerabilities demonstrated on srsRAN platforms.

  * $\bullet$

Unlike the state-of-the-art by-piece vulnerability detection, the presented
systematic vulnerability detection addressed the foundations for achieving
assurance for Future G authentication and authorization in providing the
panoramic vision and examination of the to-date 5G specifications.

##  III System Overview

Aiming at providing auto-assurance for 5G and beyond specifications to stack
implementations, we present a s vulnerability and unintended emergent
behaviors detection system. As shown in Fig. 1, The presetned system leverages
the amplification and cross-validation of fuzz testing and formal
verification. Our proposed framework builds up a virtuous recursive loop of
the following steps:

  1. 1.

Protocol Abstraction: Starting from the 3GPP technical specifications (TS) and
requirements (TR), we first convert the natural language-based specifications
into unambiguous symbolic expressions known as an authentication and
authorization flow-graph (AAF). We then further transform this flow-graph into
a properties table and generate a dependency graph. The dependency graph
serves as a foundation for deriving formal analysis models automatically. This
approach liberates the formal analysis process from labor-intensive and
expertise-dependent tasks, facilitating auto-formal verification. It also
enables incremental evolving verification by incorporating new 3GPP protocol
releases into existing formal methods, eliminating the need to start the
protocol abstraction process from scratch with each release.

  2. 2.

Formal-based Vulnerability Detection and Attack Models: With the dependancy
graph, we apply formal method via the ProVerif platform to conduct a logical
proof of security properties and potential vulnerabilities, facilitating a
robust and comprehensive evaluation of the system’s security integrity. The
formal method applied in the abstract protocols not only detect the
vulnerabilities in protocol design, also provide a space isolation to guide
fuzz testing.

  3. 3.

Search Space Isolation: The output of formal verification divides the search
space into three sets: no vulnerabilities, attack trace detected, and
uncertain areas that need further investigation. The division of the search
space effectively narrows down the uncertain regions and enables the guidance
and direction of fuzz testing.

  4. 4.

Formal Guided Fuzz Testing: With the detected attack models from formal
analysis, we direct and generate a list of fuzz testing. Compared to formal
analysis on the specifications, the initiated fuzz testing is performed on
runtime binary systems, focusing particularly on the predefined uncertain
areas and areas of identified attack traces. The guided fuzz testing is
deployed to identify runtime vulnerabilities, thereby complementing the
detection of vulnerabilities through logical proofs on protocols and assessing
the impact of the formal detected attack models and traces. Further, it also
functions as a stochastic approach for those uncertain areas that cannot be
verified through formal methods.

  5. 5.

Fortification of Protocol and Formal Verification : Based on the
vulnerabilities and unintended emergent behaviors detected by formal methods
and guided fuzz testing, we derive the solutions and fortifications to either
directly enhance the protocol’s robustness and resilience or narrow down
search spaces. By defining the space more precisely, formal verification can
be further optimized, consequently extending the scope of the security
assurance area.

We further demonstrate the proposed framework by leveraging our existing
platform of the fuzz testing-based digital twin [32, 33, 27] for 5G
cybersecurity, as illustrated in Fig. 2. Both OTA and zeroMQ modes in
legitimate communications are performed leveraging srsRAN. Interfacing with
our digital twin platform, we enable mutation-based identifiers fuzzing (Bit-
Level Fuzz Testing) and permutation-based command fuzzing (Command-Level Fuzz
Testing) that could be used for implementation-level verification, formal
discovery extension, and searching space triggering guided from the formal
method results. . With the utilization of formal result analysis, formal
guided fuzz testing, and the fortification, our proposed framework constructs
a reinforcing loop to enhance the system’s resilience

Figure 1: System Components and Connector View Figure 2: Experimental Platform
Structure and Setup[27]

##  IV Protocol Abstraction

###  IV-A Protocol and Symbolic Conversion for Formal Analysis

NSA 5G architecture can be divided into the legacy LTE authentication process
and LTE-to-5G connection reconfiguration. Compared to SA 5G network
architecture, NSA 5G architecture is more widely adopted but more vulnerable
because cross-generation of protocols introduces the vulnerabilities from LTE.
Therefore, we focus on the pre-authentication process of LTE in NSA 5G
architecture. As shown in Fig. 3, the LTE authentication in NSA architecture
can be divided into the following four parts:

Figure 3: NSA and AS Authentication and Authorization Flowgraph.

  1. 1.

RRC Connection Setup: RRC connection setup process aims to build up
connections in RRC layer. First, UE sends the RRC Connection Request command
with UE-identity and establishment cause to gNB. Then, gNB replays with radio
resource configuration to UE. If the setup process is valid, UE will send RRC
Connection Setup Complete command with necessary identifiers to gNB and
prepare for the following NAS security setup. In the RRC connection setup
process, we verify the reliability, consistency, and stability of
communications between UE and gNB. Confidentiality will not be considered
because the RRC connection setup process is designed for a non-encrypted
environment.

  2. 2.

Mutual Authentication: UE and CN adapt EPS AKA algorithm as encryption and
decryption tools to set up mutual authentication. In our designed formal EPS
algorithm, there are four required identifiers to get the corresponding
values, $AUTN$, $RES$, and $K_{ASME}$. Even if we assume the EPS algorithm is
impregnable, the previous messages containing IMSI and temporarily generated
$rand\\_id$ are neither ciphered nor integrity protected. The unencrypted
mutual authentication process is vulnerable to disclosing the user identity
under MITM attacks. Based on exploited vulnerabilities and properties, we test
the security impact of user identity by formal verification and simulate the
MITM attack mode.

  3. 3.

NAS Security Setup: After mutual authentication, CN needs to decide encryption
algorithm and integrity algorithm. To ensure the security of NAS communication
setup, UE and CN communicate with integrity protection to decide encryption
and integrity algorithm, and $K_{ASME}$, which is the top-level key to be used
in the access network. Then UE and CN can get the corresponding session key
for encryption and integrity of following symmetric NAS communication.

  4. 4.

AS Security Setup: NAS security setup shares $K_{ASME}$ between CN and UE.
However, there is still necessary to establish another channel for user status
management, like RRC. Therefore, CN generates a key $K_{eNB}$ for gNB based on
$K_{ASME}$ and NAS up-link count and forward the $K_{eNB}$ to eNB through the
private network. Same with NAS security setup, eNB and UE share the $K_{eNB}$
and selected encryption and integrity algorithm with integrity-protected
communications. Then eNB and UE use the generated RRC encryption key,
$K_{RRCenc}$, integrity key, $K_{RRCint}$, and generated UP encryption key,
$K_{UPenc}$, to establish symmetric ciphered and integrity protected RRC and
UP communication.

###  IV-B Properties Definition and Extraction

Following the Flowgraph shown in Fig.3, we further extract four major security
properties, confidentiality, integrity, authentication, and accounting, from
the 3GPP specifications that are critical in the Formal Analysis. These four
properties represent four aspects of security enhancement in the
specifications:

  1. 1.

Confidentiality represents the ability to prevent private information from
leakage.

  2. 2.

Integrity denotes the capability to keep the information unmodified.

  3. 3.

Authentication means whether the receiver can identify who and when to send
the message.

  4. 4.

Accounting is identifying whether the current message follows the right order
in session.

According to the four security properties, we generate an identifier-based
Properties Table (PT) in Fig. I to show the reflect the specification in the
control messages. The value in the security property columns represents which
identifier the current identifier depends on (N means None identifier). From
Fig. I Note 1, we conclude that RRC connection setup process which includes
three steps are unprotected in regarding confidentiality, Integrity,
Authentication and Accounting. For identifiers that are protected in some
properties, we check the critical keywordsidentifiers in each propriety. The
properties of the critical keywordsidentifiers become the assumptions of that
property examination. For instance as shown in Note 2 of Fig.I, the integrity
of $AUTN_{HSS}$ with the assumption of safe rand number (RAND) or the
assumption of leaked RAND.

The content of the Properties Table serves as the input assumption and
properties in the following formal analysis. From the table, it can be
observed that there exists the dependency between rows. That dependency
determines the flow-graph for each formal model for vulnerability detection.

TABLE I: Properties Table of Protocol Figure 4: Dependency Graph of Protocol

###  IV-C Dependency Graph Generation

To further visualize the dependency existed in the Properties Table, we
generate a Dependency Graph(DG) in Fig. 4. From the Dependency Graph, we can
extract the dependency trace of identifiers to evaluate the chain effects
along the dependency relationships and assess multi-level security risk. For
example as also shown in Note3 of Fig.I, $K_{NASenc}$ have a higher integrity
security level than $NAS$-$MAC$, because the integrity of $K_{NASenc}$ is
protected by $NAS\;Ciphering\;Algorithm$, $NAS\;\\\ Integrity\;Algorithm$ and
$KSI_{AMSE}$, which are protected by $K_{NASint}$, but the integrity of $NAS-
MAC$ is only protected by $K_{NASint}$. Based on the security risk level, we
first prove the vulnerabilities of the low-risk identifiers and then prove the
security of high-risk identifiers based on the proven assumptions of low-risk
identifiers. Following the security, propriety tracks provide the guidance of
the test target, which narrows the target range and improves the efficiency of
formal and fuzz testing.

Our security level evaluation system follows the Depth-first search (DFS)
principle, and inherent the security level from the parent node (dependency
node). For example, shown in Alg.1, the recursive algorithm adds the security
level of dependent property to their security level vector. Based on different
consideration and application scenarios, we use the Hadamard product of weight
vector and security level vector in Equation 1 to represent the global
security level. For example, we can set weight vector as $[1,1,0.5,0.5]$ if we
care more about confidentiality and integrity.

Data: $r$ = Boolean vector of dependency relation.

1:Security_Evaluation(node_$v$)

2:[c, i, au, ac] = $[1,1,1,1]$

3:while no dependent node $v^{\prime}$ exists do

4: [c, i, au, ac] += Security_Evaluation($v^{\prime}$) $\odot$ r

5:end while

6:return [c, i, au, ac]

7:

Algorithm 1 Security Level Evaluation

$S=[\alpha_{c},\alpha_{i},\alpha_{au},\alpha_{ac}]\cdot[c,i,au,ac]^{T}$ (1)

###  IV-D Dependency Analysis

Based on the defined dependency graph above, we use some samples to illustrate
the process mechanism of how to extract the highest risk path to the special
identifier.

####  IV-D1 RRC Connection Setup Dependency Analysis

From Fig. 4, we conclude get that all identifiers in RRC Connection Setup are
not protected by encryption or integrity check. We can conclude that the
security level of identifiers in RRC Connection Setup$=\left[0,0,0,0\right]$.

####  IV-D2  $K_{NASenc}$ Dependency Analysis

$K_{NASenc}$ is the most critical identifier in NAS authentication process and
responsible for the following NAS communication encryption. To prove the
security of $K_{NASenc}$, we extract a logical dependency graph of
$K_{NASenc}$, Fig. 5, from the whole dependency graph of authentication graph,
Fig. 4. From Fig. 5, we can conclude that there are three direct integrity-
dependent identifiers and only one direct authentication-dependent identifier.
We discuss the security level from two aspects of security properties:

  1. 1.

Authentication: Based on the $K_{ASME}$ derivation function, attackers can
derive the $SN_{i}d$ from the $K_{ASME}$. However, attackers can not generate
the $K_{ASME}$ from the $K_{NASenc}$. Based on the authentication conduction
of these three identifiers, the invertibility of the path is critical for
authentication tracking. The coexistence of the authentication dependency
relationship and inevitability can prove the feasibility of invertible
conduction from bottom to up.

  2. 2.

Integrity: The trustworthiness, consistency, and accuracy of the data
throughout its life cycle is termed as integrity. Based on the dependency
relationship of $K_{NASenc}$, as shown in Fig. 5, only with the ability to
modify three direct identifiers, secret attackers can modify $K_{NASenc}$
secretly. Furthermore, attackers can modify three direct identifiers only when
they can modify all five second-level identifiers, which are directly
connected to three direct identifiers. We can conclude that the minimum
requirement of $K_{NASenc}$ modification is $5$ identifiers in $3$ command,
including Attach Request, Authentication Request, and NAS Security Mode
Command.

From the above proof, we can get the security level of
$K_{NASenc}=\left[0,5,1,0\right]$.

Figure 5: Dependency Relationship of $K_{NASenc}$

##  V Formal-based Vulnerability Detection and Attack Models

Based on the 5G authentication and authorization specification abstraction in
Sec.IV, we deploy formal models and analysis to describe the logical attack
models and detect potential attack traces. In the ensuing section, we present
four samples of vulnerabilities detection at disparate stages of the NSA 5G
authentication process and analyze the mechanisms of the exploited attack
traces:(1)User Credentials Disclosure; (2)DoS or Cutting of Device using
Authentication Request,Exposing $K_{NASenc}$ and $K_{NASint}$; (3)Exposing
$K_{RRCenc}$, (4)$K_{RRCint}$ and $K_{UPenc}$ . Our key findings are
encapsulated in Table III in the result Section IX-A.

###  V-A User Credentials Disclosure

In this attack, the adversary can exploit the transparency of RRC Connection
Setup process to effortlessly access critical user identity information, which
includes but is not limited to the UE identity and establishment cause. This
illicit access enables the adversary to acquire user information and use the
ensuing session key for nefarious activities such as eavesdropping and
manipulation of subsequent communications.

Assumption. The adversary can exploit the transparency of RRC Connection Setup
process to directly access any identifier within the message. Furthermore, the
adversary is also capable of establish a fake UE or a MITM relay to eavesdrop
and manipulate the messages within the RRC Connection Setup process. To verify
the security properties of identifiers within the RRC Connection Setup
process, including aspects such as confidentiality and consistency, we
converted the aforementioned assumptions into ProVerif code.

Vulnerability. As depicted in Fig. 3, the UE initiates the process by sending
an RRC connection request to the CN. Upon receiving this request, the CN
responds by transmitting the $radioResourceConfigDedicated$ back to the UE.
The UE, in turn, obtains authentication from the CN and responds with the
$RRC-TransactionIdentifier$, $selectedPLMN-Identity$ and $dedicatedInfoNAS$ to
finalize the RRC connection setup. Nevertheless, this process presents an
exploitable vulnerability as an adversary can access all message identifiers.
Such unprotected identifiers run the risk of being eavesdropped upon and
modified, potentially enabling the adversary to orchestrate a MITM relay
attack.

Attack Trace Description. Employing formal verification, we analyzed the
confidentiality of identifiers within the RRC Connection Setup process.
Through this methodical investigation, we identified two categories of
identifiers with the most significant impact: user identities and RRC
configuration identifiers. As illustrated in Fig. 6, an attacker can access
the identifiers marked in red, delineating the pathway of the attack. In the
initial scenario, an adversary with the access to the user identity, like $UE-
identity$, is capable of launch DoS attack with real $UE-identity$. Contrary
to traditional DoS attacks, which aim to overwhelm a system’s capacity, an
$UE-identity$-based DoS attack efficiently disrupts the CN verification
mechanism through repeated use of the same $UE-identity$, leading to
authentication confusion. And in second case, with computationally derived
$RRC-TransactionIdentifier$, the adversary can establish a fake base station
or perform a MITM relay attack by manipulating these identifiers. In the
latter case, the adversary positions between the UE and the CN, intercepting
and modifying communications in real-time. Consequently, this attack model
presents a severe threat to the security and integrity of the mobile network’s
communication.

Figure 6: User Credentials Disclosure

###  V-B DoS or Cutting of Device using Authentication Request

In the mutual authentication process, not only Attach Request command sent
from UE is neither ciphered nor integrity protected, but the Authentication
Request command sent from CN is also. Attackers can directly record and replay
commands to cut off UE.

Assumption. After CN receives the Attach Request command sent from UE, CN
replies Authentication Request command to confirm whether UE is going to
attach to the network and share the session key. However, because the
Authentication Request command is neither ciphered nor integrity protected, UE
will be hard to verify who and when send the command.

Vulnerability. Due to the non-confidentiality of the Authentication Request
command, attackers can repeat the authentication request command to multi UEs,
as shown in Fig. 7. It is hard for UE to identify which authentication request
command is valid. Multi-times of authentication request command broadcasting
can lead to DoS attacks or cutting of UE. Compared to the User Credentials
Disclosure, the formal model for ”DoS or Cutting of Device using
Authentication Request” is significantly more complicated. Thus, we present
the formal proof of cutting off connection result shown in Fig. 8 about the
interaction between 5G RAN, real-UE and fake-UE.

Figure 7: DoS attack Figure 8: MITM in Mutual Authentication

###  V-C Exposing $K_{NASenc}$ and $K_{NASint}$

NAS security establishment is only protected with integrity but not
encryption, which allows attackers to access all the information but not to
modify them. Attackers can fake as UE or base station with enough information
of authentication process.

Assumption. Commands of the security authentication process in NAS security
setup is only protected by $K_{NASenc}$, a key generated based on the
identifiers of the first command.

Vulnerability. Because commands of NAS security mode setup are not ciphered,
attackers can access the necessary identifiers and generate the corresponding
session key for the following communications based on the corresponding KDF.
Then, attackers can pretend to be a base station to communicate with victim
UE, as shown in Fig. 9. With proof of formal verification, attackers can block
the communication from UE to gNB and continue the NAS security setup process
as the base station.

Figure 9: Exposure of NAS

###  V-D Exposing $K_{RRCenc}$, $K_{RRCint}$ and $K_{UPenc}$

Similar to NAS security setup process, AS security setup process is only
integrity protected. All necessary identifiers of the following RRC and UP
communications are transparent to attackers.

Assumption. Similar to NAS security setup process, all commands of AS security
setup process are only integrity protected without encryption. Attackers can
generate RRC and UP session keys based on eavesdropped identifiers, like Fig.
10.

Vulnerability. Based on the eavesdropped $K_{RRCenc}$, $K_{RRCint}$ and
$K_{UPenc}$, attackers can monitor, hijack, and modify the commands between UE
and CN.

Figure 10: Exposure of AS

##  VI Search Space Isolation

Figure 11: Definition of vulnerability region

The output of formal verification divides the search space into three sets: no
vulnerabilities, attack trace detected, and uncertain areas that need further
investigation. The division of the search space effectively narrows down the
uncertain regions and enables the scalability of vulnerability detection. Fig.
11 is the visual representation of the vulnerability space. The blue area
indicates the formal converted areas. Based on the conclusion from formal
analysis, some traces are formally provable secure, represented by green sets
in Fig. 11, and some traces are provable attacks, characterized by dark purple
sets, and there is attack variance, represented by yellow sets, which are not
provable by formal methods. In addition, large spaces cannot be converted by
the formal method, including implementation errors and non-logical describable
areas, or spaces that could be more labor-intensive and impractical to perform
formal analysis.

Thus, we introduce fuzz testing to connect with and be guided by the formal
result. The formal guided fuzz testings function for two purposes:

  * $\bullet$

Compensate for areas that remain uncovered by formal verification.

  * $\bullet$

Evaluate the potential risks and impacts of the formal provable attack sets.

  * $\bullet$

Detect identifier level unintended emergent behaviors.

##  VII Formal Guided Fuzz Testing

As detailed in Section V, formal verification divided the system’s security
landscape into three zones: safe, non-safe, and unprovable. While the safe
area necessitates no further scrutiny, the non-safe and unprovable areas
warrant further investigation using fuzz testing. Specifically, we leverage
fuzz testing to evaluate the risks of impact of the non-safe areas within
implementation stacks, as well as to ascertain the security level within the
regions previously undetermined. By leveraging our previously developed
viFuzzing platform [34][32][33] that enables bit-level and command-level fuzz
testing for 5G and Beyond protocols and implementation stacks, we effectively
perform formal guided fuzz testing and demonstrate in the range described in
Fig.11. In this session, we present two sets of bit-level fuzzing and nine
sets of command-level fuzzing to illustrate the operation of our formally
guided fuzzing framework.

We set up a relay attack mechanism interfacing our developed platform
viFuzzing and srsRAN[35] following the attack traces detected by formal
verification. The overview structure of the framework that implements formal
guided fuzz testing is shown in Fig. 12, which illustrates the dependency and
flowgraph between formal verification detections and fuzz testing results. We
further present the formal guided fuzz testing cases that addressed the four
detected vulnerabilities using formal analysis in Sec.V.

Figure 12: Integrated Solution of Formal and Fuzz Testing

###  VII-A Modification of $EstablishmentCause$

Based on the proved result of formal verification, we fix the value of C-RNTI
and replay the RRC connection request commands with different values of
identifier $EstablishmentCause$. Through the fuzzing result from Table. II,
modification of $EstablishmentCause$ can lead to the expected result from
formal verification, but the modification of UE-Identity can not affect the
connection as expected. We prove that the implementation of the srsRAN [35]
platform prevent some vulnerabilities of NSA 5G communication protocol.

Besides bit-level fuzzing, we also use command-level fuzzing to test the
vulnerability of incarceration with $rrc_{reject}$ and $rrc_{release}$ [3].
When we fixed the C-RNTI, we found the reply with $rrc_{reject}$ and
$rrc_{release}$ can lead to disconnection and repeat $rrc_{reject}$ and
$rrc_{release}$ can lead to failed connections.

TABLE II: Fuzzing Result of $establishmentCause$ Modification

###  VII-B Repeat Authentication Request Command

Based on Section V-B, the attacker can disconnect multi UEs with the repeat of
Authentication Request. Therefore, in our fuzzing attack model, the attacker
can record the Authentication Request command from one UE and forward the
recorded Authentication Request command to other UEs. To verify the
performance of the fuzzing framework, we set up three following scenarios:

  1. 1.

Only attacker can send command to UE. In this case, UE replies authentication
response and try to establish a connection, which proves what we found in
Section V-B by the formal method.

  2. 2.

One CN and multi attackers compete to send same command to UE. Even if UE gets
confused by multi-times of authentication requests, UE still has the ability
to reply by sending an authentication response to CN.

  3. 3.

One CN and multi attackers compete to send different command to UE. In this
scenario, while attackers use different RAND and disclosure IMSI to generate
different Authentication Request commands and forward different commands to
UE, UE is more likely to reply to the attackers’ requests.

###  VII-C Exposure of $K_{NASenc}$ and $K_{NASint}$

From Section V-C, we can conclude that the attacker in the MITM relay model
has the ability to act as either UE or CN. Compared to complex initial steps
in the traditional fuzz testing model, our proposed fuzzing framework only
needs a few steps to prove the feasibility and detect the implementation
vulnerabilities. We illustrate the detailed fuzzing implementation based on
formal assumptions in the following:

  1. 1.

MITM attack as fake base station. Unlike the traditional fuzz testing
approach, our framework can do fuzz testing with only access to communicated
commands. The following steps illustrate the process flow of our novel
proposed framework:

     * $\bullet$

First, our framework records normal communication commands.

     * $\bullet$

Then, our framework forwards the commands between UE and CN as normal until
mutual authentication establishment with fixed same IMSI and RAND.

     * $\bullet$

After mutual authentication is established, our framework intercepts the
commands from UE and reply with corresponding commands based on the record
communication history.

The result proves that attackers have the ability to deploy MITM attack as the
fake base station.

  2. 2.

Cutting the connection between UE and CN. Besides fuzz testing of the fake
station with blocked signals, our framework can verify the feasibility of
signal competition. The detailed process is listed as follows:

     * $\bullet$

First, our framework records multi-times of normal communication commands with
different IMSI and RAND.

     * $\bullet$

Then, our framework establishs mutual authentication with another IMSI and
RAND.

     * $\bullet$

Unlike the previous fuzz testing case, our framework replies with
corresponding commands and forwards the commands from CN, which simulates the
DoS attack.

Most DoS attacks cut off the connection between UE and CN. The result proves
the vulnerabilities of NAS security setup process. We can conclude the multi
NAS security mode commands attack is an efficient attack model.

###  VII-D Exposure of $K_{RRCenc}$, $K_{RRCint}$ and $K_{UPenc}$

Similar to fuzz testing on NAS security setup, we design two kinds of fuzzing
strategies:

  1. 1.

MITM attack as fake base station. Same with NAS fuzzing case, attackers can
successfully fake as a base station when blocking the signals from CN.

  2. 2.

Cutting the connection between UE and CN. DoS attacks with multi times of AS
security mode commands have a high probability of cutting off the connection
between UE and CN.

##  VIII Fortification of Protocol and Formal Verification

Based on the results from formal analysis and guided fuzz testing,
vulnerabilities detected by fuzz testing are feedback to the formal result and
search space, which lead to the fortification of protocol and formal
verification. This is a crucial component in improving the resilience of 3GPP
specifications.

###  VIII-A User Credentials Disclosure

The adversary can exploit the transparency of RRC Connection Setup process to
effortlessly access critical user identity information, which includes but is
not limited to the UE identity and establishment cause. This illicit access
enables the adversary to acquire user information and use the ensuing session
key for nefarious activities such as eavesdropping and manipulation of
subsequent communications.

Given the significance and susceptibility of identifiers within the RRC
Connection Setup process, it is imperative to implement integrity protection
measures for the $RRC-TransactionIdentifier$. Additionally, adopting a hash
value approach can assist in preventing the disclosure of UE identity, further
reinforcing security measures in this critical process.

###  VIII-B DoS or Cutting of Device using Authentication Request

In the mutual authentication process, not only Attach Request command sent
from UE is neither ciphered nor integrity protected, but the Authentication
Request command sent from CN is also. Attackers can directly record and replay
commands to cut off UE.

Based on the analysis of detected vulnerabilities, it is necessary to develop
a verification mechanism to identify the validation of commands. The
encryption or integrity protection of Authentication Requests becomes
necessary for mutual authentication to guarantee the security of initial
identifiers for the security establishment process. Based on the principle of
minimum change of the current protocol, we propose the following two
solutions:

  * $\bullet$

EC-AKA [36]. EC-AKA proposed new asymmetric encryption to enhance user
confidentiality before symmetric encryption is determined. However, this
solution increases the cost of stations like public key broadcasting.

  * $\bullet$

Hash value to represent IMSI [37]. This approach can prevent attackers from
getting the users’ identities. However, attackers can still modify or deploy
DoS attacks.

  * $\bullet$

Hash value with integrity protection [38]. Khan et al. proposed a combined
solution, which uses hash values to represent IMSI and adds checksum value to
protect integrity. Furthermore, the following commands in the LTE security
setup process can be encrypted by original IMSI, which is invisible to the
attacker but known to UE and CN. Hash value with integrity protection is an
optimal solution that can provide enough security for user identity at a low
cost.

###  VIII-C Exposing $K_{NASenc}$ and $K_{NASint}$

NAS security establishment is only protected with integrity but not
encryption, which allows attackers to access all the information but not to
modify them. Attackers can fake as UE or base station with enough information
of authentication process.

Same with Section VIII-B, there are two encryption methods to protect the NAS
security setup:

  1. 1.

Broadcasting asymmetric public key from gNB can be applied to encrypt the
commands.

  2. 2.

NAS security setup process can encrypt with original IMSI as symmetric key,
while the hashed IMSI is used for RRC connection setup.

###  VIII-D Exposing $K_{RRCenc}$, $K_{RRCint}$ and $K_{UPenc}$

Similar to NAS security setup process, AS security setup process is only
integrity protected. All necessary identifiers of the following RRC and UP
communications are transparent to attackers.

As proposed in previous sections, we can use asymmetric encryption to cipher
the communicated commands between UE and gNB. And we also can use hashed IMSI
as the symmetric key to encrypt the commands.

##  IX Result Analysis and Performance Assessment

###  IX-A Vulnerability Findings via Formal Method and Guided Fuzz Testing

The detailed detected attack models and vulnerabilities have been described in
details in the previous sessions. The summary of the vulnerabilities findings
are listed in Table III. At the protocol level, $4$ attack model categories,
including modification of Radio Resource Control (RRC) connection, Denial of
Service (DoS) or device disconnection using Authentication Request, exposure
of $K_{NASenc}$ and $K_{NASint}$, and exposure of $K_{RRCenc}$, $K_{RRCint}$,
and $K_{UPenc}$, are extrapolated from the attack traces inferred through
formal verification. Following the proposed formal guided fuzz testing
framework shown in Fig.1. In bit-level guided fuzzing, our system uncovers $8$
vulnerabilities. In command-level fuzzing, our framework detected $44$
vulnerabilities. Via the systematic approach, the list of vulnerabilities and
proposed solutions and fortifications significantly enhance the resilience of
the 3GPP specification and large-scale implementations, like srsRAN in our
demonstration. More importantly, unlike the state-of-the-art by-piece
vulnerability detection, it addressed the foundations for achieving assurance
for Future G authentication and authorization in providing the panoramic
vision and examination of the to-date 5G specifications.

TABLE III: Summary of Vulnerability Findings and Comparison with Existing Exploits Formal Derived Attack Models |  Vulnerability |  Assumption |  Related Existing Exploits |  Solution |  Guidance to fuzz |  Executable Vulnerabilities via Guided Fuzzing
---|---|---|---|---|---|---
Modification of RRC Connection |  Modified commands can disable the RRC functions |  known C-RNTI or TMSI |  Related to [3] |  Integrity protection |  Fuzz testing can start with different RRC status. |  54
DoS or Cutting of Device using Authentication Request. |  UE accepts authentication request without integrity. |  None |  Related to [39][36][37][38] |  $\bullet$ EC-AKA [36] $\bullet$ Hashed IMSI [37] $\bullet$ Hashed IMSI with integrity check [38] |  Repeat authentication request commands can be fuzzed at random time to test DoS and cutting of device attack. |  3
Exposing $K_{NASenc}$ and $K_{NASint}$ |  All NAS information can be monitored, hijacked and modified. |  known IMSI, MITM relay |  Related to [40] |  $\bullet$ Asymmetric encryption $\bullet$ Hashed IMSI based encryption |  NAS fuzz testing can start with known $K_{NASenc}$ and $K_{NASint}$. |  2
Exposing $K_{RRCenc}$, $K_{RRCint}$ and $K_{UPenc}$ |  All RRC and UP information can be monitored, hijacked and modified. |  known IMSI, MITM relay |  New Discovery |  $\bullet$ Asymmetric encryption $\bullet$ Hashed IMSI based encryption |  RRC fuzz testing can start with known $K_{RRCenc}$ and $K_{RRCint}$; UP fuzz testing can start with known $K_{UPenc}$. |  2

###  IX-B System Assessment of Computation Complexity in Formal Guided Bit-
Level Fuzzing

Fuzz testing is a systematic brute-force vulnerability detection approach that
involves providing large amounts of random data to find security
vulnerabilities. However, it is not computationally feasible to complete
vulnerability detection for the whole 5G NSA protocol, even for a single
command. State of the art rule-based bit-level fuzz testing strategy has been
proposed, such as [21], which narrows the scope of fuzz testing to specific
identifiers by following the protocol rules. Although the rule-based mutation
fuzz testing strategy achieves an order of magnitude reduction in
computational complexity, there are still meaningless randomly generated
inputs. Our proposed formal-guided fuzz testing strategy follows formal
verification assumptions and generates three sets of a few representative
inputs: formal-based legal inputs, formal-based illegal inputs, and randomly
generated inputs. Formal-based inputs must follow the protocol-defined rules
or format, but not randomly generated inputs.

One of the novelties and advances lies in the scalability of our proposed
system as the number of commands increases in complex protocols. To verify
complex protocols via formal methods, formal analysis requires significant
manpower and computational power. Meanwhile, attempting to cover the entire
space via fuzz testing in the current state-of-the-art methodology requires an
enormous number of test cases and impractical computation time, as the size of
fuzz testing in the brute fuzzing strategy exhibits exponential growth. On the
contrary, our presented formal-guided fuzz testing approach maintains linear
growth as the number of commands increases. In this session, we perform a
quantitative comparison between brute force fuzz testing, state of the art
bit-level fuzzing, and the formal guide fuzz testing.

As depicted in Eq. 2, the brute-force fuzzing strategy indiscriminately flips
bits within randomly selected command sets. Conversely, the rule-based fuzzing
strategy [21], as expressed in Equation 3, confines bit modifications to the
identifiers within randomly chosen command sets. In contrast to these
approaches, our formal-guided fuzz testing identifies the bit-level fuzzing
command first. Focusing on the target commands and restricts alterations to
various types of identifiers, as elucidated in Eq. 4.

For the brute force fuzz testing complexity:

$N_{brute\\_force}=2^{\sum_{k=0}^{K}{\lvert c_{k}\lvert}}$ (2)

where $N_{brute\\_force}$ denotes the number of fuzz testing cases via Brute
Force. $C=[c_{1},c_{2},\cdot\cdot\cdot,c_{K}]$ is the sets of potential
commands in the target procedures fuzz testing. $K$ represents the number of
target commands in fuzz testing, whereas $\lvert c_{k}\lvert$ is the number of
bits in command $k$.

For state of the art rule-based fuzz testing complexity:

$N_{rule\\_based}=2^{\sum_{k=0}^{K}{\lvert c\\_I_{k}\lvert}}$ (3)

where $c\\_I_{k,i}\in[c\\_I_{k,1},c\\_I_{k,2},\cdot\cdot\cdot,c\\_I_{k,i}]$
represents the identifier sets in command $c_{k}$ and $\lvert
c\\_I_{k,i}\lvert$ is the number of bits in identifier $i$ in command $c_{k}$,
$\sum_{i=1}^{I_{k}}\lvert c\\_I_{k,i}\lvert\ll\lvert c_{k}\lvert$ where
$I_{k}$ is the number of identifiers in command $c_{k}$.

For formal guided fuzz testing complexity:

$N_{formal\\_guided}=\sum_{k=1}^{T}\sum_{j=1}^{\lvert
ct\\_I_{k}\lvert}type(ct\\_I_{k,j})$ (4)

where $T=\lvert C\\_target\lvert$ is the number of target commands, whereas
$C\\_target=[ct_{1},ct_{2},\cdot\cdot\cdot,ct_{T}]$. It is to be noted that
$C\\_target$ represents a subset of commands that were detected by a formal
analysis as vulnerable commands that needed to be tested with fuzzing, that
is, $C\\_target\subseteq[c_{1},c_{2},\cdot\cdot\cdot,c_{K}]$. $\lvert
ct\\_I_{k}\lvert$ denotes the number of identifiers in target command
$ct_{k}$. $ct\\_I_{k,j}$ is the identifier $j$ of target command $ct_{k}$,
while $type(ct\\_I_{k,j})$ is the number of logical types of identifier $j$ in
target command $ct_{k}$, including legal and valid value, legal and invalid
value, and illegal random value.

The comparison of computation complexity following Eq. 4 with $4$ fuzz
strategies is shown in Fig. 13, in which fuzzing strategies are selected based
on various application scenarios.

Figure 13: Comparison of Different Bit-level Fuzzing Strategy Efficiency

(1) Connection Request command bit-level fuzzing: Based on the guidance of
formal verification in Section V-A, the RRC Connection Request command, which
includes $40$ bits of UE-Identity, $4$ bits of $EstablishmentCause$, and $1$
bit of spare, is vulnerable to DoS or MITM attacks. Traditional brute-force
fuzz testing generates more than $2^{45}$ fuzzing cases, and rule-based
fuzzing generates $2^{40}+2^{4}+1$ fuzzing cases based on the defined
identifiers. However, our formal guided fuzzing strategy requires only 9
fuzzing cases, including one legal UE-Identity case, one illegal UE-Identity
case, one random out-of-rule UE-Identity case, $2$ legal/illegal
$EstablishmentCause$ cases, $1$ random out-of-rule $EstablishmentCause$ case,
one legal spare case, one illegal spare case, and one out-of-rule spare case.
(2) Authentication Request command bit-level fuzzing: Formal verification
proved the Authentication Request command is the critical part for DoS or fake
station attacks. Inside the Authentication Request command, there are 128 bits
of $RAND$, 128 bits of $AUTN_{HSS}$ and 3 bits of $KSI_{ASME}$. Our proposed
formal guided fuzzing strategy generates $3\times 3$ fuzzing cases, while
brute-force fuzzing generates $2^{259}$ cases and rule-based fuzzing generates
$2^{128}+2^{128}+2^{3}$ cases.
(3) NAS Security Mode command bit-level fuzzing: To verify the formal
assumptions in MITM and cutting of the connection attacks, we make bit-level
fuzzing on NAS Security Mode command. NAS Security Mode command has 3 bits of
$KSI_{AMSE}$, 4 octets of UE capability, 4 bits of $EEA1$, 4 bits of $EIA1$,
and 8 octets of $NAS-MAC$. Brute force fuzzing needs all possible permutations
and random inputs, at least $2^{107}$ cases. Rule-based fuzzing generates at
least $2^{3}+2^{32}+2^{4}+2^{4}+2^{64}$ cases. However, our proposed formal
guided fuzzing only needs $3\times 5$ cases.
(4) AS Security Mode command bit-level fuzzing: To verify the formal
assumptions, AS Security Mode command bit-level fuzzing is necessary. Similar
to NAS Security Mode command, AS Security Mode command contains $4$ bits of
EEA1, $4$ bits of EIA1, and $8$ octets of MAC-I. Like illustrated in NAS
Security Mode command bit-level fuzzing, formal guided fuzzing generates
$3\times 3$ cases. In contrast, brute force fuzzing generates at least
$2^{72}$ cases, and rule-based fuzzing generates $2^{4}+2^{4}+2^{64}$ cases.

Fig. 13 provides an intuitive visualization that compares the effectiveness of
different fuzzing strategies. The upper and lower bounds of the pink area are
represented by values of ”c=1” and ”c=4” in Fig. 13. Notably, it is evident
that brute force fuzzing and rule-based fuzzing exhibit exponential growth
patterns. In contrast, our proposed formal guided fuzzing approach
demonstrates linear growth, requiring considerably less computational power
for vulnerability verification and localization. The superiority of our method
in terms of efficiency and scalability enables a realistic testing and
vulnerability detection across the entire specifications, and provides the
assurance and confidence in 5G system, especially when applied to the critical
infrastructures.

###  IX-C System Assessment of Computation Complexity in Formal Guided
Command-Level Fuzzing

In addition to vulnerability detection at the bit-level of a command using
fuzzing, it is also necessary to verify formal attack traces using command-
level fuzzing. Unlike bit-level fuzzing, no representative case can cover all
out-of-rule cases, which means there are an unlimited number of cases in
command-level fuzzing. To efficiently locate command-level vulnerabilities, we
proposed a probability-based command-level fuzzing framework in our previous
work [27]. Based on formal assumptions of RRC and User Identity Disclosure
attack, we fixed the C-RNTI and ISMI on the srsRAN platform to simulate the
disclosure of user identity. This reduced the number of fuzzing cases to
3,080. Furthermore, based on the identity disclosure assumption, we collected
all different commands on downlink channels and fuzzed all possible
permutations. From Fig. 14, we can conclude that our proposed probability-
based framework requires only $36.5\%$ of the fuzzing cases numbers using a
random fuzzing strategy. The number of cases needed for different percentages
of detected vulnerabilities is shown. In comparison to the conventional linear
growth computation-consuming random fuzzing strategy, we developed
probability-based fuzzing approach demonstrates significantly improved
performance[27]. The incorporation of prior knowledge further enhances the
effectiveness of our method, leading to even greater efficiency gains.
Theoretically, our proposed approaches have the potential to complete millions
of command-level fuzzing iterations within a modest scope of five thousand
test cases. This significant reduction in the number of required test cases
underscores the efficiency and effectiveness of our methodology.

Figure 14: Comparison of Benchmark random-based fuzzing and probability-based
fuzzing.[27]

##  X Conclusion and Future Work

Motivated by the limitations of state-of-the-art vulnerability detection
methods, which include highly computational complex and labor-intensive formal
and fuzz testing approaches, in this paper, we present a first-of-its-kind
formal guided fuzz testing approach for an efficient and systematic 5G
vulnerability detection. In particular, in the proposed approach, formal
verification is implemented to detect attack traces in 5G protocols, which are
then utilized to guide subsequent fuzz testing.

We demonstrate the detection of $4$ attack models and $61$ vulnerabilities in
5G NSA authentication and authorization procedure. We present the generality
and stability of applying the formal guided fuzz testing framework to provide
assurance in other protocols in 5G and Future G releases. The four attack
model categories, which include modification of RRC connection, DoS or device
disconnection using Authentication Request, exposure of $K_{NASenc}$ and
$K_{NASint}$, and exposure of $K_{RRCenc}$, $K_{RRCint}$, and $K_{UPenc}$, are
extrapolated from the attack traces inferred through formal verification. The
detected vulnerabilities by guided fuzz testing further identify the risks and
impacts in each of the four attack models and are verified via real-life
experiments using srsRAN. The detected attack model discovery and
vulnerability detection include the exploits discussed in existing research
and new findings that have never been revealed. Our approach connects the
strengths and coverage of formal and fuzzing methods to efficiently detect
vulnerabilities across protocol logic and implementation stacks hierarchically
and interactively. To close the loop, we incorporate feedback from the
detected attack models and vulnerabilities to fortify systems designs and
enhance system resilience. This innovative approach enables the auto-discovery
of vulnerabilities and unintended emergent behaviors from the communications
specifications to implementation stacks.

Furthermore, in addressing the computation complexity, we assess the
complexity of our approach with conventional fuzz testing results and the
state of art approaches. Conventional fuzz testing would necessitate a
staggering $9\times 10^{77}$ fuzzing cases. Latest researches [21, 18] reveal
that identifier-specific rule-based fuzz testing would require a lesser, yet
substantial, $6\times 10^{38}$ fuzzing cases. In contrast, our system uncovers
$8$ vulnerabilities within a mere $42$ representative fuzz testing cases under
the guidance of formal verification, thereby demonstrating its bit-level
vulnerability detection proficiency. In the realm of command-level fuzzing,
out-of-rule cases are infinite. However, under the formal assumption of RRC
and User Identity Disclosure attack, our framework reduces the number of
fuzzing cases to a manageable $3080$, which is further curtailed to $1027$
through probability-based fuzzing strategy, showcasing the framework’s
superior efficiency.

In the future, we will transfer the framework into an automatic multi-
dimensions vulnerability detection system with reinforcement loop feedback.
The new model will consider a wider variety of data to enable multi-
dimensional input and analysis, like log files and the state of the cache. In
addition to 5G specifications, we will expand the verification and
vulnerability detection to various specifications and implementations,
including IoT and other areas.

## Acknowledgment

The views and conclusions contained herein are those of the authors and should
not be interpreted as necessarily representing the official policies or
endorsements, either expressed or implied, of DARPA or the U.S. Government.

## References

  * [1] J. Alcaraz-Calero, I. P. Belikaidis, C. J. B. Cano, P. Bisson, D. Bourse, M. Bredel, D. Camps-Mur, T. Chen, X. Costa-Perez, P. Demestichas, M. Doll, S. E. Elayoubi, A. Georgakopoulos, A. Mämmelä, H. P. Mayer, M. Payaro, B. Sayadi, M. S. Siddiqui, M. Tercero, and Q. Wang, “Leading innovations towards 5G: Europe’s perspective in 5G Infrastructure Public-Private Partnership (5G-PPP),” in _IEEE International Symposium on Personal, Indoor and Mobile Radio Communications, PIMRC_ , vol. 2017-October, 2018.
  * [2] M. Shatnawi, H. Altaleb, and R. Zoltán, “The digital revolution with nesas assessment and evaluation,” in _2022 IEEE 10th Jubilee International Conference on Computational Cybernetics and Cyber-Medical Systems (ICCC)_. IEEE, 2022, pp. 000 099–000 104.
  * [3] S. R. Hussain, M. Echeverria, I. Karim, O. Chowdhury, and E. Bertino, “5Greasoner: A property-directed security and privacy analysis framework for 5G cellular network protocol,” in _Proceedings of the ACM Conference on Computer and Communications Security_. Association for Computing Machinery, 11 2019, pp. 669–684.
  * [4] G. Klees, A. Ruef, B. Cooper, S. Wei, and M. Hicks, “Evaluating fuzz testing,” in _Proceedings of the 2018 ACM SIGSAC conference on computer and communications security_ , 2018, pp. 2123–2138.
  * [5] A. Souri and M. Norouzi, “A state-of-the-art survey on formal verification of the internet of things applications,” _Journal of Service Science Research_ , vol. 11, no. 1, pp. 47–67, 2019.
  * [6] C. Beaman, M. Redbourne, J. D. Mummery, and S. Hakak, “Fuzzing vulnerability discovery techniques: survey, challenges and future directions,” _Computers & Security_, p. 102813, 2022.
  * [7] Y. Wang, A. Gorski, and L. A. DaSilva, “AI-Powered Real-Time Channel Awareness and 5G NR Radio Access Network Scheduling Optimization,” 2021.
  * [8] Y. Wang, S. Jere, S. Banerjee, L. Liu, V. Modeling, and S. Dayekh, “Anonymous Jamming Detection in 5G with Bayesian Network Model Based Inference Analysis Sachin Shetty,” in _IEEE International Conference on High Performance Switching and Routing 6–8 June 2022 // Virtual Conference_ , 2022.
  * [9] S. Meier, B. Schmidt, C. Cremers, and D. Basin, “The TAMARIN prover for the symbolic analysis of security protocols,” in _Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)_ , vol. 8044 LNCS, 2013.
  * [10] C. Cremers and M. Dehnel-Wild, “Component-Based Formal Analysis of 5G-AKA: Channel Assumptions and Session Confusion.” Internet Society, 3 2019.
  * [11] A. Peltonen, R. Sasse, and D. Basin, “A comprehensive formal analysis of 5g handover,” in _Proceedings of the 14th A CM Conference on Security and Privacy in Wireless and Mobile Networks_ , 2021, pp. 1–12.
  * [12] M. Labib, V. Marojevic, J. H. Reed, and A. I. Zaghloul, “Enhancing the Robustness of LTE Systems: Analysis and Evolution of the Cell Selection Process,” _IEEE Communications Magazine_ , vol. 55, no. 2, 2017.
  * [13] D. Rupprecht, K. Kohls, T. Holz, and C. Popper, “Breaking LTE on Layer Two,” in _Proceedings - IEEE Symposium on Security and Privacy_ , vol. 2019-May, 2019.
  * [14] A. Shaik, R. Borgaonkar, N. Asokan, V. Niemi, and J.-P. Seifert, “Practical Attacks Against Privacy and Availability in 4G/LTE Mobile Communication Systems,” 2017.
  * [15] D. Basin, S. Radomirovic, J. Dreier, R. Sasse, L. Hirschi, and V. Stettler, “A formal analysis of 5g authentication,” in _Proceedings of the ACM Conference on Computer and Communications Security_. Association for Computing Machinery, 10 2018, pp. 1383–1396.
  * [16] G. Klees, A. Ruef, B. Cooper, S. Wei, and M. Hicks, “Evaluating fuzz testing,” in _Proceedings of the ACM Conference on Computer and Communications Security_ , 2018.
  * [17] H. Wang, B. Cui, W. Yang, J. Cui, L. Su, and L. Sun, “An automated vulnerability detection method for the 5g rrc protocol based on fuzzing,” in _2022 4th International Conference on Advances in Computer Technology, Information Science and Communications (CTISC)_. IEEE, 2022, pp. 1–7.
  * [18] F. He, W. Yang, B. Cui, and J. Cui, “Intelligent fuzzing algorithm for 5g nas protocol based on predefined rules,” in _2022 International Conference on Computer Communications and Networks (ICCCN)_. IEEE, 2022, pp. 1–7.
  * [19] L. J. Moukahal, M. Zulkernine, and M. Soukup, “Vulnerability-oriented fuzz testing for connected autonomous vehicle systems,” _IEEE Transactions on Reliability_ , vol. 70, no. 4, pp. 1422–1437, 2021.
  * [20] X. Han, Q. Wen, and Z. Zhang, “A mutation-based fuzz testing approach for network protocol vulnerability detection,” in _Proceedings of 2012 2nd International conference on computer science and network technology_. IEEE, 2012, pp. 1018–1022.
  * [21] Z. Salazar, H. N. Nguyen, W. Mallouli, A. R. Cavalli, and E. M. Montes De Oca, “5Greplay: A 5G Network Traffic Fuzzer - Application to Attack Injection,” in _ACM International Conference Proceeding Series_. Association for Computing Machinery, 8 2021.
  * [22] S. Sheikhi, E. Kim, P. S. Duggirala, and S. Bak, “Coverage-guided fuzz testing for cyber-physical systems,” in _2022 ACM/IEEE 13th International Conference on Cyber-Physical Systems (ICCPS)_. IEEE, 2022, pp. 24–33.
  * [23] M. Ammann, L. Hirschi, and S. Kremer, “Dy fuzzing: Formal dolev-yao models meet protocol fuzz testing,” _Cryptology ePrint Archive_ , 2023.
  * [24] R. Ma, S. Ren, K. Ma, C. Hu, and J. Xue, “Semi-valid fuzz testing case generation for stateful network protocol,” _Tsinghua Science and Technology_ , vol. 22, no. 5, pp. 458–468, 2017.
  * [25] S. Bratus, A. Hansen, and A. Shubina, “Lzfuzz: a fast compression-based fuzzer for poorly documented protocols,” 2008.
  * [26] N. Osborne and C. Pascutto, “Leveraging formal specifications to generate fuzzing suites,” in _OCaml Users and Developers Workshop, co-located with the 26th ACM SIGPLAN International Conference on Functional Programming_ , 2021.
  * [27] J. Yang, Y. Wang, Y. Pan, and T. X. Tran, “Systematic meets unintended: Prior knowledge adaptive 5g vulnerability detection via multi-fuzzing,” _arXiv preprint arXiv:2305.08039_ , 2023.
  * [28] O-RAN Alliance, “O-RAN: Towards an Open and Smart RAN,” _O-RAN Alliance_ , no. October, 2018.
  * [29] Software Radio Systems, “srsRAN is a 4G/5G software radio suite developed by SRS,” 2021.
  * [30] Y. Wang, A. Gorski, and A. da Silva, “Development of a Data-Driven Mobile 5G Testbed: Platform for Experimental Research,” in _IEEE International Mediterranean Conference on Communications and Networking_ , 2021.
  * [31] Y. Wang and C. W. Bostian, “Dynamic cellular cognitive system,” Jan. 10 2012, uS Patent 8,094,610.
  * [32] Jingda Yang, Ying Wang, Tuyen X. Tran, and Yanjun Pan, “5G RRC Protocol and Stack Vulnerabilities Detection via Listen-and-Learn,” in _IEEE Consumer Communications & Networking Conference_, 2023.
  * [33] D. Dauphinais, M. Zylka, H. Spahic, F. k. Shai, J. Yang, I. Cruz, J. Gibson, and Y. Wang, “Automated Vulnerability Testing and Detection Digital Twin Framework for 5G Systems,” in _9th IEEE International Conference on Network Softwarization_ , Madrid, 6 2023.
  * [34] J. Yang, Y. Wang, Y. Pan, and T. X. Tran, “Systematic and Scalable Vulnerability Detection for 5G Specifications and Implementations,” _IEEE JOURNAL ON SELECTED AREAS IN COMMUNICATIONS(Under Review)_ , 2023.
  * [35] I. Gomez-Miguelez, A. Garcia-Saavedra, P. D. Sutton, P. Serrano, C. Cano, and D. J. Leith, “srslte: An open-source platform for lte evolution and experimentation,” in _Proceedings of the Tenth ACM International Workshop on Wireless Network Testbeds, Experimental Evaluation, and Characterization_ , 2016, pp. 25–32.
  * [36] J. B. Bou Abdo, H. Chaouchi, and M. Aoude, “Ensured confidentiality authentication and key agreement protocol for eps,” in _2012 Symposium on Broadband Networks and Fast Internet (RELABIRA)_ , 2012, pp. 73–77.
  * [37] 3GPP, “Universal Mobile Telecommunications System (UMTS); LTE; Mobility Management Entity (MME) Visitor Location Register (VLR) SGs interface specification,” 3rd Generation Partnership Project (3GPP), Technical Specification (TS) 29.118, 01 2015, version 8.5.0. [Online]. Available: https://portal.3gpp.org/desktopmodules/Specifications/SpecificationDetails.aspx?specificationId=1601
  * [38] M. Khan, P. Ginzboorg, K. Järvinen, and V. Niemi, “Defeating the downgrade attack on identity privacy in 5g,” in _International Conference on Research in Security Standardisation_. Springer, 2018, pp. 95–119.
  * [39] J.-K. Tsay and S. F. Mjølsnes, “A vulnerability in the umts and lte authentication and key agreement protocols,” in _Computer Network Security: 6th International Conference on Mathematical Methods, Models and Architectures for Computer Network Security, MMM-ACNS 2012, St. Petersburg, Russia, October 17-19, 2012. Proceedings 6_. Springer, 2012, pp. 65–76.
  * [40] M. T. Raza, F. M. Anwar, and S. Lu, “Exposing lte security weaknesses at protocol inter-layer, and inter-radio interactions,” in _Security and Privacy in Communication Networks: 13th International Conference, SecureComm 2017, Niagara Falls, ON, Canada, October 22–25, 2017, Proceedings 13_. Springer, 2018, pp. 312–338.

|  Jingda Yang (Graduate Student Member, IEEE) received the B.E. degree in
software engineering from Shandong University and the M.Sc. degree in computer
science from The George Washington University. He is currently a Ph.D. student
in the School of System and Enterprises at Stevens Institute of Technology.
His research interests are formal verification and vulnerability detection of
wireless protocol in 5G.
---|---
|  Sudhanshu Arya (Member, IEEE) is a Research Fellow in the School of System
and Enterprises at Stevens Institute of Technology, NJ, USA. He received his
M.Tech. degree in communications and networks from the National Institute of
Technology, Rourkela, India, in 2017, and the Ph.D. degree from Pukyong
National University, Busan, South Korea, in 2022. He worked as a Research
Fellow with the Department of Artificial Intelligence Convergence, at Pukyong
National University. His research interests include wireless communications
and digital signal processing, with a focus on free-space optical
communications, optical scattering communications, optical spectrum sensing,
computational game theory, and artificial intelligence. He received the Best
Paper Award in ICGHIT 2018 and the Early Career Researcher Award from the
Pukyong National University in 2020.
---|---
|  Ying Wang (Member, IEEE) received the B.E. degree in information
engineering at Beijing University of Posts and Telecommunications, M.S. degree
in electrical engineering from University of Cincinnati and the Ph.D. degree
in electrical engineering from Virginia Polytechnic Institute and State
University. She is an associate professor in the School of System and
Enterprises at Stevens Institute of Technology. Her research areas include
cybersecurity, wireless AI, edge computing, health informatics, and software
engineering.
---|---