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 missionby 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 rulesand domain type rules.