CIS 800/00x - Rigorous Internet Protocol Engineering (Fall 2011) - Reading list

Formal analysis of BGP safety

• Griffin, Timothy G.; Wilfong, Gordon. 1999. An analysis of BGP convergence properties. Proc. ACM SIGCOMM.
• Griffin, Timothy G.; Shepherd, F. Bruce; Wilfong, Gordon. 1999. Policy disputes in path vector protocols Proc. IEEE ICNP.
• Gao, Lixin; Rexford, Jennifer. 2001. Stable Internet routing without global coordination. IEEE/ACM Transactions on Networking 9(6):681-692. Previously in Proc. ACM SIGMETRICS, 2000, p307-317. [PDF]
• Sobrinho, João Luis. 2001. On the convergence of path vector protocols. Proc. IEEE Workshop on High Performance Switching and Routing, p292-296.
• Griffin, Timothy G.; Shepherd, F. Bruce; Wilfong, Gordon. 2002. The stable paths problem and interdomain routing. IEEE/ACM Transactions on Networking 10(2):232-243. [PDF]
• Gouda, Mohamed G.; Schneider, Marco. 2003. Maximizable routing metrics. IEEE/ACM Transactions on Networking 11(4):663-675.
• Sobrinho, João Luis. 2003. Network routing with path vector protocols: theory and applications. Proc. ACM SIGCOMM, p49-60. [PDF]
• Caesar, Matthew; Rexford, Jennifer. 2005. BGP routing policies in ISP networks. IEEE Network, special issue on interdomain routing, Nov/Dec 2005. [PDF]
• Feamster, Nick; Balakrishnan, Hari. 2005. Correctness properties for Internet routing. Proc. 43rd Allerton Conference on Communication, Control and Computing.
• Griffin, Timothy G.; Sobrinho, João Luis. 2005. Metarouting. Proc. ACM SIGCOMM, p1-12. [PDF]
• Sobrinho, João Luis. 2005. An algebraic theory of dynamic network routing. IEEE/ACM Transactions on Networking 13(5):1160-1173.
• Gurney, Alexander J. T.; Griffin, Timothy G. 2007. Lexicographic products in metarouting. Proc. IEEE ICNP, p113-122.
• Flavel, Ashley; Roughan, Matt; Bean, Nigel; Shaikh, Aman. 2008. Where's Waldo? Metarouting and practical searches for stability in iBGP. Proc. IEEE ICNP. [PDF]
• Flavel, Ashley; Roughan, Matthew. 2009. Stable and flexible iBGP. Proc. ACM SIGCOMM, p183-194. [PDF]

Security and cryptographic protocols

• Mitchell, John C.; Mitchell, Mark; Stern, Ulrich. 1997. Automated analysis of cryptographic protocols using Murφ. Proc. IEEE Symp. on Security and Privacy, p141-151. [PDF]
• Paulson, Lawrence C. 1998. The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6(1-2). [PDF]
• Butler, Kevin; Farley, Toni R.; McDaniel, Patrick; Rexford, Jennifer. 2010. A survey of BGP security issues and solutions. Proc. IEEE 98(1):100-122. [PDF]
• Blanchet, Bruno. 2011. From Secrecy to Authenticity in Security Protocols. In: SAS '02 [PS] (PDF can be obtained from [here])
• Anupam Datta, John C. Mitchell, Arnab Roy, and Stephan Hyeonjun Stiller. 2011. Protocol composition logic. In: Formal models and techniques for analyzing security protocols (Véronique Cortier and Steve Kremer, eds.), IOS Press, p182-221. [PDF]
• Xin Zhang, Hsu-Chun Hsiao, Geoffrey Hasker, Haowen Chan, Adrian Perrig and David Andersen. 2011. SCION: scalability control and isolation on next generation networks. IEEE Symposium on Security and Privacy 2011. [PDF]
• Sharon Goldberg, Michael Schapira, Peter Hummon, and Jennifer Rexford. 2010. How secure are secure interdomain routing protocols?. SIGCOMM 2010. [PDF]
• Phillipa Gill, Michael Schapira, and Sharon Goldberg. 2011. Let the Market Drive Deployment: A Strategy for Transitioning to BGP Security. SIGCOMM 2011. [PDF]

Domain-specific languages for network protocols

• Loo, Boon Thau; Condie, Tyson; Garofalakis, Minos; Gay, David E.; Hellerstein, Joseph M.; Maniatis, Petros; Ramakrishnan, Raghu; Roscoe, Timothy; Stoica, Ion. 2009. Declarative networking. Communications of the ACM, November 2009. [PDF]
• Karsten, Martin; Keshav, S.; Prasad, Sanjiva. 2006. An axiomatic basis for communications. Proc. ACM SIGCOMM 2007. [PDF]
• Foster, Nate; Harrison, Rob; Freedman, Michael J.; Monsanto, Christopher; Rexford, Jennifer; Story, Alec; Walker, David. 2011. Frenetic: a network programming language. Proc. ACM SIGPLAN ICFP. [PDF]
• Killian, Charles Edward; Anderson, James W.; Braud, Ryan; Jhala, Ranjit; Vahdat, Amin M. 2007. Mace: language support for building distributed systems. Proc. ACM SIGPLAN PLDI. [PDF]
• Rodriguez, Adolfo; Killian, Charles; Bhat, Sooraj; Kostic, Dejan; Vahdat, Amin. 2004. MACEDON: Methodology for Automatically Creating, Evaluating and Designing Overlay Networks. Proc. NSDI, p267-280. [PDF]
• Andreas Voellmy and Paul Hudak. Nettle: Taking the Sting Out of Programming Network Routers. Proc. PADL 2011 [PDF]

Verifying distributed systems

• Madanlal Musuvathi, David Y.W. Park, Andy Chou, Dawson R. Engler, David L. Dill. 2004. CMC: A pragmatic approach to model checking real code. Proc. OSDI [PDF]
• Musuvathi, Madanlal; Engler, Dawson R. 2004. Model checking large network protocol implementations. Proc. NSDI. [PDF]
• Junfeng Yang, Tisheng Chen, Ming Wu, Zhilei Xu, Xuezheng Liu, Haoxiang Lin, Mao Yang, Fan Long, Lintao Zhang, and Lidong Zhou 2004. MODIST: Transparent Model Checking of Unmodified Distributed Systems. Proc. NSDI. [PDF]
• Rachid Guerraoui and Maysam Yabandeh. 2011. Model Checking a Networked System Without the Network. Proc. NSDI. [PDF]
• Karthikeyan Bhargavan, Davor Obradovic, and Carl A. Gunter 2002. Formal Verification of Standards for Distance Vector Routing . Journal of the ACM. [PDF]
• Paul Barham, Austin Donnelly, Rebecca Isaacs, and Richard Mortier 2004. Using Magpie for request extraction and workload modelling OSDI. [PDF]
• Charles Killian, James W. Anderson, Ranjit Jhala, and Amin Vahdat. 2007. Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code OSDI. [PDF]