STATIC ENFORCEMENT OF TERMINATION-SENSITIVE NONINTERFERENCE USING THE C++ TEMPLATE TYPE SYSTEM

A side channel is an observable attribute of program execution other than explicit communication, e.g., power usage, execution time, or page fault patterns. A side-channel attack occurs when a malicious adversary observes program secrets through a side channel. This dissertation introduces Covert C++, a library which uses template metaprogramming to superimpose a security-type system on top of C++’s existing type system. Covert C++ enforces an information-flow policy that prevents secret data from influencing program control flow and memory access patterns, thus obviating side-channel leaks. Formally, Covert C++ can facilitate an extended definition of the classical noninterference property, broadened to also cover the dynamic execution property of memory-trace obliviousness. This solution does not require any modifications to the compiler, linker, or C++ standard. To verify that these security properties can be preserved by the compiler (i.e., by compiler optimizations), this dissertation introduces the Noninterference Verification Tool (NVT). The NVT employs a novel dynamic analysis technique which combines input fuzzing with dynamic memory tracing. Specifically, the NVT detects when secret data influences a program’s memory trace, i.e., the sequence of instruction fetches and data accesses. Moreover, the NVT signals when a program leaks secret data to a publicly-observable storage channel. The Covert C++ library and the NVT are two components of the broader Covert C++ toolchain. The toolchain also provides a collection of refactoring tools to interactively transform legacy C or C++ code into Covert C++ code. Finally, the dissertation introduces libOblivious, a library to facilitate high-performance memory-trace oblivious computation with Covert C++