Formal reasoning about intrusion detection systems

Intrusion detection is an appealing approach to improving the security of systems. The goal of intrusion detection is to detect attacks with low false positive rate and low false negative rate. New approach is needed to evaluate the effectiveness of the intrusion detection systems (IDSs).; In this dissertation, we present a formal framework for the analysis of intrusion detection systems that employ declarative rules for attack recognition. Our approach allows reasoning about the effectiveness of an IDS by formalizing and proving security properties of the IDS. Detection rules of IDSs and security requirements of the system are formalized and properties about the IDSs are proved within the framework. To illustrate the validation of our approach, we formalize and proved properties about three typical IDSs.; SHIM (System Health and Intrusion Monitoring) is used as an exemplary host-based IDS to validate our approach. We formalized all specifications of SHIM which together with a trusted file policy enabled us to reason about the soundness and completeness of the specifications by proving that the specifications satisfy the policy under various assumptions.; DRCP (Dynamic Registration and Configuration Protocol) is an auto configuration protocol in mobile Ad Hoc networks. With respect to this protocol, our approach defines a global security requirement for a network that characterizes the "good" behavior of individual nodes to assure the global property. We formally prove that the local detection rules (identifying activity that is monitored) imply the global security requirement.; OLSR (Optimized Link State Routing) protocol is a proactive, table-driven routing protocol in MANETs. We analyze a specification-based intrusion detection mechanism to detect insider attacks in the OLSR protocol. We proved that the intrusion detection approach, which focuses on monitoring of local behavior, achieves a global integrity of network routing information.; Our approach, novel to the field of intrusion detection, can, in principle, yield an intrusion detection system that detects any attack, even unknown attacks, that can imperil the security requirements of the system. The originality of our formal analysis is that it is completely based on analytical methods and does not rely on simulation or experimental evaluation.