23rd Estonian Winter School in Computer Science (EWSCS)
XXIII Eesti Arvutiteaduse Talvekool

Palmse, Estonia, March 4 - 9, 2018

Sanjiva Prasad

Dept. of Computer Science and Engineering
Indian Institute of Technology Delhi

Formal foundations of routing in networks


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 Carré up to recent work by Höfner & Möller 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 coalgebraic 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

Background reading

Valid CSS! Valid XHTML 1.0 Strict Last changed April 10, 2020 22:35 Europe/Helsinki (GMT +03:00) by local organizers, ewscs18(at)cs.ioc.ee
EWSCS'18 page: //cs.ioc.ee/ewscs/2018/