Organization. This course is open to Ph.D. students. Masters students and undergraduates may enroll with permission of the instructors. The class will be organized as a Penn/CMU joint seminar where students from both institutions will jointly discuss and present papers with the aid of video conferencing tools.
Course pre-requisites. Undergraduate knowledge in networking and security. The instructors will devote a few lectures to reviewing relevant material in networking, security, and formal tools.
|Sep 7||ABL||General introduction||Boon||PPTX|
|Formal analysis of BGP safety|
|Sep 12||A||Interdomain routing and the Border Gateway Protocol.
Please read: BGP routing policies in ISP networks
|Sep 14||A||The stable paths problem and interdomain routing. Griffin, Shepherd, Wilfong||Sangeetha||PPTX|
|Sep 19||A||Network routing with path vector protocols. Sobrinho.||Yang|
|Sep 21||A||Metarouting. Griffin, Sobrinho.||Anduo|
|Sep 26||A||Stable and flexible iBGP. Flavel, Roughan.||Lu||PPTX|
|Security and cryptographic protocols|
|Sep 28||L||Introduction to cryptography and security
Optional reading [Overview of Cryptography] and [Intro to Logic (sections 1-3)]
|Oct 3||L||S-BGP. A survey of BGP security issues and solutions. Butler, Farley, McDaniel, Rexford.||Kyle||PPTX, PDF|
|Oct 5||L||The inductive approach to verifying cryptographic protocols. Paulson. Sections 1-5||Vincent||PPTX|
|No class (Fall Term Break)|
|Oct 12||ABL||Partial specification of routing configurations (practice talk for WRiPE 2011)|
|No class (Instructors away)|
|Oct 19||L||Automated analysis of cryptographic protocols using Murφ. Mitchell, Mitchell, Stern.||Mingchen||PPTX|
|Oct 24||A||Let the market drive deployment: a strategy for transitioning to BGP security. Gill, Schapira, Goldberg.||Kevin|
|Oct 26||L||Guest lecture: SCION: scalability control and isolation on next generation networks. Zhang et al.||Xin Zhang (CMU)||PPTX|
|Project proposals due|
|Oct 31||L||From Secrecy to Authenticity in Security Protocols. Blanchet.||Chen||PPTX|
|Practical systems and case studies|
|Nov 2||ABL||Guest lecture: ConfigAssure: A Science of Configuration.
Please read: Formal Methods for Safe Configuration of Cyberinfrastructure.
Write your summaries on: Network Configuration Validation.
|Sanjai Narain (Telcordia)|
|Nov 7||B||OpenFlow, NOX (Extra reading: Practical Declarative Network Management. Hinrichs et.al.)||Lin|
|Nov 9||B||Frenetic: a network programming language. Foster et al.||Sumanth|
|Nov 14||B||Model-checking large network protocol implementations. Musuvathi, Engler.||Loris|
|Nov 16||B||BOOM Analytics: Exploring Data-Centric, Declarative Programming for the Cloud. Alvaro et al.||Zhuoyao|
|Nov 21||B||Declarative Networking. Loo et al.||Boon||PPTX|
|Nov 23||B||FATE and DESTINI: A Framework for Cloud Recovery Testing. Gunawi et.al.||Harjot|
|Nov 28||B||Mace: Language Support for Building Distributed Systems.
Optional: Life, Death, and the Critical Transition: Finding Liveness Violations in Systems Code. Killian et al.
|Nov 30||ABL||Guest lecture||Pamela Zave (AT&T Research)|
|Dec 5||ABL||Project presentations|
|Dec 7||ABL||Project presentations|