### 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 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

- S. Prasad. Formal foundations of routing. Slides from the EWSCS 2018 course.

#### Background reading

- General background reading:
- E. W. Dijkstra. A note on two problems in connexion with graphs.
*Numer. Math.*, v. 1, n. 1, pp. 269-271, 1959. [doi link] - M. Gondran, M. Minoux.
*Graphs, Dioids and Semirings*. Springer, 2008. - R. Bird, O. de Moor.
*Algebra of Programming*. Prentice Hall, 1997. - J. H. Conway.
*Regular Algebra and Finite Machines*. Chapman and Hall, 1971. - D. Kozen, F. Smith. Kleene algebra with tests: Completeness and
decidability. In
*Proc. of CSL '96*, v. 1258 of*Lect. Notes in Comput. Sci.*, pp. 244-259. Springer, 1997. [doi link] - D. Kozen. Kleene algebra with tests.
*Trans. on Program. Lang. and Syst.*, v. 19, n. 3, pp. 427–443, 1997. [doi link] - A. Silva.
*Kleene Coalgebra*. PhD thesis, Radboud University Nijmegen, 2010. - Part 1:
- P. Höfner, B. Möller. Dijkstra, Floyd and Warshall meet
Kleene.
*Formal Aspects of Comput.*, v. 24, n. 4-6 , pp. 459–476, 2012. [doi link] - Part 2:
- C. J. Anderson, N. Foster, A. Guha, J.-B. Jeannin, D. Kozen,
C. Schlesinger, D. Walker. NetKAT: Semantic foundations for
networks. In
*Proc. of POPL 2014*, pp. 113-126. ACM, 2014. [doi link] - D. Kozen. NetKAT: A formal system for the verification of
networks. In
*Proc. of APLAS 2014*, v. 8858 of*Lect. Notes in Comput. Sci.*, pp. 1-18. Springer, 2014. [doi link] - N. Foster, D. Kozen, M. Milano, A. Silva, L. Thompson. A
coalgebraic decision procedure for NetKAT. In
*Proc. of POPL 2015*, pp. 343-355. ACM, 2015. [doi link] - N. Foster, D. Kozen, K. Mamouras, M. Reitblatt, A.
Silva. Probabilistic NetKAT. In
*Proc. of ESOP 2016*, v. 9632 of*Lect. Notes in Comput. Sci.*, pp. 282-309. Springer, 2016. [doi link] - Part 3:
- T. G. Griffin, J. L. Sobrinho. Metarouting.
*Proc. of SIGCOMM '05*, pp. 1-12, ACM 2005. [doi link] - Part 4:
- M. Karsten , S. Keshav , S. Prasad, M. Beg. An axiomatic
basis for communication. In
*Proc. of SIGCOMM '07*, pp. 217-228. ACM, 2007. [doi link] - L. D. Zuck, S. Prasad. A switch, in time. In
*Proc. of TGC 2015*, v. 9533 of*Lect. Notes in Comput. Sci.*, pp. 131-146. Springer, 2015. [doi link] - L. D. Zuck, S. Prasad. Limited mobility, eventual stability. In
*Proc. of HVC 2015*, v. 9434 of Lect. Notes in Comput. Sci., pp. 139-154. Springer, 2015. [doi link]

Last changed **
March 7, 2018 18:14 Europe/Helsinki (GMT +02:00)**
by
local organizers, ewscs18(at)cs.ioc.ee

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