Formal Network Event Recognition

Purpose

Analyzing real packet traces for conformance or requirements testing of network protocols, and for recognizing anamolous events like intrusions.

People

Carl Gunter, Professor
Karthikeyan Bhargavan, PhD Student
Davor Obradovic, PhD Student
Pete McCann, Bell Labs (Collaborator)
Satish Chandra, Bell Labs (Collaborator)

Tools

NS, Network Simulator
PacketTypes, Packet Description Language
nerl, Network Event Recognition Language

Status

We have designed a language nerl to describe network monitors. We have analyzed packet event traces generated by AODV simulations in NS, using nerl. We found that the simulator code for AODV failed both conformance tests as well as requirements tests for safety properties. In order to analyize real-life packet traces on networks, we need to extend nerl to rexognize packet structures. We are investigating using PacketTypes with nerl for this purpose. In additon, real packet traces contain infidelities like packet delay, and loss. We have developed algorithms to monitor properties even in the presence of infidelities.

Papers

[1]	Karthikeyan Bhargavan and Carl A. Gunter. Requirements for a practical network event recognition language. In Proceedings of the Runtime Verification Workshop, July 2002. BibTeX entry Download PS. Download PDF.
[2]	Karthikeyan Bhargavan and Carl A. Gunter. Network event recognition for packet-mode surveillance. Submitted for publication, 2002. BibTeX entry Download PS. Download PDF.
[3]	K. Bhargavan, C.A. Gunter, M. Kim, I. Lee, D. Obradovic, O. Sokolsky, and M. Viswanathan. Verisim: Formal Analysis of Network Simulations. IEEE Transactions on Software Engineering, 28(2):129-145, February 2002. BibTeX entry Download PS. Download PDF.
[4]	Karthikeyan Bhargavan, Satish Chandra, Peter J. McCann, and Carl A. Gunter. What Packets May Come: Automata for Network Monitoring, Principles of Programming Languages, January 2001. BibTeX entry. Download PS. Download PDF.
[5]	Karthikeyan Bhargavan, Carl A. Gunter, and Davor Obradovic. Fault origin adjudication Formal Methods in Software Practice, August 2000. BibTeX entry. Download PS.
[6]	Karthikeyan Bhargavan, Carl A. Gunter, Moonjoo Kim, Insup Lee, Davor Obradovic, Oleg Sokolsky, and Mahesh Viswanathan. Verisim: Formal analysis of network simulations, August 2000. International Symposium on Software Testing and Analysis. BibTeX entry Download PS.