ITR: Model Checking for Detecting Computer System Vulnerabilities

Securing our nation's computing and networking infrastructure against damage due to malicious attacks or spontaneous faults is a problem of paramount importance. This project aims to contribute to this mission by developing novel techniques and tools based on model checking and program analysis for vulnerability analysis: the problem of identifying and monitoring weaknesses in computer systems that can be exploited to compromise system security. A major expected outcome of the project is a set of tools for determining the consistency and safety of computer system configurationss, such as those specified by firewall rules and domain type rules.