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.
Grading.
Lecture | Instructor | Paper | Presenter | Slides | ||
---|---|---|---|---|---|---|
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 |
Alex | PPTX, PDF | ||
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
analysis Optional reading [Overview of Cryptography] and [Intro to Logic (sections 1-3)] |
Limin | PPTX | ||
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. |
Santosh | |||
Nov 30 | ABL | Guest lecture | Pamela Zave (AT&T Research) | |||
Dec 5 | ABL | Project presentations | ||||
Dec 7 | ABL | Project presentations |