summary of tests currently implemented
verifies various correctness aspects of BGP configuration
browse config summaries at a high level
implementation: planned features, schedule, etc.
installation and usage information
contact us: send us feature requests, etc.
|papers and talks||-||
papers, talks, and more work on routing at MIT
Download, setup instructions, usage examples, demonstrations, etc., can be found in the manual.
The state of the art for router configuration typically involves logging configuration changes and rolling back to a previous version when a problem arises. The lack of a formal reasoning framework means that router configuration is time-consuming and ad hoc. Network operators need tools based on systematic verification techniques to ensure that BGP's operational behavior is consistent with the intended behavior (i.e., that the network is operating ``correctly''). We are designing a verification tool based on a new reasoning framework that helps operators and protocol designers reason about high-level properties of routing protocols.
Currently, the verification tool has the following two components:
rcc parses router configuration into a vendor-independent, intermediate format, represented as relational database tables.
New: Support for IGP. See the list of tests for more detail. We would like to eventually add support for other routing configuration languages and welcome assistance in doing so!
To-do list (planned features, etc.) (Updated 10/24/2005)
We could really use operator help in any of the following ways:
You can provide feedback here, or you may contact bgp-config at the domain nms.lcs.mit.edu.