Detecting the unintended in BGP policies

Internet Service Providers (ISPs) use routing policies to implement the requirements of business contracts, manage traffic, address security concerns and increase scalability of their network. These routing policies are often a high-level expression of strategies or intentions of the ISP. They have meaning when viewed from a network-wide perspective (e.g., mark on ingress, filter on egress). However, configuring these policies for the Border Gateway Protocol (BGP) is undertaken at a low-level, on a per router basis. Unintended routing outcomes have been observed. In this work, we define a language that allows analysis of network-wide configurations at the high-level. This language aims at bridging the gap between router configurations and abstract mathematical models capable of capturing complex policies. The language can be used to verify desired properties of routing protocols and hence detect potential unintended states of BGP. The language is accompanied by a tool suite that parses router configuration languages (which by their nature are vendor-dependent) and translates them into vendor-independent representations of policies.