Verification of Security Run-Time Verification Systems

点击翻译按钮获取中文摘要

Proposal #: 0341734TITLE: Verification of Security Run-Time Verification SystemsPI: Karl N LevittCoPI: Raju PandeyThrough runtime verification (RTV) a system's behavior is checkedagainst a specification. Almost always, specifications are easier tocreate and are more efficient in execution than code, thus making RTV anappealing approach to determine if a system is performing as expected.This project addresses new aspects of RTV: (1) to detect securityincidents using the technique of specification-based intrusion detectionoriginally developed at UC Davis, (2) to check that response measurestaken to mitigate an attack in progress and to effect recovery performas 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 areneeded in practice and to develop metrics for the effectiveness of RTVs, e.g., false positive and false negative rates.