The Internet paths connecting independently operated networks, also called domains or autonomous systems (ASes), are driven by semantically rich policies: the interdomain routing protocol that computes the Internet paths allows the ASes to influence path selection with their local policies, such as economic concerns or operational constraints. An AS can promote a policy compliant but globally longer path by carefully tweaking lower level path attributes that are used in the routing protocol. Such operational policies are notoriously complex and hard to understand. This paper takes a step back and asks whether a more principled logical approach can lead to AS policies that are easier to understand, reuse, evolve, and coexist. To this end, we propose to represent policies by database integrity constraints, in the form of headless datalog rules about what are the acceptable Internet paths. The simple datalog expression unifies a wide spectrum of AS policies, ranging from classic examples seen in today's routing practice to futuristic ones proposed in various extensions to Internet routing. More importantly, by leveraging datalog's connection to the theorem proving technique called the residue method, we developed a new technique for understanding the interactions among the policies - whether a policy can inadvertly affect another, and how to resolve the conflict. We also evaluated our logical policies, showing promising result with small overhead for conflict resolution on realistic large networks.
The Internet today is more than connecting remote hosts with valid paths. Rather, it is
a unique artifact connecting independently operated networks 1, also called domains or
autonomous systems (ASes), with rich AS-set policies [
Alongside the growing support for more flexible AS policies, the policy expression in terms of the route attributes remains largely ad hoc — the choice and use of the attributes are often arbitrary. For example, the AS Path (ASP) attribute — a list of ASes (each identified by a number) along the AS-level path — can implement the shortest path policy: when a route is first imported, the network attaches its own AS number to the AS Path, selects a best route with the shortest ASP, and exports to its neighbors this best route. However, a network can arbitrarily increase the length of ASP by appending its AS number multiple times to to make a longer path more preferable. An alternative to achieve the same affect is to leverage the Local Preference (LP) attribute which is compared first in route selection and thus overrides ASP: a network can promote the use of a longer path by assigning to it a higher LP. But LP is highly abused: many policies of disparate policies translate to LP only because it outweighs everything else.
Besides, a network is often influenced by many policies — separate teams within the network may issue policies addressing disparate aspects of the network, neighboring networks might also exercise policies that attempt to influence its route selection. These policies can interact in complex ways and run into subtle conflicts. The onus of combining them into a coherent route selection policy is left to the network admin who is required to carefully examine every component policy as well as their joint intent. For example, a security policy for avoiding a suspicious neighbor and an optimization policy for reducing route cost, though concerning distinct aspects of the network, can conflict due to the underlying topology: a router that connects a low-cost internal path (within the local network) to the suspicious neighbor can correlate the two policies with distinct purposes. In the presence of such conflicts, the admin must carefully re-factor and/or reset the corresponding policy attributes that are used in the prefixed BGP protocol.
Indeed, it is generally agreed that the policy practice of the Internet today, tightly coupled with the BGP protocol, is indirect and hard to understand. This paper takes a step back and asks whether a more principled logical approach can lead to policies that are easier to understand, reuse, combine, and evolve?
To this end, we investigate the use of database integrity constraints (ICs) — in the form of headless datalog rules about what are the preferable paths — for managing routing policies. The key idea is that, rather than treating policy making and route decision as a procedure that maps a set of incoming routes to one single best (outgoing) route, we view policies as logical constraints that prune the candidate routes until only the best route is left 2. To validate its feasibility, we study the expressiveness and overhead of the IC representation with extensive case studies and experiments. More importantly, we show the benefits of this logical approach by a new conflict detection and resolution technique via the theorem proving technique called the residue method. Overall, we believe this is a first step towards a more principled approach to interdomain routing policies with automated reasoning support.
Specifically, this paper makes the following contributions: 2 Or break tie by randomly select one route from a set of equally good routes We introduce database ICs as a logical representation for routing policies. Through extensive examples ranging from classic network policies to futuristic ones, we show how the IC representation unifies many disparate policies.
We leverage and extend the residue method to study interactions and conflicts among policy ICs: we present a formal characterization of policy conflicts in terms of the notion of policy residue, a fragment of a policy that anticipates its impact on the other policies. To our best knowledge, this is the first formal attempt to characterize multiple routing policies that jointly control the same path. Our formalization is logically checkable and enables conflict detection. It also offers a method of conflict resolution with rewrites — when augmented with the residue, a potentially conflicting policy is semantically constrained and resolves conflict. We study the performance overhead of the proposed logical policies by evaluating a prototype of the residue method. Our result is promising, the conflict resolution delay is < 100ms for large policies. 2
This section develops a logical representation that attempts to unify a wide range of policies previously buried in disparate route attributes. More importantly, the representation will enable automated reasoning as a means to understand and combine policies, laying a firm foundation for automated conflict resolution 4.
We propose to represent network policies as database integrity constraints (ICs). We draw on the insight that viewing the network state as factual data — database tables and views — allows us to capture network policies as non-factual data — semantic information or ICs about what are the acceptable data.
A factual network state is a finite set of ground facts, denoted by I. We can also derive new information from the network state by rules, denoted by R. The complete network state is denoted by N = R [ I. Suppose N always includes ground facts from the two route relations ri=3; ro=3, both of which have three attributes destination; next hop and path vector. ri(x; y; z) stands for an incoming route learned from a neighbor y to reach a destination x by a path z (the list of ASes along the path to x). ro stands for the output route selected by the network’s routing policy.
For example, a network state that has 3 incoming routes and 2 outgoing routes is represented by the ground rules I1 5, the derived information of all available paths to a particular destination 1.2.3.4 is represented by the rule R1.
Network facts I1: ri(1.2.3.4, router1, [AS2,AS3,AS5]) :I2: ri(1.2.3.4, router2, [AS2,AS4,AS5]) :I3: ri(1.2.3.5, router1, [AS3,AS5]) :I4: ro(1.2.3.4, router2, [AS2,AS4,AS5]) :I5: ro(1.2.3.5, router1, [AS4,AS5]) :Derived path information R1: rpath(z) :- ri(x,y,z), x=1.2.3.4.
A routing policy is a finite set of ICs, denoted by P . We divide the policy ICs into two categories: the generative ICs whose head is non-empty, and denial ICs whose head is empty. In particular, a denial IC can be read as a body condition — conjunction of literals that cannot be simultaneously true — that must be avoided for any correct network state; a generative IC can be read as a head condition that must also hold if the network state is consistent with the body condition. A basic requirement for any routing system is path validity — any selected outgoing route must also correspond to some incoming route. A network cannot invent a route that does not belong to it. This can be captured by a path validity policy encoded by the generative IC Pvalidity, equivalently, it can be formulated as the denial IC Pvalidity0 .
Path validity policy ICvalidity: ri(x,y,z) :- ro(x,y,z).
ICvalidity’: :- ro(x,y,z), :ri(x,y,z). 2.2
In this section, we use more examples to illustrate the expressiveness of the IC representation.
Many policies can be specified as constraints over a single path. For example, a source host might want to specify the explicit path (a) for carrying traffic to certain destination (d), to better control end to end performance, as expressed by the simple and direct ICcp.
Complete path policy ICcp: z=a :- ro(x,y,z), x=d.
Another popular policy regulates route selection based on the business relations of
the neighboring networks. A network often engages in one of three business relations
with its neighbors [
ICGR1 GR2 prevents the selection of a provider path when there exists a customer or peer path, respectively. Note that the operational expression of the Gao-Rexford policy in traditional BGP is a classic use case of the local preference (LP) attribute: the network needs to always attach a higher LP to the customer / peer paths as compared to the provider paths. In comparison, our declarative policy is not only more direct — we do not need to coordinate the LP attribute assignment, it is also inherently more flexible. When bound to LP, Gao-Rexford will override any other policies as LP overrides all the rest of the attributes. For example, it will be hard to add a security policy even though it might carry more weight than the economic concerns. In contrast, the declarative policy allows us to add new policy and freely combine it with the existing ones with automated conflict detection and resolution (more in x4).
Our logical approach also easily captures futuristic BGP policies introduced in
experimental BGP extensions. For example, MIRO [
ICMIRO :- ro(x,y,z), waypoint(z,b).
The foregoing examples are all non-aggregate policies in the sense that they are expressible as constraints along a single route. Next, we illustrate how to formulate aggregate policies concerning a group of routes without the explicit use of an aggregate term. First, consider the shortest path policy. Among all candidate paths connecting a pair of source and destination, shortest path policy picks a path that traverses the fewest number of networks. With the help of an auxiliary function l(path) which returns the length (number of ASes along the path) of the path, shortest path policy translates to ICsp.
Shortest path ICsp :- ro(x,y,z), ri(x,y’,z’), l(z)>l(z’).
Now consider a complex futuristic policy with aggregation. Wiser [
where the RW iser rule derives the joint cost of two path fragments and ICW iser forbids the selection of a route when there exists a better alternative (w>w’). 3
An advantage of the IC representation is that it facilitates automated reasoning of the
policies — predicating the interactions of multiple policies that jointly select paths. The
key idea is to leverage the residue method [
Given two policies C1; C2 of the form A1 :- B1 ^ B10 and A2 :- B2 ^ B20, respectively, where B1; B2 are conjunctions of relational literals and B10; B20 are conjunctions of comparison and arithmetic formulas, C1 subsumes C2 if there exists (1) a solver S for arithmetics and comparison, and (2) a substitution such that each literal in (A1 :- B1) occurs in A2 :- B2 and :B20 ^ B10 can be reduced to False by S. Intuitively, subsumption means policy C1 is more general — stronger — than C2, that is, any network state compliant with C1 is guaranteed to be compliant with C2.
For example, consider the IC clauses IC1; IC2: IC1: :- ro(x,y,z), l(z)<5.
IC2: :- ro(u,v,w), l(w)<3, w=[AS2,AS3].
IC1 subsumes IC2 with respect to a solver that is capable of arithmetic comparison because: (1) There is a substitution = fx = u; y = v; z = w that makes :- ro(x,y,z) a subclause of :- ro(u,v,w), l(w)<3 and (2) :((l(z) < 5) ) ^ (l(w) < 3) can be reduced to l(w) > 5 ^ l(w) < 3 which is False.
What interests us is partial subsumption: C1 partially subsumes C2 if there exists a subclause of C1 that subsumes C2. Partial subsumption means the subsuming policy has a non-trivial impact on the policy being subsumed. To precisely capture such impact and to anticipate how such impact modifies another policy, we leverage the notion of residue.
A residue is a fragment of a subsuming IC that actually interacts with the subsumed
IC. Residue can be obtained by the subsumption algorithm developed in [
IC3 :- ro(x,y,z), l(z)<5.
:- l(w)<5 null elements of IC2
:- ro(u,v,w) {x=u,y=v,x=w}
:-l(w)<3 l(w)>5 ∧ l(w)<3 reduces to False
ICcp z=a :- ro(x,y,z), x=d w=a :- u=d elements of IC2
:- ro(u,v,w) {x=u,y=v,x=w}
The residue precisely anticipates the policy “impact”. The “null” residue on the left shows that IC3 is stronger than IC2 (more details in x 4); on the other hand, the nontrivial residue w=a :- u=d (right in the Figure) states that the condition w = a u = d must be taken into account when applying IC2: any route to d must take a as the selected path.
In general, a non-trivial residue obtained on a subsuming policy C1 and a subsumed policy C2 states a condition that must be satisfied for C2 to be consistent with C1. This observation allows us to use the residue of C1 to semantically constrain (transform) C2. We only need to attach the residue condition to the body of C2. The result is a new policy C20 that is guaranteed to be compliant with C1. For example, Annotating IC2 with the residue of ICcp produces: IC2 semantically constrained by Ccp: :- ri(u,v,w),l(w)<3,w=[AS2,AS3],w = a u = d. 4
This section developed a residue based method to understand the interactions between policy ICs 3. Specifically, using the notions of (partial) subsumption and residue, we give a formal characterization the relations among two policies. We also give a resolution method that automatically merges potentially conflicting policies.
First, we introduce a formal concept called covering to denote when a policy is stronger than another. One policy covers another if it subsumes the second policy. Intuitively, one policy is stronger if compliance with the first policy implies compliance with the second. For example, Consider a more specific form of shortest path policy that only finds shortest path to certain destinations, with a new relation only(destinations) standing for those destinations. We express this restricted shortest path policy by ICspr as follows ICspr :- ro(x,y,z), ri(x,y’,z’), l(z)>l(z’), only(x). The shortest path policy ICsp subsumes ICspr, thus it covers the more specific policy. Intuitively, all the shortest paths must also include the shortest path to those particular destinations.
What is more interesting is partial covering: one policy partially covers another if a subclause of the first policy covers the second. Partial covering signals conflicts — two policies overlap but neither one of them is redundant. Consider two pairs of policies — shortest path and complete path, MIRO and Wiser (in x 2). For each pair, the policies are conflicting with each other. It is straightforward to spot conflicts between simple policies like shortest path and complete path, but the conflicts between MIRO and Wiser is subtler. The formal characterization of conflicts via residue reasoning helps to guard against missing a subtle conflict.
Conflict resolution in the Internet today is manual and operational: the network admin must understand the combined effort of all policies and refactor them into a hard wired list of route attributes that will be compared in a fixed order during the route selection process. In contrast, in this paper, we propose a facility that, takes a set of conflicting policies as input, generates a new coherent set by the semantic transformation process with the residue method. Between any pair of conflicting policies, the residue method rewrites the policy with lower priority, semantically constraining it with the other one with higher priority. Thus, the resolution facility automatically resolves conflicts by policy rewriting, freeing the admins from manual policy coordination.
Specifically, for two policies ICi; ICj , we use ICj jICi , to denote the semantically restricted version of ICj with respect to ICi, which is obtained by augmenting ICj with the residue of ICi. When ICi enjoys higher priority over ICj — ICi is perceived more important, we can simply keep ICi unchanged but compute ICj jICi to rewrite ICj to the restricted form, forcing ICj to also account for the concerns of ICi. Note that, by definition, ICi covers ICj . The resulting pair (ICi; ICj jICi ) can be viewed as a ranked list of policies where ICi takes effect first, and the original ICj follows.
For example, consider the complete path (ICcp) and shortest path (ICsp) policies. To obtain a shortest path policy that finds shortest path to all destinations except d, the path to which is pre-defined to be a, we can apply the residue method to obtain ICspjICcp (the residue augmented in red): :- ro(x,y,z), ri(x,y’,z’), l(z)>l(z’), :(x = d ^ z 6= a). Thus, we obtained a shortest path policy that yields to the specific path assignment of the complete path policy.
Similarly, consider the MIRO (ICMIRO) and Wiser (ICW iser) policies. A network that deploys both but prioritizes the MIRO policy — security concern over performance — can apply our resolution method to obtain the MIRO constrained Wiser policy ICW iserjICMIRO : :- ro(x,y,z), j(x,y,w), j(x,y’,w’), w>w’, :waypoint(z,b). With ICW iserjICMIRO , the Wiser portion (first 4 literals) will take effect only when the MIRO residue evaluates to true (when MIRO policy is honored). That is, performance concern kicks in only after security requirement is satisfied. 5
We evaluate the performance of our proposed logical policies in Ravel [
To measure the overhead of the residue method, we implemented a prototype of
the subsumption algorithm based residue generation in Python: for a given subsuming
clause (denoted by P1, has M literals) and a clause being subsumed (denoted by P2, has
N literals), we loop over all the subclauses of P1 and test if the subclause subsumes P2.
We applied the standard -subsumption algorithm to implement the subsumption test,
which has complexity O N k as we need to map each literal of the subclause (ranging
from 1 to k for a subclause with k literals) to a literal in P2 (ranging from 1 to N) [
We evaluated the performance of our residue generator with MIRO and Wiser policies. To test its scalability, we increased the number of waypoint literals in MIRO policy with randomly generated networks (to avoid). 0.266 0.705 delay Fig. 3: Residue generation for Wiser and MIRO. y a l e d
Figure 2 shows the residue generator processing delay (y axis, log scaled) for two MIRO policies with different size combinations (as indicated by the tuple below the x axis). For each combination, we plotted the average delay of 500 runs. The small bar on the top of each box indicates the standard variation. The left three boxes with grey filling show the growing trend of delay with respect to N — M is fixed at 2; and the right three boxes with grids filling show the growing trend with respect to M — N is fixed at 2. When M is fixed, the residue generator scales better — even for P2 having very large size of 64, it finishes in 3.356 ms on average. The delay, however, increases exponentially with M — the delay grows from 0.268ms to 37.102ms when M increase from 2 to 8.
Figure 3 presents the CDF of the residue generator processing delays (x axis, log scaled) for constraining MIRO policy with a Wiser policy — The Wiser policy has 6 literals (N = 6), and the MIRO policy has (M ) has varied size of 2, 4 and 8. For all three sizes, 99% of all the processing finished within 0.266ms, 0.705ms and 10.524ms respectively. Note that the performance here is better than that of Figure 2 — for example, the average delay is less than 10ms for M = 8 and N = 6 compared to the average delay of 37.10ms for M = 8 and N = 2. This is because the MIRO policy shares only one common predicate with the Wiser policy, i.e., the relation ro, which led to a faster result from subsumption test. 6
Closest to our IC representation of routing policies is declarative networking [
Many proposals [
In this paper, we developed a logical approach to Internet routing policies. Rather than
burying policies in the route attributes that are manipulated by the prefixed BGP
protocol, and relying on the network admin for manual configuration, we introduce database
integrity constraints (ICs) [