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.