Securing Computations With GPUs

Many modern computers have two diverse computing models baked-in: CPUs and GPUs. The diversity of these computing models arises from their historically disparate purposes: Early CPU designs focused on rapidly executing sequences of scalar operations, whereas GPU designs have focused on computing matrices (e.g., of pixels) through highly parallel computation. This dissertation proposes that this natural computational diversity has a secondary bene t that has gone underutilized: the potential to harden computations on both CPUs and GPUs against cyberattacks, and to elevate assurance of computational correctness, safety, and security through simultaneous CPU-GPU computation. To explore this thesis, the dissertation rst addresses the challenge of bringing machinechecked formal methods assurances and tools to the domain of GPU architectures and computations. A prototype framework for formal, machine-checked validation of GPU pseudo-assembly code algorithms using the Coq proof assistant is therefore presented and discussed. The framework is the rst to a ord GPU programmers a reliable means of formally machine-validating high-assurance GPU computations without trusting any speci c sourceto-assembly compilation toolchain. A formal operational semantics for the PTX pseudoassembly language is expressed as inductive, dependent Coq types, facilitating development of proofs and proof tactics that refer directly to compiled PTX object code. Secondly, a method of detecting malicious intrusions and runtime faults in software is proposed, which replicates untrusted computations onto the diverse but often co-located instruction architectures implemented by CPUs and GPUs. Divergence between the replicated computations signals an intrusion or fault. A prototype implementation for Java demonstrates that the approach is realizable in practice, and can successfully detect exploitation of Java VM and runtime system vulnerabilities even when the vulnerabilities are not known in advance to defenders. It is shown that GPU parallelism can be leveraged to rapidly validate CPU computations that would otherwise exhibit unacceptable performance if executed on GPU alone. Finally, GPU-based security is explored at the application level through the introduction of a computational methodology for reorienting, repositioning, and merging camera positions within a region under surveillance, so as to optimally cover all features of interest without overburdening human or machine analysts with an overabundance of video information. This streamlines many video monitoring applications, which are often hampered by the di culty of manually identifying the few speci c locations or frames relevant to a particular inquiry from a vast sea of scenes or recorded video clips. The approach ameliorates this problem by considering geographic information to select ideal locations and orientations of camera positions to fully cover the span without losing key visual details.