Developers of high-security systems (e.g., cryptographic libraries, web browsers) mustnot allow sensitive information (e.g., encryption keys, browser cookies) to make its way to an attacker. However, clever attackers can make use of unintentional side-channels—such as timing information or other hardware resource metrics—to infer or leak the values of these secrets. Even worse, attackers can exploit hardware features such as speculative execution to create new vectors for side-channel leakage even where none existed before.

Side-channels are not typically captured in formal program semantics—information froma side-channel is leaked to an attacker purely as a side-effect of execution, rather than any explicit data flow. Furthermore, speculative execution fundamentally destroys security properties like memory or type safety, as they implicitly assume a standard sequential execution model. Without formal models to rely on, developers find themselves manually applying ad-hoc mitigations as a best-effort solution to prevent timing side-channels and speculative attacks. Unfortunately, these ad-hoc mitigations often lead to obfuscated code—and yet give no guarantee of a sound or complete defense.

This dissertation seeks to remedy this. We explore several formal frameworks that makeside-channel effects explicit, both with and without the threat of speculative execution. Along the way, we introduce FaCT, a language and compiler for writing code free from side-channels; Pitchfork, a semantics and tool for detecting speculative side-channels in binaries; and ZFI, a framework for validating sandbox protections against speculative attacks. In addition to the systems presented in this dissertation, the research community writ large has developed several program analysis and defense tools backed by formal models, whether these models are explicit or implicit. We round out this dissertation by surveying these systems, examining various design choices and identifying areas of open research.

Ultimately, this dissertation demonstrates the power of practical, formal foundationswhen dealing with speculative side-channel security. By relying on sound, formal frameworks, high-security developers can write programs that verifiably do not leak sensitive information.