Using ACL2 to Verify Security Properties of Specification- based Intrusion Detection Systems
作者： Jim Alves-Foss , Karl Levitt , Calvin Ko , Cui Zhang , Tao Song
DOI:
关键词: Computer science 、 Soundness 、 Hierarchical database model 、 Intrusion detection system 、 Anomaly-based intrusion detection system 、 Misuse detection 、 ACL2 、 Anomaly detection 、 Security policy 、 Computer security
摘要: Intrusion detection is considered to be an effective technique detect attacks that violate the security policy of systems. There are basically three different kinds intrusion detection: Anomaly detection, misuse and specification-based [MB02]. Specification-based differs from others by describing desired functionalities security-critical entities including system programs, protocols, networks, application programs [CK97]. This means unknown will detected as well known attacks. open question which kind can a specific system. In this paper hierarchical model built reason specifications for requirements. A formal framework with ACL2 analyze improve rules systems [KM00]. SHIM (System Health Monitoring) used example show validation our [CK01]. We formalize all trusted file we about soundness completeness proving satisfy various assumptions. These assumptions properties not checked Analysis these shows role in improving
ucdavis.edu 参考文章(19)
Aaron Schwartzbard, Anup K. Ghosh, A study in using neural networks for anomaly and misuse detection usenix security symposium. pp. 12- 12 ,(1999)
Jia-Ling Lin, X.S. Wang, S. Jajodia, Abstraction-based misuse detection: high-level specifications and adaptable strategies ieee computer security foundations symposium. pp. 190- 201 ,(1998) , 10.1109/CSFW.1998.683169
C.R. Ramakrishnan, R. Sekar, Model-based analysis of configuration vulnerabilities Journal of Computer Security. ,vol. 10, pp. 189- 209 ,(2002) , 10.3233/JCS-2002-101-209
Karl Levitt, Dan Zerkle, NetKuang: a multi-host configuration vulnerability checker usenix security symposium. pp. 20- 20 ,(1996)
Matt Bishop, Computer Security: Art and Science ,(2002)
Calvin Ko, Paul Brutch, Jeff Rowe, Guy Tsafnat, Karl Levitt, System Health and Intrusion Monitoring Using a Hierarchy of Constraints recent advances in intrusion detection. pp. 190- 204 ,(2001) , 10.1007/3-540-45474-8_12
Panagiotis Manolios, J. Strother Moore, Matt Kaufmann, Computer-Aided Reasoning: An Approach ,(2011)
Prem Uppuluri, R. Sekar, Experiences with Specification-Based Intrusion Detection recent advances in intrusion detection. pp. 172- 189 ,(2001) , 10.1007/3-540-45474-8_11
Martin Roesch, Snort - Lightweight Intrusion Detection for Networks usenix large installation systems administration conference. pp. 229- 238 ,(1999)
Wenke Lee, S.J. Stolfo, K.W. Mok, A data mining framework for building intrusion detection models ieee symposium on security and privacy. pp. 120- 132 ,(1999) , 10.1109/SECPRI.1999.766909