SHAVE: Software/Hardware Assurance Verified End-to-end
Sponsored by the Air Force Research Laboratory (AFRL) and developed with funding from DARPA, and in partnership with Bluespec, Inc., Galois’s SHAVE project implemented a streaming encryption device with an assurance case spanning hardware, firmware, and software, and a high assurance trusted boot implementation, on the open source RISC-V processor architecture.
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.