Octopus

Octopus is an equivalence checker for P4 packet parsers, implemented in Python.
Its implementation uses symbolic bisimulation to compare parser behaviour.

Octopus is accompanied by the paper "Octopus: Practical Equivalence Checking of P4 Packet Parsers" by Jort van Leenen and Tobias Kappé. This work builds on the first author's bachelor's thesis "Practical Equivalence Checking of P4 Packet Parsers", supervised by Tobias Kappé and Jan Martens. The implementation builds on theoretical work from Leapfrog, a Rocq-based formal verifier for P4 packet parsers.

Features

• Equivalence checking for P4 packet parsers using (optimised) symbolic bisimulation;
• Support for IR (JSON) format from p4c-graphs;
• CLI interface with structured output.

Limitations

• Only a subset of P4_16 constructs and features are supported.

Dependencies and Compatibility

Octopus depends on the p4c-graphs tool to generate the IR JSON representation of P4 programs.

• Tested with: p4c-graphs version 1.2.x.x;
• Requires: Python 3.12 or later; tested up to 3.13.

Ensure p4c-graphs is available on your system's PATH if you provide P4 programs as input.

Docker

Octopus is available as a prebuilt Docker image, hosted on Docker Hub.

To download the image:

docker pull jortvanleenen/octopus:latest

You can verify the installation by performing a self-check on a simple P4 program:

docker run --rm jortvanleenen/octopus:latest \
  tests/correct_cases/hello-octopus.p4 tests/correct_cases/hello-octopus.p4

This should confirm that Octopus is functioning correctly.

To check your own P4 programs, mount a local directory (e.g., the current working directory) into the container. The example below mounts the current working directory to /workspace and sets that as the working directory:

docker run --rm -v "$PWD:/workspace" -w /workspace jortvanleenen/octopus:latest \
  [OPTIONS] FILE1 FILE2

The image includes the cvc5 SMT solver preinstalled. To install additional solvers, or to run custom PySMT configurations, use an interactive shell:

docker run -it --rm --entrypoint /bin/bash jortvanleenen/octopus:latest

You can then, for example, use pysmt-install to install SMT solvers. For more information, see the manual installation instructions below.

Manual Installation

To install Octopus, the following steps can be followed. Step 6 installs the project in editable mode, including development dependencies. Feel free to customise this step according to your needs. For example, one could decide to install only the runtime dependencies by removing [dev].

# 1. Clone the repository
git clone https://github.com/jortvanleenen/Octopus.git
cd Octopus

# 2. Create a virtual environment
python3 -m venv .venv

# 3. Activate the virtual environment
source .venv/bin/activate

# 4. Upgrade pip
pip install --upgrade pip

# 5. Install Hatch (build + env management tool)
pip install hatch

# 6. Install the project with dev dependencies
pip install -e .[dev]

Following the above instructions should make the octopus command available in your environment.

To use symbolic bisimulation, at least one SMT solver has to be installed locally. PySMT provides the pysmt-install command to make doing this simple.

For example, to install Z3 and cvc5, run: pysmt-install --cvc5 --z3. Afterwards, pysmt-install --check can be used to verify the installation.

Usage

octopus [OPTIONS] FILE1 FILE2

FILE1 and FILE2 are paths to the two P4 programs to compare. These can be either .p4 source files, or IR JSON files produced by p4c-graphs. One has to provide the -j option to Octopus in the latter case.

Examples

Check two IR JSON files (using symbolic bisimulation):

octopus -j parser1.json parser2.json

Check two P4 source files (Octopus invokes p4c-graphs internally):

octopus program1.p4 program2.p4

Use symbolic bisimulation with leaps disabled:

octopus program1.p4 program2.p4 --disable_leaps

Write output (certificate or counterexample) to a file:

octopus -j parser1.json parser2.json --output result.txt

Exit with status code 1 if the parsers are not equivalent:

octopus -j parser1.json parser2.json --fail-on-mismatch

Note: this is useful for scripting or CI/CD pipelines.

Print bisimulation execution time and memory usage:

octopus -j parser1.json parser2.json --stat

Customise the SMT solver portfolio and provide (global) options:

octopus -j p1.json p2.json \
--solvers '["z3",("cvc5",{"incremental":False})]' \
--solvers-global-options '{"generate_models":False}'

