Project Zarf

Project Zarf

Safer Computing with Functional ISAs

Zarf is a novel computer architecture designed with verifiability and analysis as a first-order constraint. By leveraging principles from functional programming, we can create a chip interface and architecture that makes it possible to reason about programs at the binary level.

The Zarf two-layer architecture: critical application components written in Haskell or Coq compile to function binaries on a lambda-execution layer, which cooperates with a traditional microprocessor running ordinary C and assembly code

A Fully Functional 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.

function main =
  let x = fact 5 in
  let out = putint 0 x in
  case out of { _ => 0 }

function fact n =
  case n of {
    0 => 1
    _ =>
      let n' = sub n 1 in
      let fact' = fact n' in
      let res = mult fact' n in
      res
  }

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 Implantable Cardioverter Defibrillator (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 Something Different?

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 system 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.

Does It Really Work?

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 Cardioverter 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 as one of 12 papers for the IEEE Micro "Top Picks" of the year
Selected as one of 12 papers for the IEEE Micro "Top Picks" of the year
Joseph McMahan led the development of Zarf in collaboration with the UCSB PL lab
Joseph McMahan led the development of Zarf in collaboration with the UCSB PL lab

Publications