PhD Thesis: A logic-programming approach to network security analysis

I have read this interesting PhD thesis called A logic-programming approach to network security analysis (2005) from Princeton University Computer Science Department. It is about modeling a network with respect to its security flaws. The model consists of logical statements written in Datalog that looks very similar to Prolog rules. The author captures the network topology, network and computer configurations and vulnerabilities in the model by analyzing a high-level security policy, the output from a scanner and firewall configurations.

From this model the author claims that he is able to do the following analysis (page 23):

• checking network configurations against a high-level policy specification that captures data confidentiality and integrity,
• hypothetical analysis that assumes various vulnerability situations, and
  
• the generation of attack trees.

Paper 3: Automated Discovery Of Mimicry Attacks

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.

powered by performancing firefox