Concurrency and Security Verification in Heterogeneous Parallel Systems

Abstract:

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 efficient 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.
iii
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.