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

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.
• Lecture 1 [pdf]
• Lecture 2 [pdf]
• Lecture 3 [pdf]
• Lecture 4 [pdf]


• Videos from the lectures (large, unedited files) [mp4, password-protected]

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