Trustworthy programming for multiple instruction sets

微处理器在包含敏感数据的设备（如电话）和安全关键系统（如汽车、航空电子设备）中的使用迅速增长，增加了值得信赖的软件的价值。汇编代码特别容易出错，因为它因处理器而异，甚至在同一系列处理器的不同版本之间也不同。有些软件必须直接在汇编程序中实现，如运行时系统组件（如存储管理）、性能关键操作（如算术）和操作系统的某些部分（如中断控制器）。我们无法避免在裸机上创建至少一些代码运行。我们的目标是开发一种新的编程方法来创建可靠的汇编代码软件。本项目分为两部分：1.工程设计；自底向上创建认证代码组件，使用生成证明的汇编代码反编译成数学函数定义；2. 从数学函数定义自顶向下编译认证实现认证方面是新颖的：它们包括自动证明一种新的特定于处理器的正式规范。与最近其他关于认证汇编代码的工作不同，我们的目标不仅仅是建立弱安全属性，而是处理功能正确性、终止和资源使用。我们的目标是使用非常精确的ISA模型生成深度证明。我们的目标是对基于简化语义的相对浅层分析的补充，简化语义是当前工业规模的bug查找正式软件验证工具的基础。我们的方法没有绑定到特定的指令集。最初我们将使用两种指令集：ARM和IA-32的子集，这两种指令集都被广泛使用。我们已经获得了它们的正式规格说明。我们的目标是进行多样化和现实的案例研究，包括密码学中使用的多字算法，以及用于编译代码运行时支持的存储分配和管理例程。在项目结束时，我们希望验证一个基于纯LISP支持高精度算法的简单语言的完整解释器——这是在裸机上创建经过验证的函数式语言实现的第一步。长期应用程序（可能超出了本项目的范围）正在为真正的特定于领域的函数式语言创建经过认证的运行时代码。一个鼓舞人心的例子是基于haskell的Cryptol语言，它用于指定加密算法。我们计划招募一名博士生来探索创建经过验证的操作系统组件（如驱动程序、网络软件、软硬件接口、引导加载程序和虚拟化支持）的可行性。这将需要对硬件环境的某些部分进行建模。对于一个博士生来说，验证一个完整的操作系统可能太难了，但我们打算与犹他大学的学生合作。

The rapidly growing use of microprocessors in devices containing sensitive data (e.g. phones) and safety-critical systems (e.g. automobiles, avionics) is increasing the value of trustworthy software. Assembly code is particularly error-prone as it varies from processor to processor and even between different versions of processors in the same family. Some software must be implemented directly in assembler, such as run-time system components (e.g. storage management), performance-critical operations (e.g. arithmetic) and parts of operating systems (e.g. interrupt controllers). One cannot avoid having to create at least some coderunning on bare metal .Our goal is to develop a new programming methodology for creating trustworthy assembly code software. The project has two parts: 1. bottom-up creation of certified code components using proof-producing decompilation of assembly code into mathematical function definitions; 2. top-down compilation of certified implementations from mathematical function definitionsThe certification aspects are novel: they consist of automatically proving a new kind of processor-specific formal specification.Unlike other recent work on certified assembly code, we aim to go beyond establishing weak safety properties and instead handle functional correctness, termination and resource usage. We aim to generate deep proofs using very accurate ISA models. Our goals are complementary to the relatively shallow analyses based on the simplified semantics that underlie current industrial-scale bug-finding formal software verification tools.Our methods are not tied to a particular instruction set. Initially we will work with two instruction sets: ARM and a subset of IA-32, both of which are very widely used. We already have access to formal specifications of these.We aim to conduct diverse and realistic case studies, including multi-word arithmetic as used in cryptography and storage allocation and management routines used for runtime support of compiled code. Towards the end of the project we hope to verify a complete interpreter for a simple language based on pure LISP supporting high precision arithmetic -- a first step towards creating verified implementations of functional languages on bare metal.A long-term application, probably beyond the scope of this project, is creating certified run-time code for real domain-specific functional languages. A motivating example is the Haskell-based Cryptol language, which is used for specifying cryptographic algorithms.We plan to recruit a PhD student to explore the feasibility of creating verified operating systems components such as drivers, networking software, software-hardware interfaces, boot loaders and virtualisation support. This will require modelling parts of the hardware environment. Verifying a complete operating system is likely to be too much for a single PhD student, but we intend to collaborate with students at the University of Utah.