CS 598D

Spring 2010

Formal Methods in Networking
Lead Instructor: Dr. Sanjai Narain
Telcordia Technologies
Mondays and Fridays
9:30-10:50am, Room 302

Modern formal methods are mature enough for solving industrial-strength problems. This semester-long seminar course will explore these methods in the context of networking. The methods and related systems will include Binary Decision Diagrams and SAT and SMT solvers for Boolean logic, Prolog and Datalog for definite-clause subset of first-order logic, Alloy for first-order logic, Promela for concurrent programs and Isabelle for higher-order logic. Instructors will provide an overview of these methods and of their application to networking problems such as configuration synthesis and debugging, vulnerability analysis and mitigation, security policy and protocol verification, and routing protocol design. Instructors will also outline open problems. Students will be expected to select one or more of these methods, understand these in-depth by reading papers and using implementations of these methods to solve problems of interest to them, and present their findings to the class. A list of papers covering the theory, implementation and application of these methods will be provided.

The course will be coordinated by Dr. Sanjai Narain from Telcordia Technologies. He will also teach Prolog, and applications of Alloy and SAT/SMT solvers to configuration synthesis and debugging and security policy verification. Lectures on other topics will be given by:

  • Professor Ehab Al-Shaer, University of North Carolina, Charlotte: Binary Decision Diagrams and their application to security policy verification

  • Professor Boon Thau Loo, University of Pennsylvania: Datalog and its application to routing protocol design

  • Professor Sharad Malik, Princeton: SAT and SMT solvers

  • Professor Simon Ou, Kansas State University: Datalog and its combination with MinCost SAT solvers for vulnerability analysis and mitigation

  • Mr. Andreas Voellmy, Yale University: Isabelle and its application to BGP policy verification

  • Dr. Pamela Zave, AT&T Research: Alloy and Promela and their application to protocol verification


M & F In Week of





Introduction and logic programming theory



Constraint Solving For Networking, Part I and Part II



Application of SAT/SMT solvers to theory of configuration and application of Alloy to same



Datalog and  its application to routing protocol design


Malik & Wang

SAT and SMT solvers



Datalog+MinCost SAT solvers for network vulnerability analysis and mitigation. Part I, Part II.

3/15/10 NO CLASS



Promela and application to protocol verification. Part I, Part II



Alloy and application to protocol verification, Part I, Part II



Binary decision diagrams and their application to security policy verification



Isabelle and BGP verification. Review of papers




Reconfiguration Planning

Review of BGP Stable Path Problem



Student paper presentations. Student paper review reports due 4/30



Student paper presentations



Student project presentation “The Next 10,000 BGP Gadgets. Lightweight Modeling For Stable Paths Problem” by Matve Arye, Rob Harrison, Richard Wang.

A complementary encoding of Stable Path Problem in Alloy

Reading List

SAT Solvers

Alloy and its application to configuration management

Application of SAT to configuration management

Logic programming and Prolog

Network Configuration Validation

Datalog + MinCostSAT for network vulnerability analysis and mitigation

Binary Decision Diagrams and their application to security policy verification

Alloy and Promela for protocol verification

Isabelle/HOL for protocol verification 

Datalog and its application to routing protocol design

Must read papers:

  • A Survey of Research on Deductive Database Systems, Raghu Ramakrishnan and Jeffrey D. Ullman, Journal of Logic Programming, 1993

  • Declarative Routing: Extensible Routing with Declarative Queries.
    Boon Thau Loo, Joseph M. Hellerstein, Ion Stoica, and Raghu Ramakrishnan.
    ACM SIGCOMM Conference on Data Communication, Philadelphia, PA, Aug 2005.

Optional reading:

  • Declarative Networking.
    Boon Thau Loo, Tyson Condie, Minos Garofalakis, David E. Gay, Joseph M. Hellerstein, Petros Maniatis, Raghu Ramakrishnan, Timothy Roscoe, and Ion Stoica. 

  • Implementing Declarative Overlays.
    Boon Thau Loo, Tyson Condie, Joseph M. Hellerstein, Petros Maniatis, Timothy Roscoe, and Ion Stoica.
    20th ACM Symposium on Operating Systems Principles (SOSP), Brighton, UK, October 2005.

  • Declarative Networking: Language, Execution and Optimization.
    Boon Thau Loo, Tyson Condie, Minos Garofalakis, David E. Gay, Joseph M. Hellerstein, Petros Maniatis, Raghu Ramakrishnan, Timothy Roscoe, and Ion Stoica. 

  • Formally Verifiable Networking.
    Anduo Wang, Limin Jia, Changbin Liu, Boon Thau Loo, Oleg Sokolsky, and Prithwish Basu.
    8th Workshop on Hot Topics in Networks (ACM SIGCOMM HotNets-VIII), New York, Oct 2009.

  • Declarative Network Verification.
    Anduo Wang, Prithwish Basu, Boon Thau Loo, and Oleg Sokolsky.
    11th International Symposium on Practical Aspects of Declarative Languages (PADL), in conjunction with POPL, Savannah, Georgia, Jan 2009.

  • Unified Declarative Platform for Secure Networked Information Systems.
    Wenchao Zhou, Yun Mao, Boon Thau Loo, and Martín Abadi.
    25th International Conference on Data Engineering (ICDE), Shanghai, China, Apr 2009.