CAREER: Security in the Large: Gaining Assurance in Real-World Systems

随着我们进入全球网络、无处不在的计算设备和电子商务的所谓“信息时代”，计算机安全变得越来越重要。当今计算机安全的最大挑战之一是软件保证问题：我们如何处理我们最信任的软件，甚至我们的安全软件本身，经常有漏洞的事实？本研究将研究软件保障问题的两个方面：首先确保不发生不好的事情，其次确保发生好的事情。该项目将探索遗留软件的漏洞检测，重点是检测在安全问题变得像今天这样严重之前构建的系统中普遍存在的安全漏洞类型。此外，这项工作还将研究构建需要安全的新系统的基础设施支持。启用技术是轻量级形式化方法（例如静态程序分析）与特定于领域的启发式方法的混合，主要目标是构建可在实践中使用的工具。在每种情况下，该方法的一个关键卖点是，它允许我们在漏洞被利用之前主动消除或消除安全漏洞。

As we enter the so-called "information age" of global networks, ubiquitous computing devices, and electronic commerce, computer security is of increasing importance. One of the greatest challenges in computer security today is the software assurance problem: How do we deal with the fact that our most trusted software, even our security software itself, is often buggy?This research will study two aspects of the software assurance problem: ensuring first that bad things do not happen, and second that good things do happen. The project will explore vulnerability detection of legacy software, focusing on detecting the types of security bugs that pervade systems built before security became as serious a concern as it is today. Also this work will study infrastructural support for building new systems that need to be secure. The enabling technology is a mix of lightweight formal methods (such as static program analysis) coupled with domain-specific heuristics, and a main goal will be to build tools that can be used in practice. In each case, a key selling point of the approach is that it allows us to proactively eliminate or neutralize security bugs before they are exploited.