BGP State Iterator

This repository contains the implementation and evaluation of the BGP State Iterator, published in ICNP'25.

Usage

The state iterator is a library intended to be used directly through its API. See the provided examples, and consider the documentation. The documentation can be generated with:

cargo +nightly doc --open

Evaluation

The binary eval can run the entire evaluation of the paper "Guided Exploration of Control-Plane Routing States". The kind of experiment and the number of repetitions are passed as arguments:

cargo run --release --bin=eval --features=eval -- --help

This produces the following help message:

Usage: eval [OPTIONS]

Options:
  -p, --parallel
  -t, --topo <TOPO>              [default: Colt]
  -s, --seeds <SEEDS>            [default: 5]
      --shuffle
  -e, --experiment <EXPERIMENT>  [possible values: network-size, num-peers, config-complexity, router-order, verification, link-failure]
  -h, --help                     Print help

• The experiment to run is passed with the -e flag. The experiments correspond with all experiments conducted in our evaluation.
• Use -p to run multiple scenarios in parallel (will use all available threads). Notice that every experiment is run on a single thread.
• You can modify the topology. This argument is ignored for the experiment network-size.
• Use -s to shuffle the experiments. This can give you a better estimate of how long the experiment will take. Usually, the smaller experiments are at the beginning, and the larger ones are at the end.

All results will be stored to the measurements folder.

Remark: For -e verification, the program will run the task on our re-implementation of Minesweeper. The re-implementation can be found in bgpsim-smt. Make sure to have Z3 installed.