Rigorous Internet Protocol Engineering (Fall 2011)
Instructors: Alex Gurney (Penn), Limin Jia (CMU), Boon Thau Loo (Penn)
Time: Monday and Wednesday 3:00 – 4:30pm
Penn Location: Moore 102 (DSL conference room). The lab is protected by a key code. If you are locked out, please ring the doorbell.
CMU Location: CIC 1301.
Newsgroup: http://groups.google.com/group/cis-800-003-fall11
Course Description
This graduate seminar course is to introduce students to current research on the rigorous design, implementation, and analysis of network protocols. The topics covered in this course include formal mathematical models of Internet protocols, domain specific languages (declarative, functional, or logic-based) for specifying protocols with high-assurance, and verification techniques to prove correctness and security properties of protocols. Case studies will be drawn from traditional IP protocols, BGP policy configurations, secure BGP, transport protocols, application-layer overlay networks, and protocols developed using emerging platforms such as OpenFlow. Through these case studies, students will acquire knowledge into formal modeling of protocols, and apply well-known verification techniques such as model checking and automated theorem proving into the analysis of network protocols.
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.
- Paper summaries: 30%
- Class participation: 20%
- Class presentation: 10%
- Project: 40%
Schedule
The instructors are Alex (A), Boon (B) and Limin (L). See the reading list for citations, links to papers, and additional background material.
| 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 | ||
| Oct 10 | No class (Fall Term Break) | |||||
| Oct 12 | ABL | Partial specification of routing configurations (practice talk for WRiPE 2011) | ||||
| Oct 17 | 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 | ||||