This organization maintains and organizes the Princeton Programming Languages group's network verification tools and systems.
These tools and systems include:
- nv, a network control plane intermediate representation language and analysis tool
- angler, a tool for exporting Batfish representations of network configuration files, for use by other systems
- Timepiece, a modular network control plane verification tool
Install prerequisites: Docker, python and python-poetry, and dotnet.
- Acquire your network's configuration files.
The angler repository contains some examples.
We'll imagine we have a directory "
EXAMPLE" containing a subdirectory "configs" with these files.
ls EXAMPLE/configs
# should output something like:
# file1.cfg file2.cfg file3.cfg ...- Start the
batfishDocker service.
docker run --name batfish -v batfish-data:/data -p 8888:8888 -p 9997:9997 -p 9996:9996 batfish/allinone
# after the first run, you can start it again using "docker start batfish" or "docker restart batfish"- Extract the JSON representation of the Batfish AST using angler.
cd angler
poetry install
poetry run python -m angler --full-run --simplify-bools EXAMPLE
# you should obtain an [EXAMPLE.json] Batfish JSON file
# and an [EXAMPLE.angler.json] Angler JSON file as output
# you can also perform these two steps separately by running
# poetry run python -m angler EXAMPLE
# followed by
# poetry run python -m angler --simplify-bools EXAMPLE.json- Verify your desired property of the network using Timepiece.
cd Timepiece
dotnet build Timepiece.Angler
dotnet run --project Timepiece.Angler -- run EXAMPLE.angler.json [query]- How do I make changes to how Angler represents the Batfish AST?
Modify the Batfish AST files in angler. See https://github.com/NetworkVerification/angler/tree/main/angler/bast. - How do I make changes to Angler's AST, or how Angler simplifies the Batfish AST to the Angler AST?
Modify the Angler AST files or the conversion code in angler. See https://github.com/NetworkVerification/angler/tree/main/angler/aast and https://github.com/NetworkVerification/angler/tree/main/angler/convert.py. - How do I make changes to how Timepiece models the Angler AST?
Modify the Timepiece.Angler AST or the AST-to-Zen encoding - How do I make changes to what properties Timepiece can check on an Angler file?
Add a new QueryType for your property, then add code to Program.cs to define how to construct an AnnotatedNetwork that checks the desired property.