Skip to content

A static analysis tool over the data plane state of networking devices

License

Notifications You must be signed in to change notification settings

haohui/anteater

Repository files navigation

Anteater is a tool that detects networking bugs through static analysis of the data plane state of the networking devices. Anteater translates high-level network invariants into boolean satisfiability problems (SAT), checks them against network state using a SAT solver, and reports counterexamples if violations have been found.

For more information please read the paper published in SIGCOMM'2011:

Haohui Mai et al. Debugging the data plane with Anteater. In the Proceedings of the ACM SIGCOMM 2011 conference.

Building

Anteater requires the following dependency to build and run:

  • CMake 2.6 or higher
  • LLVM 2.9
  • Boost 1.42
  • Coreutils
  • A SAT solver (currently Anteater supports Boolector, Yices and Z3)

To build Anteater:

$ cmake
$ make

You can find the invariant checkers described in the paper under the tools/scripts directory and run them to detect networking issues.

Contribution

Your pull requests are appreciated!

About

A static analysis tool over the data plane state of networking devices

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published