Specifying and compiling internet routing protocols

This dissertation describes a system that allows routing languages to be specified in a declarative style. These specifications can then be compiled into low-level code and combined with one of several pre-supplied routing algorithms to producing routing protocol implementations. The system contains two types of routing algorithms: offline and online. Offline algorithms are variants of traditional shortest paths algorithms such as Dijkstra’s algorithm, and allow the computation of routing solutions for static graphs. Online algorithms are generalised versions of current Internet routing protocols, obtained by removing the implicit routing languages and replacing them with routing interfaces. This latter type of algorithm allows the generation of fully-fledged Internet routing protocols. Traditionally, routing protocols are monolithically specified and implemented. Specifications may reach hundreds of pages of informal prose, and implementations usually contain tens of thousands of lines of source code, often with serious errors. The metarouting approach has several significant advantages. Firstly, by separately specifying routing languages and reusing existing routing algorithms, it allows the rapid development of new routing protocols. Secondly, the system is able to determine whether a particular combination of routing language and algorithm is well-behaved. This involves the automatic inference of mathematical properties of routing languages. Finally, routing language specifications can be compiled into the efficient code with minimal user intervention. In some cases the compiler is able to exploit inferred mathematical properties. This dissertation concludes with an algebraic model of protocol interaction that is termed simple route redistribution. This model demonstrates how to avoid the safety problems that are associated with the traditional interaction mechanisms of route redistribution and administration distance. Fundamental to simple route redistribution is a clear distinction between routing and forwarding. The model also captures the separation of locators and identifiers found in recent proposals for a new Internet architecture.EThOS - Electronic Theses Online ServiceGBUnited Kingdo