RVAT: Detecting Logic Vulnerabilities in Robotic Vehicles through Timed-Automata-based Simulation

RVAT (Robotic Vehicle Automata-based Testing) is a comprehensive framework for testing of flight control software. This project provides automated tools for property specification extraction, code analysis, model generation, and testing of flight control systems including ArduPilot and PX4.

Documentation

• Properties - Discovered properties for ArduPilot and PX4, comparative analysis, and violation reports
• Prompts - LLM prompt templates for property extraction, RAG-based slicing criteria identification, and formula correction

Table of Contents

• Project Structure
• Installation
  • System Requirements
  • Basic Dependencies
  • Module Dependencies
  • UAV Environment Setup
  • Python Dependencies
  • Environment Configuration
• Build
• Quick Start
• Reproduce the Figure Results
• Usage
  • Global Setup (Execute Once)
  • Property Testing Workflow
• Advanced Configuration
• Testing with PGFuzz

Project Structure

modelCheckingFlightControl/
├── cmake_deps/                  # CMake dependency configurations
│   ├── boost.cmake
│   ├── llvm.cmake
│   ├── sharedUtils.cmake
│   ├── svf.cmake
│   └── yaml-cpp.cmake
├── configs/                     # Configuration files
│   ├── IR_config.yml           # IR instrumentation configuration
│   ├── properties_config.yml   # Property testing configuration
│   ├── property_slice_criterion.json # Slice criteria for properties, generated by RAG
│   └── verifications.yml       # Testing definitions
├── dependencies/                # External dependencies
│   ├── KLEE/                   # KLEE symbolic execution engine
│   ├── llvm-16.0.4/            # LLVM compiler infrastructure
│   ├── SVF-3.1/                # Static Value-Flow analysis framework
│   └── uppaal-5.0.0-linux64/   # UPPAAL model checker
├── flight-control/              # Flight control software
│   ├── arducopter-4.4/         # ArduPilot Copter 4.4
│   └── PX4-1.15.2/             # PX4 Autopilot v1.15.2
├── git_patchs/                  # Patches for dependencies
│   ├── ardupilot.patch
│   ├── klee.patch
│   ├── llvm.patch
│   ├── pgfuzz.patch
│   └── px4.patch
├── instrumenter/                # Code instrumentation tool for data collection
├── InterpreterR/                # LLVM IR interpreter for semantic execution of TCFA
├── KLEE/                        # Instrumentation tool for KLEE symbolic execution, automatically inserts klee_entry functions
├── llvm-pdg/                    # PDG-based function-level slicing tool
├── modelTempGen/                # Model template generator
├── PGFuzz/                      # PGFuzz fuzzing tool
├── preAnalyzer/                 # Pre-analysis tools for indirect call analysis
├── prompts/                     # LLM prompts for property extraction
├── pyscript/                    # Python automation scripts (LLM integration, analysis, model generation, testing scripts)
├── sharedUtils/                 # Shared utility libraries
├── build.sh                     # Main build script
├── install-envreqs.sh           # Environment dependencies installer
├── install-modules.sh           # Module dependencies installer
├── install-uav-envs.sh          # UAV environment installer
├── requirements.txt             # Python dependencies
├── run_verify.sh                # Main verification script
├── set_env.sh                   # Environment setup script
└── verify-api.py                # Verification API

Installation

System Requirements

• Operating System: Ubuntu 22.04 LTS (recommended)
• Python: 3.11

Basic Dependencies

Install system-level dependencies and tools required by the framework:

./install-envreqs.sh -y

This script will install:

• Build tools (CMake, GCC, Clang)
• System libraries (Boost, Z3, STP, etc.)
• Development tools (Git, Ninja, etc.)

Module Dependencies

Install and configure all required modules (LLVM, KLEE, SVF, flight control software, etc.):

./install-modules.sh

This script will:

1. Clone and checkout ArduPilot Copter-4.4 with patches
2. Clone and checkout PX4-Autopilot v1.15.2 with patches
3. Clone CVC5-1.3.0 (SMT solver)
4. Clone STP-2.3.3 (constraint solver)
5. Clone KLEE-uClibc (klee_0_9_29)
6. Clone KLEE v3.1 with patches
7. Clone LLVM 16.0.4 with patches
8. Clone PGFuzz (commit 7eaebf2) with patches

All modules will be placed in appropriate directories (flight-control/, dependencies/, etc.).

UAV Environment Setup

Install UAV-specific dependencies (MAVProxy, SITL environment, etc.):

./install-uav-envs.sh

Python Dependencies

Install required Python packages:

pip install -r requirements.txt

Environment Configuration

Set up required environment variables:

source ./set_env.sh

To make environment variables permanent, add to your shell configuration:

