UC Santa Barbara

For highly critical workloads, the legitimate fear of catastrophic failure leads to both highly

conservative design practices and excessive assurance costs. One import part of the problem is

that modern machines, while providing impressive performance and efficiency, are difficult to

reason about formally. We explore the microarchitectural support needed to create a machine

with a compact and well defined semantics, lowering the difficulty of sound and compositional

reasoning across the hardware/software interface. Specifically, we explore implementation

options for a machine organization devoid of programmer-visible memory, registers, or state

update, built instead around function primitives. The resulting machine can be precisely and

mathematically described in a brief set of semantics, which we quantitatively and qualitatively

demonstrate is amenable to software proofs at the binary level.

As time continues, we become increasingly dependent on computational devices for all

facets of our lives — including our health, well-being, and safety. Many of these devices live

“in the wild,” in resource-constrained and/or embedded environments, without access to large

software stacks and heavy language run-times. At the same, increasing trends in heterogeneity

in computer architecture gives the opportunity for new cores in system-on-chips (SoC’s) that

provide support for increasing critical workloads. We propose an implementation and provide

an evaluation of such a device, the Zarf Architecture for Recursive Functions (Zarf), provid-

ing a interface of reduced semantic complexity at the ISA level, giving designers a platform

amenable to reasoning and static analysis. The described prototype is comparable to normal

embedded systems in size and resource usage, but it is far easier to reason about programs

according to analysis. This can serve both resource-constrained devices, providing a new hard-

ware platform, and resource-rich SoC’s, serving as a small, trusted co-processor that can handle

critical workloads in the larger ecosystem.