TWC: Small: Trustworthy Code Generation for the LLVM Compiler Infrastructure

软件应用程序以虚拟指令集(即，作为“虚拟代码”)，并在发货后转换为物理计算机的指令集(“机器代码”)，例如在将应用程序下载到iPhone时或就在执行嵌入许多网页中的代码之前。越来越多的LLVM虚拟指令集(由首席研究人员在之前的NSF资助下开发)正被各个行业使用。此模型的一个严重问题是，应用程序开发人员无法测试为其应用程序生成的最终计算机代码：他们只能测试虚拟代码。该项目正在开发新技术，使应用程序开发人员能够对作为虚拟代码发布的应用程序的最终代码有更高的信心。基本方法称为“翻译验证”，它允许从虚拟代码到机器代码的翻译过程还生成一个正式证明，证明机器代码保留了虚拟代码的所有正确行为，并且不会引入任何意外的不正确行为。与现有的翻译验证工作不同，该工作可以为两种非常不同的语言之间的翻译生成证明，以及在虚拟代码中存在可能的不正确行为的情况下的形式保证。除了这些可靠性优势外，该策略还提高了软件的安全性，因为虚拟代码如今被广泛用作加强重要系统(例如Web浏览器、操作系统和数据库系统)的安全要求的手段。这样的系统依赖于虚拟代码到机器代码的正确转换来加强安全性，正式验证的转换将防止安全漏洞，否则可能会由复杂(因此，天生容易出现错误的)翻译器中的错误引入安全漏洞。

It is becoming widespread practice for software applications to be shipped in the form of a virtual instruction set (i.e,. as "virtual code") and translated to the instruction set of a physical computer ("machine code") after shipping, e.g., when downloading an app to an iPhone or just before execution for code embedded in many Web pages. Increasingly the LLVM virtual instruction set (developed by the principal investigator under prior NSF funding) is being used by various industries. A serious problem with this model is that application developers are unable to test the final computer code that is generated for their applications: they are only able to test the virtual code.This project is developing new techniques that allow application developers to have much higher confidence in the final code for applications that ship as virtual code. The basic approach, called "translation validation," allows the translation process from virtual to machine code to also generate a formal proof that the machine code preserves all the correct behaviors of the virtual code, and does not introduce any unexpected incorrect behaviors. Unlike existing work on translation validation, this work can generate proofs for translation between two very different languages, as well as formal guarantees in the presence of possible incorrect behaviors in the virtual code. Besides these reliability benefits, the strategy also improves the security of software because virtual code is widely used today as a means to enforce security requirements of important systems, e.g., Web browsers, operating systems, and database systems. Such systems rely on correct translations of virtual code to machine code to enforce security, and formally verified translations will prevent security vulnerabilities that might otherwise be introduced by bugs in complex (and so, inherently bug-prone) translators.