echo "source $(pwd)/set_env.sh" >> ~/.bashrc
source ~/.bashrc

Build

Build all components of the RVAT framework:

./build.sh all

The build process compiles:

• dependencies: LLVM, KLEE, SVF, etc.
• instrumenter: Code instrumentation tool for data collection
• InterpreterR: LLVM IR interpreter for semantic execution of TCFA
• KLEE: Instrumentation tool for KLEE symbolic execution, automatically inserts klee_entry functions
• llvm-pdg: PDG-based function-level slicing tool
• modelTempGen: Model template and structure expander
• preAnalyzer: Pre-analysis tools for indirect call analysis
• sharedUtils: Shared utility libraries

For selective builds, you can build individual modules:

# Build specific modules
./build.sh ist
./build.sh klee

# Show available build targets
./build.sh help

Quick Start

For users who have completed the Global Setup and want to quickly test a property:

1. Download verifyDataBase

Download the pre-configured database containing property definitions and test configurations:

verifyDataBase Link: https://osf.io/f7bjx/overview?view_only=f44a4580641548c299d801c06033813b

# Check sum of the downloaded file
sha256sum -c checksums.txt
# Merge parts
cat verifyDataBase.tar.gz.part.* > verifyDataBase.tar.gz
# Extract the database to project root directory
tar -xvzf verifyDataBase.tar.gz -C /path/to/RVAT/

Note: Ensure you extract verifyDataBase to the project root directory (e.g., ~/RVAT/).

2. Specify Property

Specify which property you want to test:

./run_verify.sh -u specify_property <property_name>

# Example:
./run_verify.sh -u specify_property PX_POSITION_P3

3. Run Testing

Execute testing for the specified property:

./run_verify.sh -u verify

Reproduce the Figure Results

Figure	Command	Data
Figure 2	python pyscript/LLM/property_extraction/similarity_threshold_selection.py	pyscript/LLM/property_extraction/
Figure 3 (a)	python pyscript/initializer/plotBlockSizeCDF.py	verifyDataBase/model_inputs/times/
Figure 3 (b)	python pyscript/initializer/plotCoverageLinechart.py	verifyDataBase/model_inputs/times/
Figure 4 (a)	python pyscript/pyTools/draw_tools/draw_fs_time_series.py	verifyDataBase/draw_datas/
Figure 4 (b)	python /home/lqs66/RVAT/pyscript/pyTools/draw_tools/manual_control_setpoint_plot.py	verifyDataBase/draw_datas/case_1_manual_control_setpoint.csv
Figure 5	python pyscript/pyTools/draw_tools/draw_case2_failsafe_on.py	verifyDataBase/draw_datas/case2_failsafe_on.bin
Figure 6	python pyscript/pyTools/draw_tools/draw_case2.py	verifyDataBase/draw_datas/case2.bin
Figure 7 (a-b)	python pyscript/pyTools/draw_tools/draw_case3.py	verifyDataBase/draw_datas/case3_roll/pitch.bin

Usage

Global Setup (Execute Once)

Before testing any properties, complete these one-time setup steps:

1. Build Flight Control Software

./run_verify.sh -u build_uavs -cn verify

This compiles the flight control software with appropriate flags for testing.

2. Generate IR (Intermediate Representation)

Generate LLVM IR for the target flight control system:

# For ArduPilot
./run_verify.sh -u gen_ir ardupilot

# For PX4
./run_verify.sh -u gen_ir px4

Generated IR files will be saved in verifyDataBase/ir_and_elf/.

3. Generate Input Templates

./run_verify.sh -u gen_temps ardupilot  # or px4

This generates:

• verifyDataBase/inputTemplates/<flight_control>_modelInGV.tmp (global variables)
• verifyDataBase/inputTemplates/<flight_control>_modelInHeap.tmp (heap memory)

4. Extract Properties from Flight Control Documentation

Automatically extract properties from flight control documentation using LLM:

4.1. Extract Documentation Paragraphs

python verify-api.py uav_doc_extract -t <type> -p <path>

Example for PX4:

python verify-api.py uav_doc_extract -t px4 -p ~/Desktop/px4_wiki/

Generated CSV files are saved to pyscript/LLM/data/<type>_doc_pairs/.

4.2. Generate Property Specifications with LLM

python verify-api.py extract_property_specifications -f <input_csv> -r -m [deepseek | openrouter]

Generated properties are saved as JSON files.

4.3. Vectorize LLM-Generated Property Specifications

# For ArduPilot
python verify-api.py text_embedding -t ardupilot

# For PX4
python verify-api.py text_embedding -t px4

4.4. Evaluate Similarity Threshold

# For ArduPilot
python verify-api.py similarity_threshold -t ardupilot

