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

点击翻译按钮获取中文摘要

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.