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.