Noninterference and intrusion detection

This paper presents an intrusion detection methodology based on the concept of noninterference for detecting race-condition attacks. In general, this type of attack occurs when an unprivileged process causes a privileged process to perform illegal operations by executing strategic operations in the appropriate timing window. We apply the noninterference model in a novel way that allows us to formally represent valid interleaving between privileged and unprivileged processes. Instead of proving a system satisfies noninterference assertions, we derive an algorithm for checking the assertions at run-time based on the developed theory and a formal model of Unix system calls. Our methodology can detect unknown race-condition attacks. In addition, this work provides an example of the application of formal specification and reasoning in intrusion detection.