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.