Table of contents

Get Started

SWAT has two primary usage modes: Active Exploration Mode and Passive Exploration Mode. In Active Mode, The Symbolic Explorer is responsible for interacting with the System under Test (SuT). Hence the Explorer either starts your SuT repeatedly with new values or sends HTTP requests to your SuT.

UserPassive ModeActive ModeSystem under TestJavaSymbolic ExplorerPythonSymbolic ExecutorJavaProvidesExecutes/QueriesSymbolic TraceStartsResultsAttachesUserSymbolic ExplorerPythonSystem under TestJavaProvidesInteractsStartsResultsHarness/ Driver>_Executes/QueriesOutput/ResponseSymbolic TraceSymbolic ExecutorJavaAttachesbetween Symbolic Explorer and SuT in symbolic loop (green)Direct interaction between Symbolic Explorer and SuT in symbolic loop (green)No direct interaction Newinputs

Active Mode

When running SWAT in active mode (i.e. for SV-Comp) the symbolic explorer doubles as the driving harness for the SuT. This means that the symbolic explorer directly interacts with the SuT either by sending requests to drive new executions or by starting the SuT and providing the new values. Correspondingly, the main (symbolic execution) loop is between the symbolic explorer initiation new executions and the instrumented SuT providing new traces and constraints. This is highlighted in green in the above figure. The Active Mode page provides a more in-depth explanation of this mode and how to use it.

Passive Mode

The passive mode is not yet added to this repository, but will be added soon!

When running SWAT in passive mode, the symbolic explorer is only responsible for receiving trace data and maintaining the execution tree. I addition endpoints are exposed that allow the user/ harness to initiate symbolic exploration and consequently gain new instantiations of the symbolic variables that lead to unexplored regions in the SuT.

This mode pairs well with, i.e., HTTP fuzzers. Here the fuzzer has to be adapted to receive new values for the fuzzable variables from the symbolic explorer.

Table of contents