CIS 800/003 - 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.

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.



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
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 PDF
Sep 21 A Metarouting. Griffin, Sobrinho. Anduo PDF
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) PDF
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 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 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