A Fully Function Instruction Set 

Normal, imperative architectures have been difficult to model, and the task of composing verified components is still an open problem.  This is due to many factors: large amounts of machine state, which complicates modeling and proofs; mutable machine state, which prevents abstraction and composition; large numbers of instructions and features, which must all be modeled for reasoning to be complete; arbitrary control flow, which requires approximation to soundly determine possible execution paths; unenforced call conventions, making the ``function'' an optional abstraction; implicit semantics, such as exceptions, flag updates, and other implicit mutations.

In avoiding these traits, we have designed an ISA that is small, explicit in all arguments, and completely free of state manipulation and side effects. With this higher level of abstraction, the basic building block of programs is not the instruction but the function. These are strict, mathematical functions, free of side effects and mutation, which allow precise and formal semantics to be attached to ISA operations.

Bringing Reliability to Critical Devices 

Some devices cannot tolerate failures, like those used in avionic and medical applications. We create a sample medical device, an Implanatable Cardioverter Defribillator (ICD), and show that we can reason about the Zarf assembly code to prove correctness, timing properties, and data integrity.

Two Domain Approach

Because not all existing code is amenable to being rewritten in a pure functional style for the purposes of analysis, we operate a Zarf core in tandem with a traditional microprocessor. That way, only critical application components need to be rewritten for the Zarf ISA, where they can be reasoned about in a formal and compositional way.

Why would we want anything different than traditional ISAs?

Computers today control everything from medical devices, to cryptographic exchanges, to autonomous vehicles.  However, software can exhibit subtle bugs that only show up in certain weird conditions.  Building a truly trustworthy embedded systems requires deep reasoning about the potential effects that sequences of machine instructions can have on full system operation.  When the ability to reason about and verify low-level software is a priority, it leads one to reconsider the role of the ISA.  The machine we introduce, Zarf, is a leap towards ease of analysis by executing code in a manner closely resembling the underlying computational model on which proof and reasoning systems are already built. Properties such as isolation, composition, and correctness can be reasoned about incrementally, rather than monolithically. However, instead of requiring a complete reprogramming of all software in a system, we examine a novel system architecture consisting of two cooperating layers: one built around a traditional imperative ISA, which can execute arbitrary, untrusted code, and one built around a novel, complete, purely functional ISA for reasoning about behavior at the binary level. Application behaviors that are mission critical can be hoisted piecemeal from the imperative to the functional world as needed.

Can you really build a functional machine and run software on it?

Yes!  To demonstrate the usefulness of this platform, we have developed, modeled, and tested an Implantable Cardio Defibrillator (ICD) --- an embedded medical device which is implanted in a patient's chest cavity, monitors the heart, and administers shocks under certain conditions to prevent or counter cardiac arrest. Though ICDs provide life-saving treatment for patients with serious arrhythmia, they, along with other embedded medical devices, have seen thousands of recalls due to dangerous software bugs. We were able to formally verify the correctness of a low-level implementation of the core functions in Coq and directly extract executable assembly code without needing software runtimes. The ISA semantics allow us to construct an integrity type system and formally prove that the rest of the code never corrupts the critical functions. Furthermore, the functional abstraction built into the binary code allows us to bound worst-case execution time, even in the face of garbage collection. Taken altogether, we have an embedded medical application whose core components have been proven correct, where non-interference is guaranteed, where real-time deadlines are assured to be met, and where C code can execute arbitrary auxiliary functions in parallel for monitoring.

Selected Publications

Joseph McMahan, Michael Christensen, Lawton Nichols, Jared Roesch, Sung-Yee Guo, Ben Hardekopf, and Timothy Sherwood. An Architecture for Analysis  IEEE Micro ( Volume: 38, Issue: 3, May./Jun. 2018 )

Joseph McMahan, Michael Christensen, Lawton Nichols, Jared Roesch, Sung-Yee Guo, Ben Hardekopf, and Timothy Sherwood. An Architecture Supporting Formal and Compositional Binary AnalysisProceedings of the 22th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), March 2017. Xian, China

Joseph McMahan, Michael Christensen, Kyle Dewey, Ben Hardekopf, and Timothy Sherwood. Bouncer: Static Program Analysis in Hardware Proceedings of the International Symposium of Computer Architecture. (ISCA)June 2019. Phoenix, Arizona