Verification of Security Run-Time Verification Systems

提案编号：0341734标题：安全运行时验证系统的验证PI：Karl N Levitt CoPI：Raju Pandey通过运行时验证（RTV），根据规范检查系统的行为。几乎总是，规范比代码更容易创建，执行效率更高，因此使RTV成为一种有吸引力的方法来确定系统是否按预期运行。该项目解决了RTV的新方面：（1）使用最初在加州大学戴维斯分校开发的基于规范的入侵检测技术来检测安全事件，（2）检查用于减轻正在进行的攻击并实现预期的恢复性能的响应措施，（3）使用自动化的形式化方法（即，ACL2）验证RTV关于总体安全策略的规范，（将为Unix特权程序和许多网络协议开发策略），（4）寻求统一安全性和容错性的RTV通用方法，（5）利用NASA试验台对RTV进行试验（安全攻击和自然故障），以确定在实践中所需的规范组件，并制定RTV有效性的度量标准，例如，假阳性率和假阴性率。

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.