A temporal logic based framework for intrusion detection
By
We propose a framework for intrusion detection that is based on runtime monitoring of temporal logic specifications. We specify intrusion patterns as formulas in an expressively rich and efficiently monitorable logic called Eagle. Eagle supports data-values and parameterized recursive equations, and allows us to succinctly express security attacks with complex temporal event patterns, as well as attacks whose signatures are inherently statistical in nature. We use an online monitoring algorithm that matches specifications of the absence of an attack, with system execution traces, and raises an alarm whenever the specification is violated. We present our implementation of this approach in a prototype tool, called Monid and report our results obtained by applying it to detect a variety of security attacks in log-files provided by DARPA.
Keywords Intrusion detection - security - temporal logic - runtime monitoring
BibTeX
@inproceedings{conf/forte/NaldurgST04,
author = "Naldurg, Prasad and Sen, Koushik and Thati, Prasanna",
editor = "de Frutos-Escrig, David and Núñez, Manuel",
title = "A Temporal Logic Based Framework for Intrusion Detection",
booktitle = "FORTE",
crossref = "conf/forte/2004",
ee = "http://dx.doi.org/10.1007/978-3-540-30232-2_23",
keywords = "formal methods, software engineering",
pages = "359-376",
year = "2004",
}
@proceedings{conf/forte/2004,
editor = "de Frutos-Escrig, David and Núñez, Manuel",
title = "Formal Techniques for Networked and Distributed Systems -
FORTE 2004, 24th IFIP WG 6.1 International Conference, Madrid
Spain, September 27-30, 2004, Proceedings",
isbn = "3-540-23252-4",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
volume = "3235",
year = "2004",
}