Model-Based Analysis of Configuration Vulnerabilities

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:

1. Formal specification of desired security properties. An example of such a property is ``no ordinary user can overwrite system log files''.

2. 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.

3. Verification techniques to check whether the abstract model satisfies the security properties.

A model-based approach can be used to detect known and as-yet-unknown vulnerabilities, in contrast 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. It shows that known techniques, such as model abstraction and constraint-based representations, can be employed to tackle the infinite-state model-checking problems that arise in 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 that automated and systematic vulnerability analysis of realistic systems to be feasible in the near future.

Bibtex Entry:

@article{RS:JCS02,
author = {C. R. Ramakrishnan and  R. Sekar},
title = {Model-Based Analysis of Configuration Vulnerabilities},
journal = {Journal of Computer Security ({JCS})},
volume = {10},
number = {1 / 2},
pages = {189--209},
year = {2002}
}

Full Paper:

[pdf]

C. R. Ramakrishnan
(cram@cs.sunysb.edu)