5GBaseChecker

This is the public release of the code of 5GBaseChecker, a security analysis framework for the control plane protocols of 5G baseband.

Based on this tool, we have the following USENIX Security '24 paper and BlackHat '24 talk:

USENIX Security 2024 paper: "Logic Gone Astray: A Security Analysis Framework for the Control Plane Protocols of 5G Basebands" (USENIX'24). Link: https://www.usenix.org/conference/usenixsecurity24/presentation/tu

BlackHat 2024 Talk: https://www.blackhat.com/us-24/briefings/schedule/index.html#cracking-the-g-fortress-peering-into-gs-vulnerability-abyss-40620

Table of Contents

• Introduction
• Requirements
• 5GBaseChecker Overview
• StateSynth
  • Modified Cellular Stack
    • Configuration Requirements
    • Sim Card Requirements
  • Running Passive Learner
  • Running State Learner
• DevScan
• DevLyzer
  • Install NuSMV
  • DevLyzer Component Overview
  • Run DevLyzer
• Acknowledgement
• License

Introduction

5GBaseChecker is an efficient, scalable, and dynamic security analysis framework based on differential testing for analyzing 5G basebands’ control plane protocol interactions. It captures basebands’ protocol behaviors as finite state machines (FSMs) through black-box automata learning, identifies input sequences for which the extracted FSMs provide deviating outputs, and leverages these deviations to identify security properties from specifications to triage if the deviations found in 5G basebands violate any properties.

Requirements

• Ubuntu 20.04 (tested OS)
• USRP B210 (tested SDR)
• sysmoISIM-SJA2 SIM Card
• adb
• graphviz
• jdk 11
• maven
• python 2
• python 3
• pydot
• MongoDB 4.4
• NuSMV 2.6.0

5GBaseChecker Overview

5GBaseChecker has three primary components, namely, StateSynth, DevScan, and DevLyzer. The StateSynth module employs a hybrid and collaborative automata learning approach to extract finite state machines (FSMs) from 5G baseband implementations. DevScan then compares these FSMs to identify deviations between the FSMs constructed by StateSynth. DevLyzer further triages these deviations to determine security properties and identify potential vulnerabilities. Figure 1 illustrates the workflow of 5GBaseChecker.

Figure 1: Workflow of 5GBaseChecker

StateSynth

The StateSynth module consists of State learner, and a modified cellular stack (OAI gNodeB, srsRAN gNodeB and Open5GS as Core Network). It can be utilized to construct FSM for 5G UE devices. We provide instructions on how to build and run below.

Modified Cellular Stack

The modified cellular stack will convert the queries from state learner to concrete packets and send it to the UE.

You can find detailed instructions to install Open5GS here: building-open5gs-from-sources. Please note that we are using MongoDB 4.4.

• Build Open5GS

cd "StateSynth/modified_cellular_stack/5GBaseChecker_Core"
meson build --prefix=`pwd`/install
ninja -C build

You can find detailed instructions to install OAI here: NR_SA_Tutorial_OAI.

• Building OAI gNodeB

cd "StateSynth/modified_cellular_stack/5GBaseChecker_OAI_gnb/cmake_targets"
sudo ./build_oai  -w USRP -C --gNB --ninja 

You can find detailed instructions to install srsRAN here: srsRAN document.

• Building srsRAN gNodeB

cd "StateSynth/modified_cellular_stack/5GBaseChecker_srs_gnb"
mkdir build && cd build
cmake ..
make srsenb -j4

Configuration Requirements

A set of modified configurations are given at StateSynth/modified_cellular_stack/conf.

Sim Card Requirements

It's possible that the commercial UE doesn't search any 5G gNodeB and initiates the connection due to SIM card. We followed this link to program our SIM card and it works.

Running Passive learner

First, install the dependencies for Trace2Model. You can find the detail instructions here.

To run Passive learner and extract potential counter-examples(PCEs), execute the following commands:

cd 5GBaseChecker/StateSynth/Trace2Model
python3 learn_model.py -i /5GBaseChecker/StateSynth/Trace2Model/benchmarks/TelAviv/example.txt --incr --dfa -w 3
python3 ./DotProcess.py 
cp 5GBaseChecker/StateSynth/Trace2Model/FSM2.dot 5GBaseChecker/StateSynth/fsm_comparator/FSM
python2.7 ./iterative_checker.py -lts1 FSM/FSM1.dot -lts2 FSM/FSM2.dot -o FSM1_vs_FSM2
python3 ./CEextract.py

Running State Learner

Please update scripts under the directory StateSynth/5GBaseChecker_Statelearner according to your machine configuration before you run the State Learner.

To run the state learner, you can execute the following commands:

java -jar StateSynth/5GBaseChecker_Statelearner/out/artifacts/5GBaseChecker_Statelearner_jar/5GBaseChecker_Statelearner.jar fgue.properties

To change input symbols or other learning parameters, e.g., device name, max depth, etc., please change StateSynth/5GBaseChecker_Statelearner/fgue.properties accordingly.

You can put potential counter-examples (PCEs) extracted the learning phase of other phones to StateSynth/5GBaseChecker_Statelearner/CEStore/input, this could help accelerate the FSM learning procedure.

DevScan

DevScan takes a set of FSMs constructed by StateSynth as inputs and provides the deviating behavior inducing message sequences. We have included two sample FSMs for demonstrating the use of the component. It can be run with the following commands:

cd "DevScan/fsm_checking/fsm_equivalence_checker_5GBaseChecker"
python3 Autorun.py

After this command, the result will be stored in the DevScan/fsm_checking/fsm_equivalence_checker_5GBaseChecker/Result folder. Then execute the following command to summarize the result.

python3 AutoAnalysis.py

After executing the above command, you will get an output file deviant-queries.json. This will be the input for DevLyzer.

DevLyzer

Install NuSMV

You can download NuSMV from here.

To add NuSMV to your PATH environment variable, you need to edit your ~/.bashrc file.

1. Open the ~/.bashrc file in a text editor. nano ~/.bashrc.
2. Add the path to NuSMV to your PATH variable: Find the directory where NuSMV is installed. Let's assume it is installed in /usr/local/NuSMV/bin. Add the following line at the end of your ~/.bashrc file: export PATH=$PATH:/usr/local/NuSMV/bin.
3. Save and close the file.
4. Source the ~/.bashrc file to apply the changes. source ~/.bashrc
5. Verify the changes. Check if NuSMV is accessible by typing: NuSMV --version. This should display the version of NuSMV, confirming that it is correctly added to your PATH.

DevLyzer Component Overview

DevLyzer has an attack_trace_checker folder. All the input and output alphabets are placed in the all_input.txt and all_output.txt files respectively. The LTL properties are placed in the ltl_properties.txt file. The main python script for DevLyzer is main.py. The deviant_queries.json contains all the deviations among devices output from DevScan.

Run DevLyzer

Run the main.py file.

cd DevLyzer
python3 ./main.py

The console will show (total number of deviations analyzed) / (total number of deviations provided). It will also display the input sequence of unresolved deviations (if any). Our provided deviations list and program takes ~20 minutes to run on our machine.

Citation

@inproceedings {tu2024logic,
author = {Kai Tu and Abdullah Al Ishtiaq and Syed Md Mukit Rashid and Yilu Dong and Weixuan Wang and Tianwei Wu and Syed Rafiul Hussain},
title = {Logic Gone Astray: A Security Analysis Framework for the Control Plane Protocols of 5G Basebands},
booktitle = {33rd USENIX Security Symposium (USENIX Security 24)},
year = {2024},
isbn = {978-1-939133-44-1},
address = {Philadelphia, PA},
pages = {3063--3080},
url = {https://www.usenix.org/conference/usenixsecurity24/presentation/tu},
publisher = {USENIX Association},
month = aug
}

Acknowledgement

We thank Open5GS, OpenAirInterface, srsRAN, Trace2Model and StateLearner developers for making their tools publicly available. 5GBaseChecker modifies these tools to implement the FSM Inference Module.

License

This work is licensed under the GNU Affero General Public License (GNU AGPL v3.0). Please refer to the license file for details.