1. Verifying Hypervisors
Hypervisors are a critical part of the compute infrastructure; however, proving their correctness remains challenging and often relies on project-specific efforts using ad-hoc tools and specifications.
In this project, we take the opposite approach and propose a top-down analysis of hypervisor correctness by transforming the problem of proving high-level properties, such as isolation, into a simpler problem of lock-step execution with a reference machine. As a result, we derive two sufficient criteria for hypervisor correctness: faithful emulation and faithful execution. We design the faithfulness criteria to depend solely on the specification of the architecture, enabling the re-use of existing, high-quality mechanized formal ISA specifications.
Our project aims to produce a push-button framework to verify the memory isolation and emulation correctness of RISC-V hypervisors.
2. Hardware/software contracts
The discovery of Spectre challenged many speculation optimizations in processors, compelling architects to design new defense mechanisms. While these techniques enable more programs to execute securely, they reduce execution efficiency, prompting questions about the relative security guarantees and performance tradeoffs that different defense mechanisms offer.
To characterize defenses precisely, researchers introduced hardware/software (HW/SW) contracts, which add a specification layer between the hardware's detailed micro-architectural behavior and its running software. HW/SW contracts explicitly define the security guarantees hardware enforces and specify which programs are eligible to receive these guarantees, enabling architects to formally compare and evaluate security/performance tradeoffs among the myriad proposed defenses. Researchers have primarily applied these ideas on paper, to simple microarchitectural models.
In this project, we formalize HW/SW contract machinery inside an interactive theorem prover. First, we will demonstrate how the framework allows us to specify and verify the correctness of software mitigations, such as compiler transformations that add speculative fences. Second, we plan to use the framework to characterize the defenses of functionally verified RISC-V processors we are designing in our lab.
3. Verified dataflow rewriter
Dynamically scheduled high-level synthesis transforms sequential C descriptions into dynamic dataflow graphs to generate hardware circuits. This dynamic nature enables efficient execution even with complex memory accesses that standard HLS tools cannot exploit. Engineers typically optimize these circuits by allowing extra runtime behavior through execution reordering; however, as permitted behaviors increase, reasoning about these optimizations becomes more difficult. Excessive behavioral freedom can lead to hardware that produces incorrect results or deadlocks.
We created a system in Lean (an interactive theorem prover) to reason about such circuits, enabling developers to write local transformations and verify their preservation of circuit correctness. Our framework includes a function that applies local transformations to larger circuits and generates a mechanized proof confirming the new circuit behaves like the input circuit. The framework's main contributions include:
- modular circuit semantics for abstracting subcircuits, and
- connection-agnostic semantics that avoid restricting all components to queue-based connections.