Formal verification of standards for distance vector routing protocols

ABSTRACT

We show how to use an interactive theorem prover, HOL, together with a model checker, SPIN, to prove key properties of distance vector routing protocols. We do three case studies: correctness of the RIP standard, a sharp real-time bound on RIP stability, and preservation of loop-freedom in AODV, a distance vector protocol for wireless networks. We develop verification techniques suited to routing protocols generally. These case studies show significant benefits from automated support in reduced verification workload and assistance in finding new insights and gaps for standard specifications.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Dimitri Bertsekas , Robert Gallager, Data networks, Prentice-Hall, Inc., Upper Saddle River, NJ, 1987
	2	Karthikeyan Bhargavan , Carl A. Gunter , Insup Lee , Oleg Sokolsky , Moonjoo Kim , Davor Obradovic , Mahesh Viswanathan, Verisim: Formal Analysis of Network Simulations, IEEE Transactions on Software Engineering, v.28 n.2, p.129-145, February 2002 [doi>10.1109/32.988495]
	3	Bhargavan, K., Gunter, C. A., and Obradovic, D. 2000a. An assessment of tools used in the Verinet Project. Technical Report MS-CIS-00-15, University of Pennsylvania, Philadelphia, Pa.
	4	Bhargavan, K., Gunter, C. A., and Obradovic, D. 2000b. A taxonomy of logical network analysis techniques. Technical Report MS-CIS-00-14, University of Pennsylvania, Philadelphia, Pa.
	5	Karthikeyan Bhargavan , Carl A. Gunter , Davor Obradovic, Fault origin adjudication, Proceedings of the third workshop on Formal methods in software practice, p.61-71, August 2000, Portland, Oregon, United States [doi>10.1145/349360.351132]
	6	Chiang, C.-C. 1997. Routing in clustered multihop, mobile wireless networks with fading channel. In Proceedings of IEEE SICON '97 (April 1997). IEEE Computer Society Press, Los Alamitos, Calif., pp. 197--211.
	7	Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1512-1542, Sept. 1994 [doi>10.1145/186025.186051]
	8	Cypher, D., Lee, D., Martin-Villalba, M., Prins, C., and Su, D. 1998. Formal specification, verification, and automatic test generation of ATM routing protocol: PNNI. In Formal Description Techniques & Protocol Specification, Testing, and Verification ((FORTE/PSTV) IFIP, Nov. 1998). Kluwer, Boston, Mass.
	9	Freier, A. O., Karlton, P., and Kocher, P. C. 1996. Secure socket layer. IETF draft, Nov. Available online at home.netscape.com/eng/ssl3.
	10	Lixin Gao , Jennifer Rexford, Stable Internet routing without global coordination, Proceedings of the 2000 ACM SIGMETRICS international conference on Measurement and modeling of computer systems, p.307-317, June 18-21, 2000, Santa Clara, California, United States
	11	M. J. C. Gordon , T. F. Melham, Introduction to HOL: a theorem proving environment for higher order logic, Cambridge University Press, New York, NY, 1993
	12	Timothy G. Griffin , Gordon Wilfong, An analysis of BGP convergence properties, Proceedings of the conference on Applications, technologies, architectures, and protocols for computer communication, p.277-288, August 30-September 03, 1999, Cambridge, Massachusetts, United States
	13	Griffin, T. G., and Wilfong, G. 2000. A safe path vector protocol. In Proceedings of INFOCOM 2000 Conference (Tel Aviv, Israel, March 2000). IEEE Computer Society Press, Los Alamitos, Calif.
	14	Constance Heitmeyer , James Kirby , Bruce Labaw, Applying the SCR requirements method to a weapons control panel: an experience report, Proceedings of the second workshop on Formal methods in software practice, p.92-102, March 04-05, 1998, Clearwater Beach, Florida, United States [doi>10.1145/298595.298863]
	15	Hendrick, C. 1988. Routing Information Protocol. RFC 1058, IETF. Website: www.ietf.org.
	16	Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
	17	Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
	18	Christian Huitema, Routing in the Internet, Prentice-Hall, Inc., Upper Saddle River, NJ, 1995
	19	ISO 1990. Intermediate System to Intermediate System Intra-Domain Routing Exchange Protocol for Use in Conjunction with the Protocol for Providing the Connectionless-Mode Network Service. ISO 8473. Website: www.iso.org.
	20	Jackson, D., Ng, Y., and Wing, J. 1999. A Nitpick analysis of mobile IPv6. Formal Aspects Comput. 11, 6 (Nov.), 591--615.
	21	Malkin, G. 1993. RIP, version 2: Carrying Additional Information. RFC 1388, IETF. Website: www.ietf.org.
	22	Malkin, G. 1994. RIP, version 2: Carrying Additional Information. RFC 1723, IETF. Website: www.ietf.org.
	23	Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
	24	Mitchell, J. C., Shmatikov, V., and Stern, U. 1998. Finite-state analysis of SSL 3.0. In Seventh USENIX Security Symposium (San Antonio, 1998). USENIX, Berkeley, Calif., pp. 201--216.
	25	Moy, J. 1994. OSPF, version 2. RFC 1583, IETF. Website: www.ietf.org.
	26	Shree Murthy , J. J. Garcia-Luna-Aceves, An efficient routing protocol for wireless networks, Mobile Networks and Applications, v.1 n.2, p.183-197, Oct. 1996 [doi>10.1007/BF01193336]
	27	Obradovic, D. 2002. Real-time model and convergence time of BGP. In Proceedings of IEEE INFOCOM 2002 (New York, June 2002). IEEE Computer Society Press, Los Alamitos, Calif.
	28	Charles E. Perkins , Pravin Bhagwat, Highly dynamic Destination-Sequenced Distance-Vector routing (DSDV) for mobile computers, Proceedings of the conference on Communications architectures, protocols and applications, p.234-244, August 31-September 02, 1994, London, United Kingdom
	29	Perkins, C. E., and Royer, E. M. 1998. Ad Hoc on-demand distance vector (AODV) Routing. Internet-Draft, version 2, IETF. Website: www.ietf.org.
	30	Charles E. Perkins , Elizabeth M. Royer, Ad-hoc On-Demand Distance Vector Routing, Proceedings of the Second IEEE Workshop on Mobile Computer Systems and Applications, p.90, February 25-26, 1999
	31	Radia Perlman, An algorithm for distributed computation of a spanningtree in an extended LAN, Proceedings of the ninth symposium on Data communications, p.44-53, September 1985, Whistler Moutain, British Columbia, Canada
	32	Radia Perlman, Interconnections: bridges and routers, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1992
	33	Rekhter, Y., and Li, T. 1995. A Border Gateway Protocol 4 (BGP-4). RFC 1771, IETF. Website: www.ietf.org.
	34	Royer, E. M., and Toh, C.-K. 1999. A review of current routing protocols for ad hoc mobile wireless networks. IEEE Person. Commun. 6, 2 (April), 46--55.
	35	Varadhan, K., Govindan, R., and Estrin, D. 1996. Persistent route oscillations in inter-domain routing. ISI Technical Report 96-631. USC/Information Sciences Institute, Los Angeles, Calif.
	36	Wang, B. Y., Meseguer, J., and Gunter, C. A. 2000. Specification and Formal Verification of a PLAN Algorithm in Maude. In Proceedings of the 2000 ICDCS Workshop on Distributed System Validation and Verification (April 2000), T. Lai, Ed. IEEE Computer Society Press, Los Alamitos, Calif., pp. E:49--E:56.