TWC: Medium: Collaborative: Retrofitting Software for Defense-in-Depth

长期以来，计算机安全界一直倡导构建多层防御来保护系统的概念。不幸的是，在软件开发实践中很难实现这一愿景，而且软件往往带有不足的防御，通常是以临时方式开发的。开发人员在保护具有多层防御的软件系统时面临着许多挑战。他们缺乏完整的框架来表达不同软件层的策略和机制，缺乏自动工具来添加这些防御，以及缺乏工具来证明增强了防御的软件具有宣传的保证水平。该项目开发了新的技术来升级软件，以进行纵深防御。它对问题有一个全面的看法，重点是自动化的交互工具，开发人员可以使用这些工具来确定站点级别的安全目标，探索添加安全机制的设计空间，并改造旧代码以以机器验证的方式实施安全策略以确保安全。该项目开发了用于正式策略语言设计和验证的理论和工具、静态和动态代码分析、为开发人员探索安全、功能和性能权衡设计空间的交互工具，以及正式验证程序转换的正确性的方法，以引入授权、攻击者遏制和审计机制等防御措施。更广泛的影响源于系统安全性的提高和实现更好安全性的成本的降低，以及研究生、本科生和高中生暑期学校形式的教育活动。开发的工具将向公共领域发布，使该领域的软件开发人员受益。

The computer security community has long advocated the concept of building multiple layers of defense to protect a system. Unfortunately, it has been difficult to realize this vision in the practice of software development, and software often ships with inadequate defenses, typically developed in an ad hoc fashion.Developers face a number of challenges when protecting a software system with multiple layers of defense. They lack holistic frameworks in which to express policies and mechanisms for different software layers, automated tools to add these defenses, and tools to prove that software enhanced with defenses has an advertised level of assurance.This project develops new techniques to retrofit software for defense in depth. It takes a comprehensive view of the problem, with an emphasis on automated, interactive tools that developers can use to identify site-level security goals, explore the design space of adding security mechanisms, and retrofit legacy code to enforce security policies in a manner that can be machine-verified for assurance. The project develops theory and tools for formal policy language design and validation, static and dynamic code analyses, interactive tools for developers to explore the design space of security, functionality and performance tradeoffs, and methods to formally verify the correctness of program transformations to introduce defenses such as authorization, attacker containment, and auditing mechanisms.The broader impact stems from the improved security of systems and the reduced cost of achieving better security, also education activities in the form of summer schools for graduate, undergraduate and high-school students. The tools developed will be released to the public domain, benefiting software developers in the field.