This papers describes an approach to checking that the models of model-based anomaly detection approachs really detect malicious system calls. Especially, the approach is aimed at discovering Mimicry Attacks, that is, calls that, for instance uses a buffer overflow, to invoke malicious system call sequences disguised as none-dangerous call sequences. Previously, the discovery of mimicry attacks were done manually.
A model-based anomaly detection approach uses a model describing the "normal" and allowed behavior of a monitored system. However, model-based anonaly detection can sometimes be cheated by the use of mimicry attacks that imitates "normal" behavior and thus these attacks are not detected.
In this paper they create a model of the Operating System (OS) monitored by a model-based anomaly detection system. Then they use the OS model to create a Push Down Automaton/Push Down System of the anomaly detection system. Thereafter a model checker, given a malicious goal for an attack (for instance, to create a new user account), can automatically either find a successful attack call sequence not detected by the detection system or prove that there are no attack call sequences for that goal not detected by the modeled automaton. This means that the reliability of this approach depends heavily on that the OS model is correct.
I think this was a quite interesting paper with nice results, though I am not that familiar with model checking and formal methods.
A model-based anomaly detection approach uses a model describing the "normal" and allowed behavior of a monitored system. However, model-based anonaly detection can sometimes be cheated by the use of mimicry attacks that imitates "normal" behavior and thus these attacks are not detected.
In this paper they create a model of the Operating System (OS) monitored by a model-based anomaly detection system. Then they use the OS model to create a Push Down Automaton/Push Down System of the anomaly detection system. Thereafter a model checker, given a malicious goal for an attack (for instance, to create a new user account), can automatically either find a successful attack call sequence not detected by the detection system or prove that there are no attack call sequences for that goal not detected by the modeled automaton. This means that the reliability of this approach depends heavily on that the OS model is correct.
I think this was a quite interesting paper with nice results, though I am not that familiar with model checking and formal methods.
powered by performancing firefox
No comments:
Post a Comment