An Architecture for Analysis
Joseph McMahan, Michael Christensen, Lawton Nichols, Jared Roesch, Sung-Yee Guo, Ben Hardekopf, Timothy Sherwood · IEEE Micro · 2018
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 and specification languages. This approach allows assembly-level verified versions of critical code to operate safely in tandem with arbitrary code without the need for large supporting trusted computing bases.