The 2020 CGS/ProQuest Mathematics, Physical Sciences, and Engineering Award Winner:
Caroline J. Trippel, Princeton University
Concurrency and Security Verification in Heterogeneous Parallel Systems
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.
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-of-concept 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.
The 2020 CGS/ProQuest Humanities and Fine Arts Award Winner:
Akhil Rao, University of Colorado Boulder
The Economics of Orbit Use: Theory, Policy, and Measurement
Earth's orbits are a congestible resource with novel dynamic externalities. In this dissertation my coauthors and I examine the nature of orbit use externalities, study the policy choice space to classify existing policies and identify a class of optimal policies, consider the extent to which technological advancements can mitigate these externalities, and calculate the magnitude and time path of both an optimal satellite tax and the welfare gains from implementing it. Three key results emerge. First, open access to Earth's orbits drive the problems of excess collision risk and debris production. Left to their own devices, profit-maximizing firms may collapse the resource for generations by triggering a cascade of hazardous-fragment-producing collisions. Second, though the majority of extant policy discussions have focused on instruments targeting satellite launches, optimal policies will target satellites in orbit rather than the act of launching satellites. Despite physical uncertainty over collisions, price or quantity policy implementations are equivalent and either can maximize social welfare. Debris removal technologies cannot obviate the need for policy; they can only reduce equilibrium collision risk to the extent that satellite-owning firms pay for removal. Third, an optimal satellite tax (or orbit rental fee) for low-Earth orbit beginning in 2020 would start at approximately $40,000 USD per satellite per year, and grow at approximately 5.2% per year to preserve resource rents. The tax would increase the net present value of the satellite industry by around $1.75 trillion USD in 2020, and by over $4 trillion by 2040. Delaying action may be very costly: relative to a baseline of having begun optimal management in 2015, beginning optimal management in 2035 forgoes on the order of $4.6 trillion USD of permanent orbit use value in 2040.