Title :
Noninterference and intrusion detection
Author :
Ko, Calvin ; Redmond, Timothy
fDate :
6/24/1905 12:00:00 AM
Abstract :
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.
Keywords :
Unix; authorisation; formal specification; hazards and race conditions; Unix system calls; formal model; formal specification; illegal operations; intrusion detection methodology; noninterference; privileged process; race condition attack detection; reasoning; strategic operation execution; timing window; unprivileged process; valid interleaving; Application software; Computer security; Contracts; Formal specifications; Interleaved codes; Intrusion detection; Operating systems; Protection; Runtime; Timing;
Conference_Titel :
Security and Privacy, 2002. Proceedings. 2002 IEEE Symposium on
Print_ISBN :
0-7695-1543-6
DOI :
10.1109/SECPRI.2002.1004370