LTL-Fuzzer is a greybox fuzzer to find violations of arbitrary Linear-time Temporal Logic(LTL) properties. It is built on top of the AFL fuzzer and involves additional program instrumentation to check if a particular execution trace is accepted by the Büchi automaton representing the negation of the given LTL property. Our framework takes as input a sequential program written in C/C++, and an LTL property. It finds violations, or counterexample traces, of the LTL property in stateful software systems.
LTL-Fuzzer substantially extends directed greybox fuzzing to witness arbitrarily complex event orderings. We note that existing directed greybox fuzzing approaches are limited to witnessing reaching a location or witnessing simple event orderings such as crashes or use-after-free. This is the main contribution of our work: algorithms and an implementation of our ideas in a tool that is able to validate any LTL property, thereby covering a much more expressive class of properties than crashes or use-after-free. Our work adapts directed greybox fuzzing (which directs the search towards specific program locations) to find violations of temporal logic formulae.
The paper PDF can be found at https://arxiv.org/abs/2109.02312.
@InProceedings{ltlfuzzer,
title={Linear-time Temporal Logic guided Greybox Fuzzing},
author={Meng, Ruijie and Dong, Zhen and Li, Jialin and Beschastnikh, Ivan and Roychoudhury, Abhik},
booktitle={proceedings of the 37th IEEE International Conference on Software Engineering (ICSE 2022)},
year={2022},
publisher={ACM}
}
- Ubuntu 18.04
- 8G RAM
- Install basic dependencies:
sudo apt install -y build-essential make cmake ninja-build git binutils-gold binutils-dev curl wget
- Install Boost 1.71:
sudo apt install libboost-all-dev libboost-dev
- Install LLVM 11.0.0 with Gold-plugin(can refer to this building script. After that, please copy the following libraries into the specified location:
sudo cp /usr/lib/llvm-11/lib/libLTO.so /usr/lib/bfd-plugins/
sudo cp /usr/lib/llvm-11/lib/LLVMgold.so /usr/lib/bfd-plugins/
- Install spot 2.9.7. You could also follow thses instructions.
wget -q -O - https://www.lrde.epita.fr/repo/debian.gpg | sudo apt-key add -
sudo echo 'deb http://www.lrde.epita.fr/repo/debian/ stable/' >> /etc/apt/sources.list
sudo apt update
sudo apt install -y spot libspot-dev libgtest-dev
- Install Python3 and related modules:
sudo install python3 python3-dev python3-pip
sudo pip3 install --upgrade pip
sudo pip3 install networkx pydot pydotplus
- Clone LTL-Fuzzer and them compile as follows:
cd LTL-Fuzzer
mkdir build
cd build
cmake ../
make
cd ../AFLGo
make
cd llvm-mode
make
cd ../distance_calculator
cmake -G Ninja ./
cmake --build ./
- The subject under test in RERS19 (http://rers-challenge.org/2020/) is located in:
LTL-Fuzzer/experiment/Problem1/src
- All events specified in the subject is stored in the following file:
LTL-Fuzzer/experiment/Problem1/all_event_dir/all_events.txt
- Program locations corresponding to events are stored in the following file:
LTL-Fuzzer/experiment/Problem1/target/targets.txt
- Instrumented subjects are stored in the following directory:
LTL-Fuzzer/experiment/Problem1/build_dir
- The LTL property under check is stored in the following directory:
LTL-Fuzzer/experiment/Problem1/ltl_dir
- The fuzzing initial seeds and outputs are stored, respectively:
LTL-Fuzzer/experiment/Problem1/input_folder
LTL-Fuzzer/experiment/Problem1/output_folder
- Specifying the home directory, e.g., at home dir:
export LTLFuzzer=~/LTL-Fuzzer/
- Specifying the subject directory and name under test:
export SUBJECT=$LTLFuzzer/experiment/Problem1/
export EXECName=Problem1
- Specifying a LTL property to be checked:
export LTL="!(! (true U oU) | (! oU U ((oZ & ! oU) & X (! oU U oP))))"
- Instrumenting the example subject uploaded in the repo, experiment/Problem1
cd $LTLFuzzer/scripts/
./instrument-problem1.sh $SUBJECT/target/targets.txt $SUBJECT/src $SUBJECT/build_dir
- Launching a fuzzing campaign. We use the default fuzzing options here, but you could change fuzzing options as the instructions shown in the Config-Options.md.
cd LTL-Fuzzer/build/src
./ltlfuzz 0
- The testing framework is the same as testing RERS subjects besides one additional fuzzing dictionary file:
LTL-Fuzzer/experiment/testTelnet/telnet.dict
- Specifying the home directory, e.g., at home dir:
export LTLFuzzer=~/LTL-Fuzzer/
- Specifying the subject directory and name under test:
export SUBJECT=$LTLFuzzer/experiment/testTelnet/
export EXECName=telnet-server.minimal-net
- Specifying a LTL property to be checked:
export LTL="!(G((WILL_DISABLED)->(X(G((DO)|(DONT))))))"
- Instrumenting the example subject uploaded in the repo, experiment/testTelnet
cd $LTLFuzzer/scripts/
./instrument-telnet.sh $SUBJECT/targets/targets.txt $SUBJECT/contiki $SUBJECT/build_dir
- Launching a fuzzing campaign. We use the default fuzzing options here, but you could change fuzzing options as the instructions shown in the Config-Options.md.
cd LTL-Fuzzer/build/src
./ltlfuzz 1
- Ruijie Meng
- Zhen Dong
- Jialin Li
- Ivan Beschastnikh
- Abhik Roychoudhury
We use AFLGo as one component to direct fuzzing towards a particular program location. Thanks to AFLGo's developers. We also welcome other contributors to improve and extend LTL-Fuzzer.
This project is licensed under the Apache License 2.0 - see the LICENSE file for details.