CIS 800/00x - Rigorous Internet Protocol Engineering (Fall 2011) - Reading list
[Main course page]
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]