Verification of routing policies by using model checking technique

BGP, the de-facto inter-domain routing protocol, is well-known for its complexity in configuring correct behaviour. This stems from the fact that the protocol is policy-based. Despite best practice and guidelines, it is not uncommon to have policy conflicts in a real network. Currently, there is a lack of tools to verify that required properties, especailly, the convergence property, holds in a set of BGP configurations. This paper presents an approach to verifying BGP routing policy configurations by using a mathematical-rich technique, model checking. The experiments on sample network configurations are demonstrated. The convergence property are verified by using two linear temporal logic (LTL) formulas. The experimental results has shown that it is possible to conclude, based on the results of the verification, whether or not a set of BGP routing policy configurations will converge on a solution for a particular network destination.