DIKEUE

This is the public release of the code of our paper titled "Noncompliance as Deviant Behavior: An Automated Black-box Noncompliance Checker for 4G LTE Cellular Devices" (CCS'21).

The paper: https://dl.acm.org/doi/10.1145/3460120.3485388

Table of Contents

• Introduction
• Requirements
• DIKEUE Overview
• FSM Inference Module
  • Learner
  • Modified Cellular Stack
  • Device Resetter
  • Running FSM Inference Module
• FSM Equivalence Checker
• Acknowledgement
• License

Introduction

DIKEUE is an automated black-box testing framework for 4G Long Term Evolution (LTE) control-plane protocol implementations in commercial-of-the-shelf (COTS) cellular devices (UEs). It adopts a property-agnostic differential testing approach to identify deviant behavior in UEs.

Requirements

• Ubuntu 18.04 (tested OS)
• USRP B210 (tested SDR)
• adb
• graphviz
• jdk 11
• maven
• python 2
• pydot

DIKEUE Overview

DIKEUE has two primary components, namely, FSM inference module, and FSM equivalence checker. The FSM inference module requires blackbox access to UEs and uses active automata learning to extract the protocol state machine of UE implementations. On the other hand, the FSM equivalence checker tries to identify diverse set of deviant behavior by taking pairs of state machines generated by the prior component. Figure 1 shows the workflow of DIKEUE.

Figure 1: Workflow of DIKEUE

FSM Inference Module

The FSM inference module contains a learner and an adapter which communicates with a UE with blackbox access. The learner generates abstract symbols which is converted to concrete packets by the adapter. Additionally, the adapter optimizes the number of over-the-air packets and resolves inconsistencies to reduce the time required for learning the finite state machine of the UE.

Figure 2: FSM Inference Module

Learner

The learner uses active automata learning to learn the protocol state machine of the device under test. It generates many membership queries and equivalence queries to construct hypthesis models and to check for their validity. The cache resolver and inconsistency resolver is also embedded to the learner. To run the learner, the following commands can be used:

cd "FSM_Learner_Module/statelearner/"
mvn package shade:shade
java -jar target/stateLearner-0.0.1-SNAPSHOT.jar src/lteue.properties

Modified Cellular Stack

The learner sends queries to the modified cellular stack, which generates concrete packets. It is given at FSM_Learner_Module/modified_cellular_stack.

srsLTE

Our modified cellular stack is built on srsLTE 19.03. Instructions to build srsLTE can be found at the original repository and also at FSM_Learner_Module/modified_cellular_stack/srsLTE. After building, srsEPC and srsENB can be run from their respective build directories.

Configuration Requirements

A set of modified configurations are given at FSM_Learner_Module/modified_cellular_stack/conf. These configuration files should be used instead of default srsLTE configurations.

Sim Card Requirements

FSM_Learner_Module/modified_cellular_stack/conf/srsepc/user_db.csv contains the sim card information and keys that can be used by srsLTE. These should be updated according to the used sim card with the device under test. However, IMSI and other information should follow srsLTE standards. For further details, please refer to srsLTE website. Moreover, other configuration files, e.g., FSM_Learner_Module/modified_cellular_stack/conf/srsenb/enb.conf, FSM_Learner_Module/modified_cellular_stack/conf/srsepc/epc.conf, etc., will need to be change accordingly as well.

Figure 3: Modified FSM Inference Module

Device Resetter

Our implementation requires a device resetter, which controls the device and resets when requested by the learner.

To run the device resetter, the following commands can be used:

cd "FSM_Learner_Module/device_resetter/"
python2 resetter.py all

Note that for each devices, the following two functions need to be updated inside device_resetter:

• airplane_mode_on
• airplane_mode_off

Running FSM Inference Module

To run the the FSM Inference Module, first you need to program a sim card according to srsLTE requirements, and insert it into the device under test. Then, you need to run the device_resetter. After that, you need to run srsEPC, and srsENB. Finally, you need to run statelearner.

All the queries will be saved in the my_database.sqlite. In the the learner is run again it will read queries from the database and in case the query is not found then communicate with the adapter. For running the learner from scratch the tables of the database will have to be deleted.

To change input symbols, output symbols, or other learning parameters, e.g., device name, learning algorithm, max depth, etc., please change FSM_Learner_Module/statelearner/src/lteue.properties accordingly.

FSM Equivalence Checker

The FSM equivalence checker takes two finite state machines in dot format 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 "FSM_Equivalence_Checker/"
python2 iterative-checker.py

Additional command line options can be viewed with:

python2 iterative-checker.py --help

It takes the equivalence checker around 40-45 mins in our machine to check equivalence between the two FSMs. After the checking is done it will create two files: FSM1_vs_FSM2_final and FSM1_vs_FSM2_time. FSM1_vs_FSM2_final contains the deviating queries for the same input symbol. FSM1_vs_FSM2_time contains the timing for each round of model checking with nuXmv. The Folder already includes a nuXmv binary so installing nuXmv is not required.

Acknowledgement

We thank srsRAN and StateLearner developers for making their tools publicly available. DIKEUE modifies these tools to implement the FSM Inference Module.

License

This work is licensed under Apache License 2.0. Please refer to the license file for details.