Model-Based Vulnerability Analysis of Computer Systems

C. R. Ramakrishnan, R. Sekar


Vulnerability analysis is concerned with the problem of identifying weaknesses in computer systems that can be exploited to compromise their security. Most vulnerabilities arise from unexpected interactions between different system components such as server processes, filesystem permissions and content, and other operating system services. Existing vulnerability techniques (such as those used in COPS and SATAN) are based on enumerating the known causes of vulnerabilities in the system and capturing these causes in the form of rules, e.g., a world- or group-writable .login file is a well known vulnerability that enables one user to gain all access privileges of another user. However, the generation of the rules relies on expert knowledge about interactions among many components of the system. Issues such as system complexity, race conditions, many possible interleavings, hidden assumptions etc. make it very hard even for experts to come up with all such rules. In contrast, we propose a new model-based approach where the security-related behavior of each system component is modeled in a high-level specification language such as CSP or CCS. These component models can then be composed to obtain all possible behaviors of the entire system. Finding system vulnerabilities can now be accomplished by analyzing these behaviors using automated verification techniques (model checking in particular) to identify scenarios where security-related properties (such as maintaining integrity of password files) are violated. In contrast to previous approaches that mainly address well-known vulnerabilities, our model-based approach has the potential to automatically seek out and identify known and as-yet-unknown vulnerabilities.

Bibtex Entry:

author = {C. R. Ramakrishnan and  R. Sekar},
title = {Model-Based Vulnerability Analysis of Computer Systems},
booktitle = {Second International Workshop on Verification, Model Checking, and Abstract Interpretation ({VMCAI})},
address = {Pisa, Italy},
month = {September},
year = {1998}

Full Paper: [pdf]

Home | Papers

C. R. Ramakrishnan