Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

State Machine Mutation-based Testing Framework for Wireless Communication Protocols

Syed Md Mukit Rashid, Tianwei Wu, Kai Tu, Abdullah Al Ishtiaq, Ridwanul Hasan Tanvir, Yilu Dong, Omar Chowdhury, Syed Rafiul Hussain

TL;DR

Proteus, a protocol state machine, property-guided, and budget-aware automated testing approach for discovering logical vulnerabilities in wireless protocol implementations, is proposed and evaluated in two different protocol implementations.

Abstract

This paper proposes Proteus, a protocol state machine, property-guided, and budget-aware automated testing approach for discovering logical vulnerabilities in wireless protocol implementations. Proteus maintains its budget awareness by generating test cases (i.e., each being a sequence of protocol messages) that are not only meaningful (i.e., the test case mostly follows the desirable protocol flow except for some controlled deviations) but also have a high probability of violating the desirable properties. To demonstrate its effectiveness, we evaluated Proteus in two different protocol implementations, namely 4G LTE and BLE, across 23 consumer devices (11 for 4G LTE and 12 for BLE). Proteus discovered 25 unique issues, including 112 instances. Affected vendors have positively acknowledged 14 vulnerabilities through 5 CVEs.

State Machine Mutation-based Testing Framework for Wireless Communication Protocols

TL;DR

Proteus, a protocol state machine, property-guided, and budget-aware automated testing approach for discovering logical vulnerabilities in wireless protocol implementations, is proposed and evaluated in two different protocol implementations.

Abstract

This paper proposes Proteus, a protocol state machine, property-guided, and budget-aware automated testing approach for discovering logical vulnerabilities in wireless protocol implementations. Proteus maintains its budget awareness by generating test cases (i.e., each being a sequence of protocol messages) that are not only meaningful (i.e., the test case mostly follows the desirable protocol flow except for some controlled deviations) but also have a high probability of violating the desirable properties. To demonstrate its effectiveness, we evaluated Proteus in two different protocol implementations, namely 4G LTE and BLE, across 23 consumer devices (11 for 4G LTE and 12 for BLE). Proteus discovered 25 unique issues, including 112 instances. Affected vendors have positively acknowledged 14 vulnerabilities through 5 CVEs.
Paper Structure (32 sections, 18 figures, 14 tables, 1 algorithm)

This paper contains 32 sections, 18 figures, 14 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries and Notations
  3. Motivation of PROTEUS
  4. Running Example
  5. Benefit of Having PSM and Properties
  6. Design Overview and Challenges
  7. Proteus Overview
  8. Challenges and Insights
  9. $\mathsf{RegExGenerator}$: Constructing Test Skeletons From Security Properties
  10. $\mathsf{TraceBuilder}$: Generating Test Cases from Test Skeletons and Guiding PSM
  11. Mutating a PSM
  12. Instantiated Trace Generation
  13. $\mathsf{TraceDispatcher}$: Test Execution and Flaw Detection
  14. Experiments
  15. Experiment Setup For Testing
  16. ...and 17 more sections

Figures (18)

  • Figure 1: A partial LTE protocol state machine used as guiding PSM for running example. The transition labels are presented in Table \ref{['tab:ble_running_example_table']}, with red transitions indicating mutations.
  • Figure 2: Overview of Proteus.
  • Figure 3: Example AST of a PLTL formula.
  • Figure 4: Two kinds of mutations M1 and M2. The transition labels are presented in Table \ref{['tab:ble_running_example_table']}.
  • Figure 5: After authentication.
  • ...and 13 more figures