The Formally Verifiable Routing (FVR) project addresses a long-standing challenge in networking research — bridging the gap between formal theories (for reasoning about protocol correctness) and actual implementations. One of our significant contributions is the FSR (Formally Safe Routing) toolkit [SIGCOMM’11 demo], that attempts to bridge this gap in the context of interdomain routing, by unifying research in routing algebras with recent advances in declarative networking to produce provably correct distributed implementations. Specifically, FSR automates the process of analyzing routing configurations expressed in algebra for safety (i.e. convergence) using SMT solvers, and automatically compiles routing algebra into declarative routing implementations. In addition to the FSR toolkit, the FVR project has also explored the use of theorem proving and rewriting logic techniques for verifying routing protcols. See our contributions and publications for more details.

Contributions

Formally Safe Routing (FSR) Toolkit

FSR is a comprehensive toolkit for analyzing and implementing routing policies, ranging from high-level guidelines to specic router congurations. The FSR toolkit performs all of these functions from the same algebraic representation of routing policy. We show that routing algebra has a very natural translation to both integer constraints (to perform safety analysis using SMT solvers) and declarative programs (to generate distributed implementations). Our SIGCOMM’11 demonstration with realistic topologies and policies shows how FSR can detect problems in an AS’s iBGP conguration, prove suf- cient conditions for BGP safety, and empirically evaluate convergence time.

Analyzing BGP Instances using Maude

Analyzing Border Gateway Protocol (BGP) instances is a crucial step in the design and implementation of safe BGP systems. Today, the analysis is a manual and tedious process. Researchers study the instances by manually constructing execution sequences, hoping to either identify an oscillation or show that the instance is safe by exhaustively examining all possible sequences. In [FMOODS’11], We propose to automate the analysis by using Maude, a tool based on rewriting logic. We have developed a library specifying a generalized path vector protocol, and methods to instantiate the library with customized routing policies. Protocols can be analyzed automatically by Maude, once users provide specifications of the network topology and routing policies. Using our Maude library, protocols or policies can be easily specified and checked for problems. To validate our approach, we performed safety analysis of well-known BGP instances and actual routing configurations.

Declarative Network Verification (DNV)

DNV [PADL’09] is a declarative network verifier that utilizes theorem proving, a well established verification technique where logic-based axioms that automatically capture network semantics are generated, and a user-driven proof process is used to establish network correctness properties. DNV takes as input declarative networking specifications written in the Network Datalog (NDlog) query language, and maps that automatically into logical axioms that can be directly used in existing theorem provers to validate protocol correctness. DNV is a significant improvement compared to existing use case of theorem proving which typically require several man-months to construct the system speci.cations. Moreover, NDlog, a high-level specification, whose semantics are precisely compiled into DNV without loss, can be directly executed as implementations, hence bridging specifications, veri.cation, and implementation. To validate the use of DNV, we present case studies using DNV in conjunction with the PVS theorem prover to verify routing protocols, including eventual properties of protocols in dynamic settings.

Operational Semantics of Declarative Networking

Declarative networking programs allow both facts and programs to be distributed among different nodes in a network. However, the distributed nature of the underlying systems poses serious challenges to developing efficient and correct algorithms for evaluating these programs. In [PPDP’11], we propose efficient asynchronous algorithm to compute incrementally the changes to the states in response to insertions and deletions of base facts. Our algorithm is formally proven to be correct in the presence of message reordering in the system. To our knowledge, this is the first formal proof of correctness for such an algorithm.

Pair-wise Minimal Cost (MinCost) Protocol

Students

Postdocs

Faculty

Past contributors

