Finding the Right Abstraction for a Modular Router: An Axiomatic Basis

Martin Karsten and S. Keshav
University of Waterloo
Waterloo, Ontario, Canada

Traditional routers make several implicit assumptions about Internet forwarding. Typically, they assume that nodes
are addressed by one or more static IP addresses and that packet forwarding decisions are supposed to be made purely on the
basis of IP ‘routing’ tables and inspecting only IP headers. However, when considering that routing (forwarding) functionality
is implemented not only at traditional routers, but also at  firewalls, VLAN switches, MPLS routers, NAT boxes,
firewalls, mesh routing nodes, and other middleboxes, the limitations of these assumptions become clear. In reality:

- DHCP, anycast, multicast, NAT, mobile IP and others break the static association between a node and its IP
address.
- Packet forwarding requires inspection of many layers, including IP or VLAN tunnels, overlays, and shims, such as MPLS.

In face of these significant extensions to the classical model, even understanding the topology of the Internet in terms of its
connectivity has become a daunting task. It has become difficult to define elementary concepts such as a neighbour and
peer relationships, let alone the more complex processes of forwarding and routing. Further, there is not even a common
and well-defined language for fundamental networking concepts, with terms such as 'name', 'address', or 'port' being
the subject of seemingly endless debate.

Yet, surprisingly, the system still works! Most users, most of the time, are able to use the Internet. What lies behind the
unreasonable effectiveness of the Internet? We postulate that all extensions to the traditional model, no matter how ad hoc, 
obey a set of underlying principles, which preserve connectivity. However, with a few notable exceptions, these principles have 
rarely been systematically studied.

In recent work, we have axiomatically specified basic internetworking concepts that allow us to construct (a) a theoretically
sound framework to express architectural invariants – such as the deliverability of messages - even in the presence
of network dynamism, middleboxes, and a variety of compositions of different protocols, and (b) an expressive
meta-language in which to rapidly implement any desired packet forwarding scheme. The concepts and the metalanguage derived 
from them serve not only to clarify the essential architecture of the Internet, but also provide a bridge between formal proofs on 
node reachability and a practical implementation of various forwarding schemes. We believe that the conceptual clarity that arises
from our work allows us to (a) quickly sketch the essential aspects of any type of communication network, no matter how exotic, 
and (b) apply concepts from one network technology to another.

Our work brings together three research threads that span the networking and formal verification communities. The
first thread is that of using formal notation to compactly and precisely model network communication, and, in particular,
communication in the Internet. This allows us to derive elementary axiomatically-sound forwarding and control operations.
Second, we exploit standard techniques in formal verification to prove the correctness of network protocols
composed from these operations. Finally, our work builds on extensive past work in rapid protocol prototyping. We
use meta-compilation to translate from a protocol expressed in terms of elementary operations to a C++ implementation
that can be embedded in the Click engine and incorporated into the Internet.

It is illuminating to compare our definition of names and addresses to that in common use. Commonly, the name of
an object is a 'human-readable' string, and the address is a 'machine-readable' location. Names are meant to refer to
entities, and addresses are meant to get to them. This is, of course, incorrect when faced with name-based forwarding
and address masquerading. By tightly coupling the act of communication with the concept of a name and precisely
specifying the scope of a name, we not only achieve conceptual clarity but also can resolve a host of conceptual pitfalls.
For instance, an IP address is an address in the public IP scope, but devolves to a name within a NAT gateway that
bridges name scopes. Similarly, a "toll-free" number is an address until it reaches a translation table, that then translates
it to another address in the same scope. These distinctions are possible because of the simplicity and clarity of our
axiomatic framework.

Our axiomatic approach has allowed us to discover heretofore hidden isomorphisms. For instance, it is easy to see that
NAT is essentially the same as RSVP-TE or ATM, in that it sets up a forwarding table that translates between name
spaces. These name spaces are the public and private IP name spaces, which are, in principle, similar to the VCI
spaces in ATM. Even more interestingly, the same bridging of name spaces is accomplished in Mobile IP, IP multicast
and I3. Therefore, the same protocol engine, with minor modifications, can be used to implement these protocols!
From a more pragmatic perspective, implementation optimizations for any of these protocols apply equally to all.
Another interesting consequence of our work is the potential to automatically build validated protocol implementations,
perhaps even in hardware. We can do so by expressing a protocol in terms of elementary operations, and then
using a Hoare-logic theorem prover to prove its correctness. The same protocol can then be meta-compiled, perhaps to
an FPGA. This would eliminate error-prone human coding of complex protocols.

In current work, we are using our metalanguage to compactly specify an Ethernet bridge, an IP router, a NAT middlebox,
and an I3 router. Moreover, we compile this metalanguage to build working systems (on top of Click) that
interoperate with existing implementations. This gives us some confidence that our axiomatic foundation is a good first 
step in finding the right abstraction for building a modular router.