# For PX4
python verify-api.py similarity_threshold -t px4

4.5. Cluster Property Specifications

# For ArduPilot
python verify-api.py clustering -t ardupilot

# For PX4
python verify-api.py clustering -t px4

5. Build Flight Control Code Vector Database

Create vector embeddings of flight control source code for RAG-based analysis:

# For ArduPilot
./run_verify.sh -u vectorize ArduCopter

# For PX4
./run_verify.sh -u vectorize px4

This step:

• Parses flight control source code
• Creates vector embeddings using code embedding models
• Stores embeddings in vector database (Qdrant)
• Enables RAG-based slice criterion identification in property testing workflow

Property Testing Workflow

For each property to be tested, follow these steps:

Step 1: Specify Property to Test

./run_verify.sh -u specify_property <property_name>

Step 2: Generate Slice Criterion with RAG

./run_verify.sh -u find_slice_criterion

The slice criterion is inserted into configs/property_slice_criterion.json.

Step 3: Generate Program Slice

./run_verify.sh -u slice

Function-level slices are saved to verifyDataBase/func_slice/<property_name>_Slice_FS.yml.

Step 4: Instrument Data Collection Code

./run_verify.sh -u instrument

The Instrumenter parses configs/IR_config.yml to instrument the IR. Key instrumentation parameters:

• IC_GUARD: Controls global variable dumping
• RET_C_RATE: Controls return value collection frequency
• time_c_cycle: Controls basic block execution time collection frequency

Step 5: Compile Instrumented Code

./run_verify.sh -u ir_build

Step 6: Upload to Raspberry Pi

./run_verify.sh -u upload_pi

Note: For PX4, you need to upload:

• build/xxx/etc
• build/xxx/bin
• flight-control/PX4-1.15.2/posix-configs/rpi/px4_hil_complated.config

Step 7: Collect Model Inputs

Run the instrumented executable on Raspberry Pi to collect model input seeds (entry function parameters, memory variable values, basic block execution times):

Run UAV software:

# Run UAV software on Raspberry Pi
./run_verify.sh -u run_uav

# For timing properties (additional execution)
./run_verify.sh -u run_uav --isTime

Start Simulation Environment:

./run_verify.sh -u run_sim  # Use export HEADLESS=1 for headless mode

Execute flight missions according to the property being tested (see user guide for specific commands).

Step 8: Download Collected Data

./run_verify.sh -u download_pi

Step 9: Create Input Seed Files

./run_verify.sh -u create_input_seeds

Important: After this step, check the console output for entry argument offsets and update heap + xx values in configs/IR_config.yml accordingly.

Example output:

[INFO] Entry Args:
[INFO]  id: 0, type: ptr, size: 8, value: 158692, raw: 548883406192

Calculate the offset (for PX4: subtract 33528; for ArduPilot: subtract 194045).

Step 10: Instrument KLEE Entry Function

./run_verify.sh -u instrument_klee_entry

Before this step, ensure the queries field in configs/IR_config.yml is complete.

Step 11: Symbolic Execution with KLEE

./run_verify.sh -u klee

KLEE performs symbolic execution to generate test cases.

Step 12: Convert .ktest to Model Input Files

./run_verify.sh -u create_inputs

Converts KLEE test cases (.ktest) to model input files (.mi).

Step 13: Generate UPPAAL Timed Automata Model

./run_verify.sh -u gen_uppaal_model

Before generating the model, ensure configs/verifications.yml contains the property configuration.

Models with timing constraints are automatically augmented with:

• Global clocks: For system-wide time constraints (e.g., mission deadlines)
• Local clocks: For bounded response times (reset on transitions)

Generated models are saved to verifyDataBase/uppaal_models/<property_name>/.

Step 14: Execute Testing

./run_verify.sh -u verify

UPPAAL tests the timed automata model against the TCTL property.

Generate Counter-Example Trace:

export MODEL_INPUT_PATH=<path_to_model_input.mi>
./dependencies/uppaal-5.0.0-linux64/bin/verifyta -q -t 0 <path_to_model.xml>

Advanced Configuration

Configuration Files

• configs/properties_config.yml: Define properties, entry functions, TCTL formulas, and variable mappings
• configs/IR_config.yml: Configure instrumentation parameters, entry arguments, and KLEE queries
• configs/verifications.yml: Testing definitions for UPPAAL model generation
• configs/property_slice_criterion.json: Slicing criteria for each property

Viewing Model Input Files

Convert binary .mi files to XML for inspection:

python pyscript/initializer/deserialize_to_xml.py \
  <path_to_input.mi> \
  <path_to_output.xml>

Testing with PGFuzz

For configuration and usage instructions, please refer to: https://github.com/purseclab/PGFUZZ