Computer Science and Computer Engineering students Joseph McMahan, Michael Christensen, Lawton Nichols, Jared Roesch, and Sung-Yee Guo, under the advisement of UCSB CS Professors Hardekopf and Sherwood had their work on "An Architecture for Analysis" chosen for the 2018 IEEE Micro "Top Pick" Award.  This year 12 papers we selected by a combination of industry experts and faculty from across all of the top computer architecture conferences. This is the 2nd paper from UCSB to receive the award this year. Their work explores a new type of computer, one built around lambda calculus, as a way to create truly trustworthy hardware/software systems. The resulting system can serve as a platform for computations where the cost of failure is very high such as in medical, control, or cryptocurrency applications.

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. — the authors 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. They are able to 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, they implemented an FPGA-based prototype that runs an embedded medical application which monitors and treats life-threatening arrhythmias. Though the system integrates untrusted and imperative components, the 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 noninterference proof, and a guarantee that the prototype meets critical timing requirements. The paper will appear in the May-June 2018 award edition of IEEE Micro.