Skip to main content

Covid-19 Notice

All campus events (including Division of Extension sponsored events outside of Dane County) are canceled through June 30, with limited exceptions to be granted by deans or vice chancellors. Even if an event is not yet labeled as canceled, it's likely to be canceled, postponed or modified to online only, from now through June 30. Please check with organizers before attending.

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

Event Details

Monday, April 29, 2019
4-5:10 p.m.

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. TriCheckconducts 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, CheckMateuses related axiomatic techniques to evaluate susceptibility of a hardware design and its related system support to formally-specified classes of security exploits; in response, it synthesizes proof-of-concept exploit code when a design is susceptible. CheckMate automatically synthesized programs representative of Meltdown and Spectre attacks as well as new exploits, MeltdownPrime and SpectrePrime,that I have demonstrated on Intel hardware.

Coffee and cookies will be available.