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

Schedule

Reading List

SAT Solvers

• Boolean satisfiability from theoretical hardness to practical success. S. Malik. L. Zhang. Communications of the ACM, August 2009.

Alloy and its application to configuration management

• Network Configuration Management Via Model Finding. S. Narain. Proceedings of USENIX Large Installation System Administration (LISA) Conference, San Diego, CA, 2005. Full report.

Application of SAT to configuration management

• Declarative Infrastructure Configuration Synthesis and Debugging. S. Narain, V. Kaul, G. Levin, S. Malik. Journal of Network Systems and Management, Special Issue on Security Configuration, eds. Ehab Al-Shaer, Charles Kalmanek, Felix Wu. 2008.

• OPIUM: Optimal Package Install/Uninstall Manager. C. Tucker, D. Shuffleton, R. Jhala, S. Lerner.

Logic programming and Prolog

• Predicate logic as a programming language. R. Kowalski.

• The semantics of predicate logic as a programming language. M. H. van Emden

• Clause and effect. Prolog programming for the working programmer. Chris Mellish. Springer, 1997.

Network Configuration Validation

• Network Configuration Validation. Sanjai Narain, Gary Levin, Rajesh Talpade. Chapter in Guide to Reliable Internet Services and Applications, edited by Chuck Kalmanek (AT&T), Richard Yang (Yale) and Sudip Misra (IIT). Springer Verlag, 2009

• Using Service Grammar to diagnose configuration errors in BGP-4. Proceedings of USENIX Large Installation System Administration (LISA) Conference, San Diego, CA 2003

Datalog + MinCostSAT for network vulnerability analysis and mitigation

• What you always wanted to know about datalog (and never dared to ask), by Stefano Ceri, Georg Gottlob, and Letizia Tanca.

• XSB: A system for efficiently computing well-founded semantics, by Prasad Rao, et al.

• Online justification for tabled logic programs , by Giridhar Pemmasani, et al.

• MulVAL: A logic-based network security analyzer, by Xinming Ou, Sudhakar Govindavajhala, and Andrew Appel.

• (*)A scalable approach to attack graph generation, by Xinming Ou, Wayne F. Boyer, and Miles A. McQueen.

• (*)SAT-solving approaches to context-aware enterprise network security management, by John Homer and Xinming Ou.

Binary Decision Diagrams and their application to security policy verification

• Ehab Al-Shaer begin_of_the_skype_highlighting     end_of_the_skype_highlighting, Will Marrero, Adel El-Atawy and Khalid Elbadawi, Network Security Configuration in A Box: End-to-End Security Configuration Verification, IEEE International Conference in Network Protocols (ICNP’ 09), October 2009

• Hazem Hamed, Ehab Al-Shaer and Will Marrero, Modeling and Verification of IPSec and VPN Security Policies, IEEE ICNP'2005, November 2005, (Acceptance rate 17%)

• Ehab Al-Shaer, Hazem Hamed, Raouf Boutaba and Masum Hasan, Conflict Classification and Analysis of Distributed Firewall Policies, IEEE Journal on Selected Areas in Communications, Issue: 10, Volume: 23, Pages: 2069 - 2084, October 2005

• On Static Reachability Analysis of IP Networks by G. Xie, J. Zhan, D. Maltz, H. Zhang, A. Greenberg, G. Hjalmtysson, J. Rexford (2005) On Static Reachability Analysis of IP Networks. IEEE INFOCOM

Alloy and Promela for protocol verification

• Logic Model Checking, Gerard J. Holzmann, introductory lecture in a course at Caltech, 2010.

• Introduction to the book Software Abstractions, Daniel Jackson, 2006.

• Lightweight verification of network protocols: The case of Chord, Pamela Zave, 2010.

• For a complete description, including of projects, see http://www2.research.att.com/~pamela/fmin.html

Isabelle/HOL for protocol verification 

• Isabelle Home Page: http://isabelle.in.tum.de/index.html

• Isabelle/HOL tutorial: http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf. Read chapter 1-3,5-7. Chapter 10 demonstrates an application of Isabelle/HOL to proving the correctness of a security protocol.

• Isar (the proof language for Isabelle/HOL) in this short tutorial: http://isabelle.in.tum.de/dist/Isabelle/doc/isar-overview.pdf

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.