SHAVE: Software/Hardware Assurance Verified End-to-end

The vast majority of today’s hardware has neither an assurance case nor any formal guarantees about its behavior. As a result, engineers who design and build high assurance systems must make assumptions about the properties of the underlying hardware on which those systems run, but cannot rely on any guarantees about the hardware’s behavior. Hardware vendors make few promises even at an informal level, much less scientific or mathematical claims, about how their systems operate. 

The primary goal of the SHAVE project was to demonstrate that building end-to-end assurance cases—claims about the top-level functionality of a system that are backed up by evidence spanning the system’s software, firmware, and hardware—is both possible and practical given the state of the art in applied formal methods tools and techniques. To do this, Galois developed the SHAVE formal method and demonstrated its efficacy by building an inline streaming encryption engine based on the RISC-V processor architecture and a formal assurance case for its correctness and security. 

Galois also used these techniques to develop a formal model and high assurance implementation of trusted boot with attestation for RISC-V.