### Sanjiva Prasad

Dept. of Computer Science and Engineering

Indian Institute of Technology Delhi

India

## Formal foundations of routing in networks

#### Abstract

Algebraic structures such as **semirings** have long provided the
mathematical basis for framing path-related questions such as
connectivity and least-cost paths in communication networks. A long
series of work starting from Berge and Carre’ up to recent work by
Hoefner & Moeller show that algorithmic solutions to these problems,
such as those given by Dijkstra and by Roy/Floyd/Warshall, can be
**algebraically** derived within a framework of *cost semirings*.

**Packet-switching** networks additionally require being able to define
filters and describe complex sets of paths. The theory of *Kleene
Algebras with Tests*, specialised for networks yields a
domain-specific algebraic language (NetKAT of Foster, Kozen, Silva et
al.) in which reachability properties of packet switching networks can
be expressed and proved (using co-algebraic techniques).

Real networks however require complex protocols for Routing, i.e,
establishing "good" paths satisfying certain desired properties along
which packets may be forwarded. The **Routing Algebra** framework of
Sobrinho, Griffin, et al provides a formalism in which a large family of
routing policies can be expressed and about which correctness conditions
can be proven with respect to given routing mechanisms.

The generality of the structure and behaviour of modern-day networks
requires more abstract treatments, such as the *Axiomatic Basis of
Communication* suggested by Karsten et al., in which minimal
assumptions about abstract switches are used to formulate fundamental
notions in networks such as naming, addresses, peers, tunnels, paths,
namespaces etc. We conclude with a reformulation of these axioms using
**Linear-time Temporal Logic**, using which questions about message
deliverability can be expressed even in the presence of mobility
(Mobile IP), message encryption (TOR) and other dynamic features of
networks.

#### Course materials

Last changed **
February 10, 2018 2:46 Europe/Helsinki (GMT +02:00)**
by
local organizers, ewscs18(at)cs.ioc.ee

EWSCS'18 page:
http://cs.ioc.ee/ewscs/2018/