BGP Simulation & Traffic Engineering via Z3 SMT Solving

A formal-methods approach to network routing analysis: encoding BGP best-path election, parameter inference, global traffic engineering, and resilient traffic engineering as constraint-satisfaction problems and solving them with the Z3 SMT solver.

University project — Computabilità, Complessità e Logica (Computability, Complexity, and Logic)
B.Sc. AIDA · Year 2 · Semester I · UniTS

---

Overview

The project implements a Python toolkit that models the Border Gateway Protocol (BGP) decision process at four levels of increasing complexity, each accompanied by a formal complexity certificate:

Module	Problem	Complexity
decision.py	Primal — elect the best BGP route	O(N) — P
dual.py	Dual — infer parameters to make a target route win	O(N) — P
te.py	Global Traffic Engineering — assign parameters so no link exceeds 90% utilisation	NP-complete
rte.py	Resilient TE — same as TE but robust to up to k simultaneous link failures	NP-complete (fixed k) / Σ₂ᴾ-complete (k as input)

The main entry point is the Jupyter notebook BGP_Simulation.ipynb, which walks through all four problems with worked examples and interactive traces.

---

BGP Decision Process

The toolkit implements RFC 4271 §9.1.2 best-path selection restricted to the following four criteria (in priority order):

Step	Attribute	Winning condition
1	LOCAL_PREF	Highest wins
2	AS_PATH effective length	Shortest wins (base + prepend count)
3	MED	Lowest wins
4	Router-ID	Lowest wins (deterministic tie-break)

---

Repository Structure

BGP_Z3/
├── BGP_Simulation.ipynb   # Main Jupyter notebook (71 cells)
└── bgp/                   # Python package
    ├── __init__.py
    ├── models.py           # BGPRoute dataclass
    ├── decision.py         # Primal: best-path election (O(N))
    ├── dual.py             # Dual: parameter inference via Z3 Optimize
    ├── te.py               # Global Traffic Engineering (NP-complete)
    ├── rte.py              # Resilient TE with failure scenarios
    ├── display.py          # Terminal pretty-printing utilities
    ├── nb_display.py       # Notebook-specific display helpers
    ├── te_display.py       # TE result display
    ├── rte_display.py      # RTE result display
    └── topology_plot.py    # Network topology visualisation (matplotlib)

---

Quick Start

1. Create and activate a virtual environment

python3 -m venv .venv
source .venv/bin/activate   # Windows: .venv\Scripts\activate

2. Install dependencies

pip install -r requirements.txt

---

Module API

Primal — best-path election

from bgp import BGPRoute, best_path, best_path_with_trace

routes = [
    BGPRoute("R1", "10.0.0.0/8", local_pref=200, as_path=[65001], router_id="1.1.1.1"),
    BGPRoute("R2", "10.0.0.0/8", local_pref=100, as_path=[65002], router_id="2.2.2.2"),
]

winner = best_path(routes)                        # → BGPRoute("R1", ...)
winner, steps = best_path_with_trace(routes)      # also returns elimination trace

Dual — parameter inference

from bgp import solve_dual

result = solve_dual(
    routes     = routes,
    target_id  = "R2",
    free_params = {"R2": {"local_pref"}},   # let Z3 choose R2's LOCAL_PREF
)
# result.satisfiable → True
# result.assignments → {"R2": {"local_pref": 201}}

Traffic Engineering

from bgp import Link, TrafficDemand, RoutePath, solve_te

links   = [Link("A", "B", capacity=1000), ...]
demands = [TrafficDemand(ingress="A", prefix="10.0.0.0/8", volume_mbps=600)]
paths   = [RoutePath(route, physical_path=[...]), ...]

result = solve_te(links, demands, paths, free_params={...})

Resilient Traffic Engineering

from bgp import generate_failure_scenarios, solve_rte

scenarios = generate_failure_scenarios(links, k=1)   # all single-link failures
result    = solve_rte(links, demands, paths, free_params={...}, k=1)

---

Complexity Summary

Problem	Hardness	Key argument
BGP Best-Path (Primal)	P (O(N))	Lexicographic total order → linear scan
Parameter Inference (Dual)	P (O(N))	Greedy level-by-level fix; Z3 used for generality
Global Traffic Engineering	NP-complete	Reduction from 3-PARTITION; winner-takes-all discrete routing
Resilient TE (fixed k)	NP-complete	Contains plain TE; O(|E|^k) scenarios, each poly-checkable
Resilient TE (k as input)	Σ₂ᴾ-complete	∃∀ quantifier alternation; verifier itself NP-hard

See the notebook for the full in-code analysis with pseudocode and encoding details.

---

Dependencies

Package	Role
z3-solver	SMT solving for Dual, TE, and RTE
matplotlib	Topology plots

---

References

• RFC 4271 — A Border Gateway Protocol 4 (BGP-4), §9.1.2 Decision Process
• Garey & Johnson (1979) — Computers and Intractability, 3-PARTITION (SP15)
• de Moura & Bjørner (2008) — Z3: An Efficient SMT Solver