Affiliations: Department of Computer Science, State University of New York, Stony Brook, NY 11794, USA. E-mail: cram@cs.sunysb.edu, sekar@cs.sunysb.edu
Correspondence:
[*]
Corresponding author.
Note: [1] This research is supported partially by DARPA-ITO under contract number F30602-97-C-0244 and by the NSF under grants EIA-9705998, CCR-9711386, CCR-9876242, and CCR-0098154.
Abstract: Vulnerability analysis is concerned with the problem of identifying weaknesses in computer systems that can be exploited to compromise their security. In this paper we describe a new approach to vulnerability analysis based on model checking. Our approach involves:
Formal specification of desired security properties. An example of such a property is “no ordinary user can overwrite system log files”.An abstract model of the system that captures its security-related behaviors. This model is obtained by composing models of system components such as the file system, privileged processes, etc.A verification procedure that checks whether the abstract model satisfies the security properties, and if not, produces execution sequences (also called exploit scenarios) that lead to a violation of these properties.
An important benefit of a model-based approach is that it can be used to detect known and as-yet-unknown vulnerabilities. This capability contrasts with previous approaches (such as those used in COPS and SATAN) which mainly address known vulnerabilities. This paper demonstrates our approach by modelling a simplified version of a UNIX-based system, and analyzing this system using model-checking techniques to identify nontrivial vulnerabilities. A key contribution of this paper is to show that such an automated analysis is feasible in spite of the fact that the system models are infinite-state systems. Our techniques exploit some of the latest techniques in model-checking, such as constraint-based (implicit) representation of state-space, together with domain-specific optimizations that are appropriate in the context of vulnerability analysis. Clearly, a realistic UNIX system is much more complex than the one that we have modelled in this paper. Nevertheless, we believe that our results show automated and systematic vulnerability analysis of realistic systems to be feasible in the near future, as model-checking techniques continue to improve.