Publications

  • Reduction-based Analysis of BGP Systems with BGPVerif.
    Anduo Wang, Alexander J.T. Gurney, Xianglong Han, Jinyan Cao, Carolyn Talcott, Boon Thau Loo, and Andre Scedrov.
    ACM SIGCOMM Conference on Data Communication (demonstration), Helsinki, Finland, Aug, 2012.
  • Route Shepherd: Stability Hints for the Control Plane.
    Alexander J.T. Gurney, Xianglong Han, Yang Li, and Boon Thau Loo.
    ACM SIGCOMM Conference on Data Communication (demonstration), Helsinki, Finland, Aug, 2012.
  • A Calculus of Policy-Based Routing Systems.
    Anduo Wang, Carolyn Talcott, Alexander J.T. Gurney, Boon Thau Loo, and Andre Scedrov.
    31st Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC), 2012. (Brief announcement)
  • Maintaining Distributed Logic Programs Incrementally.
    Vivek Nigam, Limin Jia, Boon Thau Loo and Andre Scedrov.
    Computer Languages, Systems & Structures (COMLAN), Elsevier Publishing, 2012.
  • FSR: Formal Analysis and Implementation Toolkit for Safe Inter-domain Routing.
    Anduo Wang, Limin Jia, Wenchao Zhou, Yiqing Ren, Boon Thau Loo, Jennifer Rexford, Vivek Nigam, Andre Scedrov, Carolyn L. Talcott.
    IEEE/ACM Transactions on Networking (ToN), 2012.
  • Reduction-based Formal Analysis of BGP Instances. [Paper] [Technical report]
    Anduo Wang, Carolyn Talcott, Alexander J.T. Gurney, Boon Thau Loo and Andre Scedrov.
    18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Mar 2012. (24.5% acceptance)
  • Partial Specifications of Routing Configurations.
    Alexander J. T. Gurney, Limin Jia, Anduo Wang, and Boon Thau Loo.
    1st International Workshop on Rigorous Protocol Engineering (WRiPE), co-located with ICNP 2011, Vancouver, Canada, Oct 2011.
  • FSR: Formal Analysis and Implementation Toolkit for Safe Inter-domain Routing. [Paper] [Extended Technical Report]
    Yiqing Ren, Wenchao Zhou, Anduo Wang, Limin Jia, Alexander J.T. Gurney, Boon Thau Loo, and Jennifer Rexford.
    ACM SIGCOMM Conference on Data Communication (demonstration), Toronto, Canada, Aug, 2011.
    Runner-up for the ACM Student Research Competition at SIGCOMM’11.
  • Maintaining Distributed Logic Programs Incrementally. [Paper]
    Vivek Nigam, Limin Jia, Boon Thau Loo and Andre Scedrov.
    13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP), Odense, Denmark, July, 2011.
  • Analyzing BGP Instances in Maude. [Paper] [Technical Report]
    Anduo Wang, Carolyn L. Talcott, Limin Jia, Boon Thau Loo, and Andre Scedrov.
    International Conference on Formal Techniques for Networked and Distributed Systems (FMOODS/FORTE), Reykjavik, Iceland, Jun, 2011. (32.3% acceptance)
  • An Operational Semantics for Network Datalog. [Paper]
    Vivek Nigam, Limin Jia, Anduo Wang, Boon Thau Loo, and Andre Scedrov.
    Third International Workshop on Logics, Agents, and Mobility (LAM), in conjunction with LICS, July 2010.
  • Formally Verifiable Networking. [Paper] [Talk] [ICNP’09 poster] [Extended PX talk]
    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. (16.0% acceptance)
  • A Theorem Proving Approach Towards Declarative Networking. [Paper] [Talk]
    Anduo Wang, Boon Thau Loo, Changbin Liu, Oleg Sokolsky, Prithwish Basu.
    (TPHOLs 2009) Emerging Trends Section, August, 2009.
  • Formalizing Metarouting in PVS. [Paper] [Talk] [TPHOLs’09 poster] [PVS codes]
    Anduo Wang, Boon Thau Loo.
    Automated Formal methods (AFM 2009), co-located with CAV09, July, 2009.
  • Declarative Network Verification. [Paper] [Talk] [Extended Technical Report]
    Anduo Wang, Prithwish Basu, Boon Thau Loo, Oleg Sokolsky.
    Eleventh International Symposium on Practical Aspects of Declarative Languages (PADL), co-located with ACM’s Principles of Programming Languages, Jan, 2009.

Funding

This research is partly supported by the AFOSR Young Investigator Award (FA9550-12-1-0327), NSF Expeditions in Computer Augmented Program Engineering (ExCAPE) project (ITR-1118996), NSF grants CNS-1040672, CNS-0845552, CCF-0820208, IIS-0812270, and the Presidio project (FA9550-08-1-0352) on Collaborative Policies and Assured Information Sharing.