Seminar
July 9, 2003

Speaker: Tao Song, UCD Ph.D. candidate

Topic: "Formal reasoning detection rules of specification-based IDS"

Abstract: A specification-based intrusion detection system can detect unknown attacks as well as known attacks. There is an open question: Which kind of attacks can be detected with given specifications? A hierarchical model is built to reason specifications for different security requirements. A formal framework is built with ACL2 to analyze and improve detection rules of intrusion detection systems . SHIM (System Health and Intrusion Monitoring) is used as an example to show the validation of our model and framework. We formalize all specifications of SHIM and a trusted file policy and we reason about the soundness and completeness of the specifications by proving the specifications satisfy the policy with various assumptions. These assumptions are properties of the system that are not checked by the intrusion detection system. Analysis of these assumptions shows the role of SHIM in improving the security of the system.