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.