Two WiSA students graduate with doctorates
Posted 29 July 2006
Two WiSA students have successfully defended their doctoral thesis.
Shai Rubin, co-advised by Somesh Jha and Barton Miller defended his thesis
on June 28, 2006. His dissertation is entitled Formal Models and Tools
to Improve NIDS Accuracy.
It is accepted among researchers and industry professionals that the accuracy of current network intrusion detection systems (NIDS) is questionable. It is well known that NIDS generate many false alarms. It is less publicized, however, that NIDS miss equally many real attacks.
Shai's dissertation is about improving NIDS accuracy. The underlying thesis is that formal methods, previously used in areas such as software analysis and protocol verification, can help evaluate and increase the accuracy of such systems.
Shai's disseration addresses NIDS accuracy from three different directions. First, it develops a testing methodology which has already gained recognition through finding vulnerabilities in commercial systems. Second, it develops a technique to evaluate the accuracy of a NIDS signature. A signatures the core of accuracy because it specifies how a NIDS should recognize an attack. Last, it develops a novel signature that matches many different variants of the same attack.
While all of these techniques have been demonstrated to work in practice, the most important contribution of this dissertation is a set of concepts that unify them. They are based on formal methods, methods that have a solid mathematical foundations. This basis provides the ability to precisely define the test cases that should be covered during testing. For signature construction, this basis enables a definition of the properties that a signature must posses, and to verify that it indeed possesses them. The basis also enables a precise definition of all variants of an attack that a signature must identify. Further, such a mathematical basis also enables automatically conversion of the signature specification into a signature that can be used in practice.
These techniques are not a panacea for NIDS accuracy. However, they provide the means to systematically improve it. For example, the methods presented in this dissertation have been used to improve the accuracy of real network-based intrusion detection systems deployed worldwide.
Jonathon Giffin, also co-advised by Somesh Jha and Barton Miller,
defended his thesis on July 25th, 2006. Jon's dissertation is entitled
Model-Based Intrusion Detection System Design and Analysis.
Eighteen years after the original Internet worm of 1988, software still suffers from vulnerabilities that allow attackers to gain illicit access to computer systems. Attackers exploit vulnerabilities to hijack control of a process' execution as a means to access or alter a system as they desire.
Jon's dissertation argues that model-based anomaly detectors can retrofit efficient attack detection ability to vulnerable programs. These detectors restrict a process' execution using a precomputed model of normal, expected behavior. It shows how to construct models of behavior using static binary analysis. While previous statically-constructed models have traded attack detection ability for performance, the new Dyck model developed in this dissertation is the first statically-constructed model that balances security and performance, and it demonstrates that the previous trade-off was not a fundamental limitation of static analysis. The dissertation further improves the Dyck model by incorporating into the model information about data values used in the program and about the execution environment in which the program runs. It quantifies such improvements with a new evaluation metric for complex program models.
The dissertation then attacks program models. It shows how to automatically discover mimicry and evasion attacks that avoid detection by hiding malicious activity within valid behavior allowed by the model. It starts with two models: a program model of the application's execution behavior and a model of security-critical operating system state. Given unsafe OS state configurations that describe the goals of an attack, it then finds behaviors allowed as valid execution by the program model that produce the unsafe configurations. The goal here is to show that a program model allows no malicious behavior, or to find particular weaknesses in the model.
This work demonstrates the viability of model-based anomaly detection. Although the vulnerabilities of the past eighteen years may persist, model-based anomaly detection provides a mechanism to prevent attackers exploiting a vulnerability from accessing or damaging the system.
