SHF: Medium: 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.