To achieve performance scaling at manageable power and thermal levels, modern

systems architects employ parallelism along with high degrees of hardware specialization and heterogeneity. Unfortunately, the power and performance improvements

afforded by heterogeneous parallelism come at the cost of significantly increased design

complexity, with different components being programmed differently and accessing

shared resources differently. This design complexity in turn presents challenges for

architects who need to devise mechanisms for orchestrating, enforcing, and verifying

the correctness and security of executing applications.

As it turns out, software-level correctness and security problems can result from

problematic hardware event orderings and interleavings that take place when an

application executes on a particular hardware implementation. Since hardware designs

are complex, and since a single user-facing instruction can exhibit a variety of different

hardware execution event sequences, analyzing and verifying systems for correct

and secure orderings and interleavings of these events is challenging. To address

this issue, this dissertation combines hardware systems architecture approaches with

formal methods techniques to support the specification, analysis, and verification of

implementation-aware event ordering scenarios. The specific goal here is enabling

automatic synthesis of implementation-aware programs capable of violating correctness

or security guarantees when such programs exist.

First, this dissertation presents TriCheck, an approach and tool for conducting

full-stack memory consistency model verification (from high-level programming languages down through hardware implementations). Using rigorous and ecient formal

approaches, TriCheck identified flaws in the 2016 RISC-V memory model specification

and two counterexamples to a previously proven-correct compiler mapping scheme

from C11 onto Power and ARMv7.

Second, after making the important observation that memory consistency model

and security analyses are amenable to similar approaches, this thesis presents CheckMate, an approach and tool for conducting hardware security verification. CheckMate

uses formal techniques to evaluate susceptibility of a hardware system design to

formally-specified security exploit classes. When a design is susceptible, proof-ofconcept exploit codes are synthesized. CheckMate automatically synthesized programs

representative of Meltdown and Spectre and new exploits, MeltdownPrime and SpectrePrime.

Third, this dissertation presents approaches for handling memory model heterogeneity in hardware systems, focusing on correctness and highlighting applicability of

the proposed techniques to security.