Jonathan M. Smith, David J. Farber, Carl A. Gunter, Sampath Kannan, Insup Lee and Scott M. Nettles
DARPA-sponsored network security research in the 1970s led to the Overseer[3] idea, where network packets were checked for correctness with respect to a protocol graph. Active Networks make this feasible.
We propose to use Active Network technology to construct survivable network infrastructures based on the idea of ``self-checking'' systems. Programmable network infrastructure provides the opportunity to add network functionality ``on-the-fly''. Among the functions that can be added are modules that detect intrusions, link failures, and failures to meet quality-of-service guarantees. Building verifiable systems requires formal methods, but large-scale operation requires distributed and largely autonomous algorithms, which are presently out of reach of most formal design methods. Our research will address this problem in the context of Active Networks.
Our work takes the following approach. As suggested by early work of Cerf, Farber, and Postel, protocols are represented as graphs that show the protocol's flow of control and message emissions. Distributed systems use such protocols to operate over the network. Traversing paths through the protocol graph results in sequences of valid states, corresponding to valid sequences of messages. These message sequences are examined and validated by the programmable network infrastructure. If an invalid sequence is detected, the infrastructure performs an exceptional action, for example, raising an alarm, or blocking further messages. Different portions of the network observe different sequences of messages. Thus it is natural to design a highly distributed monitor. Such a design has the added advantage of being efficient and scalable.
We propose to use a formal language for high-level protocol specification and to perform static analysis on the protocol to verify that it meets the specification. A central idea in the proposed work is to derive checking criteria from the verified protocol. The graph of this protocol will provide a correct validation model for the message flow at each point in the network. These models can be converted to Active Network programs that behave as a sophisticated packet filter under the direction of the original protocol. This checking of state traversals can be applied broadly in an Active Net. For network security, unusual and unexpected message sequences can be used to detect large classes of intrusions. For real-time systems, timing information from a real-time program can be distilled into a time-checking algorithm for message interarrivals. Many program properties that result in message exchange in a distributed system can be ``self-checked'' by a Self-Checking Active Network (SCAN). An important property of the graph-derived self-checks is the increasing robustness of the self-checking scheme with increases in either the network scale or the complexity of the system being self-checked.
In the DARPA -funded SwitchWare project, Penn and Bellcore are investigating the use of formal methods and modern, strongly typed programming languages to build a robust Active Network node. In the work proposed here, SwitchWare nodes will serve as a programmable network infrastructure which can be loaded with monitors using the protocol graph to determine whether a message sequence is valid. We will evaluate our ideas experimentally by building a small prototype programming system that would translate protocols into packet sequence parsers, which we would inject into a SwitchWare node. Various attacks on the network infrastructure will be performed to test the strength of the relation between message sequences and correct system behavior. An extended version of this information is available.
[1] D. L. Tennenhouse, J. M. Smith, W. D. Sincoskie, D. J. Wetherall, G. Minden, "A Survey of Active Network Research," IEEE Communications, January, 1997.
[2] A. Mahmood and E. J. McCluskey, "Concurrent Error Detection Using Watchdog Processors - A Survey," in IEEE Transactions on Computers, 37(2), pp. 160-174, February, 1988.
[3] J. R. Pickens and D. J. Farber, "The Overseer: A Powerful Communications Attribute for Debugging and Security in Thin-Wire Connected Control Structures," Proceedings of International Computer Communications Conference, August 1976.
[4] "SwitchWare: Accelerating Network Evolution," U. Penn CIS TR MS-CIS-96-38, 1996, http://www.cis.upenn.edu/~jms/white-paper.ps
[5] A. Keromytis and J. Smith, "Creating Efficient Fail-Stop Cryptographic Protocols," submitted to IEEE Security and Privacy, December 2, 1996.
[6] M. Blum and S. Kannan. Designing Programs that Check their Work. Journal of the ACM, 42, 1995.
[7] I. Lee, P. Bremond-Gregoire, and R. Gerber. A Process Algebraic Approach to the Specification and Analysis of Resource-Bound Real-Time Systems. Proc. of the IEEE, pages 158--171, Jan 1994.
The SwitchWare project is funded by DARPA.