Note: evaluation of the options is done using ast.literal_eval(), so the argument must be a valid Python literal. For --solvers, the following object is accepted: list[str | tuple[str, dict[str, Any]]]. For --solvers-global-options, the following object is accepted: dict[str, Any].

Perform external filtering by specifying an additional constraint that must hold for accepting pairs:

octopus p1.p4 p2.p4 \
"hdr_l.field0 == (hdr_r.field1 + hdr_r.field2) and hdr_l.field0[15:0] == '0xABCD_16' and True or False"

Note: a (larger) constraint can also be specified using an external file with the --filter-accepting-file option. Evaluation of these options is done using ast.parse() (mode eval), so the argument must be a valid Python expression.

Similarly to above, a constraint can be provided that should hold for disagreeing pairs using --filter-disagreeing-string and --filter-disagreeing-file respectively.

CLI Options

Octopus provides a command-line interface (CLI) with the following options:

Short	Long	Description
-h	--help	Show a help message and exit
	--version	Show the version of Octopus and exit
-j	--json	Specify that both inputs are in IR (p4c) JSON format
	file1	Path to the first P4 program
	file2	Path to the second P4 program
-v	--verbosity	Increase output verbosity (-v, -vv, -vvv)
-L	--disable_leaps	Disable leaps; only use single-step bisimulation
-o	--output	Write the bisimulation certificate or counterexample to the specified file
-f	--fail-on-mismatch	Exit with code 1 if the parsers are not equivalent
-S	--stat	Measure and print bisimulation execution time and memory usage
-s	--solvers	Specify which SMT solvers to use along with their options
	--solvers-global-options	Specify global options for all solvers
	--filter-accepting-string	Define an additional constraint for accepting pairs via a string.
	--filter-accepting-file	Define an additional constraint for accepting pairs via an external file.
	--filter-disagreeing-string	Define an additional constraint for disagreeing pairs via a string.
	--filter-disagreeing-file	Define an additional constraint for disagreeing pairs via an external file.

Verifying Claims and Benchmarking

To verify the claims made in the paper, you can run the benchmark scripts, which are also included in the Docker image. These scripts will execute the equivalence checks and output the relevant results.

• See tests/runner.py for the Leapfrog and Whippersnapper benchmarks. Execute the script with --help, for more details.

• See tests/plotter.py for the figure generation part of the Whippersnapper benchmarks, including the raw data that was used to generate this.

• See tests/programs-survey-exp.py for the code responsible for statistics and equivalence class generation over the p4-programs-survey parsers.

As an example of how to run the benchmarks, run the container interactively and execute the following command:

python3 tests/runner.py -o o.txt

To add benchmarks or test cases, see the tests directory. Within this directory, you can find subdirectories for correct cases, incorrect cases, and benchmarks. Additionally, a template file has been provided (tests/framework_template.p4) to help you get started.

Leapfrog Benchmarks

The benchmark set is taken from Doenges et al. (2022). As our manner of input differs from theirs, we have provided a mapping from our folder names to their benchmark filenames.

• States denotes the total number of states in both parser programs.
• Branched is the number of bits tested in all transition select statements.
• Total is the total number of bits across all variables.

Category	Name	File	States	Branched (b)	Total (b)
Utility	State rearrangement	IPFilter	5	8	256
	Variable-length format 2	IPOptions2	30	32	672
	Variable-length format 3	IPOptions3	45	96	672
	Header initialisation	SelfComparison	10	12	736
	Speculative extraction	MPLSVectorized	5	3	192
	Relational verification	SloppyStrictStores	6	32	1056
	External filtering	SloppyStrictFilter	6	32	1056
Applicability	Edge	EdgeSelf	28	52	2584
	Service provider	ServiceproviderSelf	22	25	2536
	Datacenter	DataCenterSelf	30	274	2272
	Enterprise	EnterpriseSelf	22	80	1952
	Translation validation	EdgeTrans	30	56	3036

Notes

• Full filenames in Leapfrog are <name-in-table>Proof.v, except for SloppyStrictStores and SloppyStrictFilter, which are as is.
• The Leapfrog GitHub repository incorrectly lists EthernetProof.v as the benchmark file for state rearrangement.
• The number of branched and total bits has been corrected for most benchmarks, as these were incorrect in the Leapfrog paper.
• In Leapfrog's Enterprise benchmark, the size of the IPv4 header was incorrectly specified. We were able to adjust this to the correct value by looking at the original code in the parser-gen repository.

License

This project is licensed under the MIT License. See the LICENSE file for details.