SHF: Medium: Collaborative Research: Self Certifying Compilation and its Applications

软件被嵌入到我们的日常活动中。确保软件值得信任-做到预期的事情-并且安全-不容易受到攻击-是首要关注的问题。在建立高级程序的正确性方面投入了大量的注意力。这个项目的重点是确保编译器执行的转换通常是复杂和不透明的，而不会降低其输入程序的可信性和安全性保证。该项目追求的关键创新是自我认证，它保证了编译的正确性和安全性。自认证编译器创建有形的、可独立检查的证明，以证明编译运行的正确性。通过链接来自外部分析工具的信息，证书还可以帮助获得更好的机器代码。特别是，它们允许自动插入防御措施，以保护程序免受常见的安全攻击。这项工作建立在现有的理论思想和编译器实现的基础上，同时将它们扩展到新的方向。自认证编译器是在流行的LLVM框架中实现的，这使得它适合程序员立即采用，并以透明的方式向最终用户提供其安全好处。可证明的程序正确性是计算的一个真正的“大挑战”。通过开发自认证编译器的理论和实现，该项目在迎接这一挑战方面向前迈出了重要的一步。

Software is embedded into our daily activities. Ensuring that the software is trustworthy - does what is intended - and secure - is not vulnerable to attack - is a prime concern. Much attention has been devoted to establishing the correctness of high-level programs. This project is focused on the important task of ensuring that the, often complex and opaque, transformations carried out by a compiler do not degrade the trustworthiness and security guarantees of its input program.The key innovation pursued in this project is self-certification which guarantees the correctness and security of compilation. A self-certifying compiler creates a tangible, independently-checkable proof, justifying the correctness of the compilation run. By linking in information from external analysis tools certificates can also aid in obtaining better machine code. In particular, they allow for automatic insertion of defensive measures, which protect the program from common security attacks. This work builds on existing theoretical ideas and compiler implementations, while extending them in new directions. The self-certifying compiler is implemented in the popular LLVM framework, making it suitable for immediate adoption by programmers, and its security benefits available to end users in a transparent fashion. Provable program correctness is a true "Grand Challenge" for computing. By developing both theory and implementation of a self-certifying compiler, this project is taking a significant step forward in meeting that challenge.