PhD Defense: "Zarf: A New, Functional Architecture for Binary-Level Static Analysis and Program Safety"

Joseph McMahan

June 7th (Friday), 1:00pm
Phelps Hall, Room 1431

For highly critical workloads, the legitimate fear of catastrophic failure leads to both highly conservative design practices and excessive assurance costs. One important 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. The platform can be enhanced with hardware-based type-checking, guaranteeing that all programs loaded onto the platform are free from runtime errors.

We propose an implementation and provide an evaluation of such a device, the Zarf Architecture for Recursive Functions (Zarf), providing an 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 soundly. This can serve both resource-constrained devices, providing a new hardware platform, and resource-rich SoC’s, serving as a small, trusted co-processor that can handle critical workloads in the larger ecosystem.

About Joseph McMahan:

photo of joseph mcmahanJoseph McMahan is a Ph.D. candidate working with Timothy Sherwood in the ArchLab. His work centers around the intersection of formal methods, security, and architecture. His major project has been a novel processor architecture, Zarf, which enhances reasoning at the binary level. Other work has focused on new analysis techniques for quantifying hardware side-channels.

Hosted by: ArchLab