Verification of Security Run-Time Verification System

Through runtime verification (RTV) a system’s behavior is checked against a specification. Almost always, specifications are easier to create and are more efficient in execution than code, thus making RTV an appealing approach to determine if a system is performing as expected. This project addresses new aspects of RTV: (1) to detect security incidents using the technique of specification-based intrusion detection originally developed at UC Davis, (2) to check that response measures taken to mitigate an attack in progress and to effect recovery perform as expected, (3) to use formal methods to verify the specifications for an RTV with respect to overall security policies, (4) to seek a general approach to RTV that unifies security and fault tolerance, and (5) to use the NASA test-bed to run experiments on an RTV (security attacks and natural faults) to identify components of the specifications that are needed in practice and to develop metrics for the effectiveness of RTVs.

Approach

In this project, we will develop a formal framework that permits analysis of the rules in intrusion detection and response systems. This analysis will be used to identify errors and improve the quality of the rules. In particular, we focus our effort on misuse detection and specification-based detection, both employing declarative rules to detect intrusive activity. Based on our experience, developing good misuse signatures and good specifications for programs is tricky and error prone. It often requires insights into the attacks and critical security aspects of a system. In
addition, one needs to be very careful when writing them to avoid gaps in coverage, or redundant coverage which degrades performance. In particular, it is hard to judge whether changes to the rules actually improve or degrade their efficacy with respect to their ability to detect new attacks. This research will explore the application of techniques from formal method research to assist the development and analysis of detection rules. We will employ verification techniques to prove that a given rule set, together with the operating system, can enforce a given
security policy. In addition, we will employ model checking techniques for identifying possible ways the policy can be violated without being detected by the detection rules. In particular, we will model the expert rules in SNORT, EMERALD and SHIM in this research. We envision that the analysis will allow one to provide a solid argument that the given intrusion detection rules can detect certain attacks and violations of certain security policies, thus providing assurance of the security of the overall system beyond the level of assurance achieved by experiments and testing. In addition to increasing the coverage of intrusion detection systems and our confidence in that coverage, we will provide a methodology to make future enhancements and to allow others to continue this work in other areas, with other intrusion detection systems, and on other platforms and automated response. Once the rules have been created and verified, experimentation against real traffic, mission tasks, and attacks will be used to 1) experimentally validate the system and 2) identify rules that might be weakened and the effect on overall security.

Funding

NSF

Contact person:
Karl Levitt
levitt@cs.ucdavis.edu

last modified 5/5/04