Verification of Security Run-Time Verification Systems

University Of California-Davis, Davis CA

Investigators

Abstract

Proposal #: 0341734 TITLE: Verification of Security Run-Time Verification Systems PI: Karl N Levitt CoPI: Raju Pandey 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 automated formal methods (i.e., ACL2) to verify the specifications for RTV with respect to overall security policies, (policies will be developed for Unix privileged programs and for numerous network protocols), (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, e.g., false positive and false negative rates.