Verification of Routing Protocols

Purpose

The formal verification of correctness for routing protocols. We have analyzed the Routing Information Protocol for IP networks, Flow-based Adaptive Routing for active networks, Ad-hoc On-demand Distance Vector Routing for wireless networks and the Border Gateway protocol for Inter-domain routing in the internet.

People

Carl Gunter, Professor
Karthikeyan Bhargavan, PhD Student
Davor Obradovic, PhD Student
Bow Yaw Wang, PhD Student (Collaborator)
Jose Meseguer, SRI (Collaborator)
Luc Ong, Cambridge (Collaborator)

Tools

HOL90, Theorem Prover
SPIN, Model Checker
PVS, Theorem Prover
Maude, Rewriting System

Status

Protocol	Requirement	Status	Personnel	Tools
Routing Information Protocol	Convergence of routes	Proved convergence. Derived sharp real-time bounds.	Karthikeyan Bhargavan, Carl Gunter Davor Obradovic	HOL90, SPIN, PVS
Ad-hoc On-demand Distance Vector Routing Protocol	Loop-freedom of routes	Demonstrated failure of loop-freedom. Proved loop-freedom under assumptions.	Karthikeyan Bhargavan, Carl Gunter, Davor Obradovic	HOL90, SPIN
Border Gateway Protocol	Route Convergence		Davor Obradovic, Carl Gunter
FBAR - an active network routing protocol		Carried out instance verification	Bow Yaw Wang, Carl Gunter	Maude

Papers

[1]	Karthikeyan Bhargavan, Davor Obradovic, and Carl A. Gunter. Formal verification of standards for distance vector routing protocols, 2002. Journal of the ACM, to appear. BibTeX entry Download PS. Download PDF.
[2]	Davor Obradovic. Real-time Model and Convergence Time of BGP, Proceedings of IEEE INFOCOM, 2002. BibTeX entry. Download PS.
[3]	Karthikeyan Bhargavan, Carl A. Gunter, and Davor Obradovic. RIP in SPIN/HOL, Theorem Proving and Higher Order Logics, August 2000. BibTeX entry. Download PS.
[4]	Karthikeyan Bhargavan, Davor Obradovic, and Carl A. Gunter. Formal verification of standards for distance vector routing protocols, 2000. Working Paper. Presented in the Recent Research Session at Sigcomm 1999. BibTeX entry
[5]	Bow-Yaw Wang, José Meseguer, and Carl A. Gunter. Specification and formal verification of a PLAN algorithm in Maude. In Tenh Lai, editor, Proceedings of the 2000 ICDCS workshop on Internet 2000, Distributed Real-Time Systems, Group Computation and Communications, Wireless Networks and Mobile Computing, Distributed System Validation and Verification, Knowledge Discovery and Data Mining in the World Wide Web, pages E:49-E:56. IEEE Computer Society, April 2000. BibTeX entry