CSR - - - PDOS: A New Foundation for the Evolution of Critical Systems

该项目的目标是为现有的C程序创建一条进化路径，使其成为更安全、更可验证的编程语言。大多数关键的软件系统都是用C编写的，这是出了名的容易受到错误和安全漏洞的攻击。尽管存在更安全的新语言，但除了完全重写之外，还没有办法处理现有的数百万行关键C软件。研究人员创造了新的技术，将遗留的C程序翻译成一种新的更安全的C语言变体，以及用新语言分析和重构程序的基础设施。重构允许通过大多数自动化转换在程序安全/安全性方面取得增量进展。早期的结果表明，将使用CPP预处理器的C程序转换为可重构且更易于分析的C语言变体是可能的，而且重要的重构，例如删除缓冲区溢出安全漏洞，在一些程序员指导下可以自动完成。除了翻译和重构技术之外，研究人员还计划创建一种可扩展的语言，以探索未来替代C语言的特性，这种语言既支持对遗留C语言的翻译，也支持通过重构生成更安全代码的复杂分析。主要的交付成果包括翻译和重构工具、C语言更安全变体的定义、扩展基本语言的体系结构，以及一组翻译的程序，例如驱动程序和操作系统的关键部分，它们展示了大部分自动翻译和重构，以及减少重要C程序漏洞的最终目标。

The goal of this project is to create an evolutionary path for existing C programs into a safer, more verifiable programming language. The majority of critical software systems are written in C, which is notoriously vulnerable to bugs and security holes. Although new languages exist that are safer, there has been no method for handling the millions of lines of existing critical C software, except for complete rewriting. The investigators create new technology to translate legacy C programs into a new safer variant of C, as well as the infrastructure to analyze and refactor programs in the new language. Refactoring allows incremental progress in program safety/security via mostly automated transformations. Early results show that it is possible to translate C programs with the CPP preprocessor into a variant of C that is refactorable and easier to analyze, that important refactorings, such as the removal of buffer overrun security holes, can be mostly automatic with some programmer guidance.In addition to translation and refactoring technology, the investigators plan to create an extensible language to enable exploration into the features of a future replacement language for C, one that enables both translation from legacy C, and sophisticated analyses that lead to safer code via refactoring.Key deliverables include the translation and refactoring tools, the definition of a safer variant of C, an architecture for extending the base language, and a set of translated programs, such as drivers and key parts of an OS, that demonstrate both mostly automatic translation and refactoring, and the end goal of reduced vulnerabilities for important C programs.