一句话：提出一种对应 λ 演算的嵌入式计算层架构，使汇编级代码可组合地形式验证，并能与不可信代码安全共存。
针对安全攸关嵌入式系统中完整二进制难以推理、验证代码难以与任意指令式或未验证组件安全共存的问题，论文提出一种由薄计算层控制的体系结构，该层与 λ 演算紧密对应，借助函数式编程原则使汇编更接近 Coq 等推理框架。该计算层在提供完整可编程性的同时具有紧凑、精确且完备的语义，硬件开销与普通嵌入式系统相当。作者用 FPGA 实现原型运行嵌入式医疗应用（监测与治疗致命性心律失常），尽管系统集成未验证指令式组件，仍对端到端系统多属性进行形式验证，包括核心算法汇编实现正确性、可信数据非干涉完整性以及关键时序要求。
Building a trustworthy life-critical embedded system requires deep reasoning about the potential effects that sequences of machine instructions can have on full system operation. Rather than trying to analyze complete binaries and the countless ways their instructions can interact with one another --- memory, side effects, control registers, implicit state, etc. --- we explore a new approach. We propose an architecture controlled by a thin computational layer designed to tightly correspond with the lambda calculus, drawing on principles of functional programming to bring the assembly much closer to myriad reasoning frameworks, such as the Coq proof assistant. This approach allows assembly-level verified versions of critical code to operate safely in tandem with arbitrary code, including imperative and unverified system components, without the need for large supporting trusted computing bases. We demonstrate that this computational layer can be built in such a way as to simultaneously provide full programmability and compact, precise, and complete semantics, while still using hardware resources comparable to normal embedded systems. To demonstrate the practicality of this approach, our FPGA-implemented prototype runs an embedded medical application which monitors and treats life-threatening arrhythmias. Though the system integrates untrusted and imperative components, our architecture allows for the formal verification of multiple properties of the end-to-end system, including a proof of correctness of the assembly-level implementation of the core algorithm, the integrity of trusted data via a non-interference proof, and a guarantee that our prototype meets critical timing requirements.
@inproceedings{McMahanCNRGHS17,
title = {An Architecture Supporting Formal and Compositional Binary Analysis},
author = {Joseph McMahan and Michael Christensen and Lawton Nichols and Jared Roesch and Sung-Yee Guo and Ben Hardekopf and Timothy Sherwood},
booktitle = {ASPLOS},
year = {2017},
doi = {10.1145/3037697.3037733}
}