Sciweavers

RAID
2004
Springer

Formal Reasoning About Intrusion Detection Systems

14 years 3 months ago
Formal Reasoning About Intrusion Detection Systems
We present a formal framework for the analysis of intrusion detection systems (IDS) that employ declarative rules for attack recognition, e.g. specification-based intrusion detection. Our approach allows reasoning about the effectiveness of an IDS. A formal framework is built with the theorem prover ACL2 to analyze and improve detection rules of IDSs. SHIM (System Health and Intrusion Monitoring) is used as an exemplary specification-based IDS to validate our approach. We have formalized all specifications of a host-based IDS in 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. These assumptions are properties of the system that are not checked by the IDS. Analysis of these assumptions shows the beneficial role of SHIM in improving the security of the system. The formal framework and analysis methodology will provide a sci...
Tao Song, Calvin Ko, Jim Alves-Foss, Cui Zhang, Ka
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where RAID
Authors Tao Song, Calvin Ko, Jim Alves-Foss, Cui Zhang, Karl N. Levitt
Comments (0)