Made to Order: Verifying Correctness and Security of Hardware through Event Orderings

Correctness and security problems in modern computer systems can result from problematic hardware event orderings and interleavings during an application's execution. Since hardware designs are complex and since a single user-facing instruction can exhibit a variety of different hardware execution sequences, analyzing and verifying systems for correct event orderings is challenging. My work addresses these challenges by combining hardware architecture and systems approaches with formal methods to support the specification, analysis, and verification of implementation-aware event ordering scenarios, with the specific goal of automatically synthesizing implementation-aware programs capable of violating correctness or security guarantees. In this talk, I will present two formal, early-stage verification tools and techniques rooted in this approach. TriCheck conducts axiomatic full-stack memory consistency model (MCM) verification (from high-level programming languages down through hardware implementations). Using rigorous and efficient formal approaches, TriCheck identified flaws in RISC-V's draft MCM specification and two counterexamples to a previously proven-correct compiler mapping scheme from C11 to IBM Power and ARMv7. Noting that MCM and security analysis are amenable to similar approaches, CheckMate uses related axiomatic techniques to evaluate susceptibility of a hardware design and its related system support to formally-specified classes of security exploits; in respo