CT-ISG: Reasoning about Composable Intrusion Detection Systems

University Of California-Davis, Davis CA

Investigators

Abstract

This project is developing a method to formally verify SPIDS that monitor other components of a system, including network protocols, routers, and applications. In each case, the creative steps are to (1) develop the specification that determines when an alert is to be delivered, (2) develop a security requirement against which the SPIDS is verified, and (3) carry out the verification. Beyond verifying each of these SPIDS in isolation, this proposal addresses their composition driven by the verification with respect to a global security requirement for an entire system. A running example of the system to be considered consists of a host running Linux, a wireless network running auto-configuration protocols and the OLSR routing protocol. Although not containing the functionality of a real network, this example includes most of the layers in the network protocol stack for a wireless environment.