Information and networking technologies play an increasingly important role in our critical-services infrastructure, such as those for power generation and distribution, telecommunication, commerce and banking, and transportation. Securing our computing and networking infrastructure against damage due to malicious attacks or spontaneous faults is therefore a problem of paramount importance.

Vulnerability analysis statically determines whether there are legal executions of the system that can potentially violate system's security objectives. Many system vulnerabilites arise not from errors in individual components, but from the manner in which system components are combined. For instance, consider the vulnerabilty in early versions of the UNIX finger program, which was run with superuser privileges. The finger program can read the  .plan file of a fingered user. A malicious user u can symbolically link a file f as his/her .plan even if the user has no read access to f. The user then can read the file f by simply running finger u. The vulnerability arises not due to actions of individual components--- symbolic links and .plan--- but rather on their interaction.

We are developing techniques based on program analysis and concurrent system verification techniques for automatically detecting vulnerabilites resulting from complex interactions among multiple components. We plan to use a model based approach wherein each component's security-related behavior is described by a model. These models can be analyzed to derive execution sequences that lead to vulnerable system states. Using this methodology, we can not only certify whether a system is vulnerable or not, but if indeed it is vulnerable, obtain a concrete sequence of events that exhibits the vulnerability. A significant goal of the project is to develop a set of tools for determining the consistency and safety of configurations typically used to secure computer systems, such as firewall and domain type rules. The security of computer systems in practical everyday use is expected to considerably benefit from the research done in this project and the resulting tools.