We rely on a deep stack of abstractions to efficiently build software applications without having to completely understand the nuance of language run- times, operating systems, and processor architectures. Each layer in the stack relies on the guarantees of the layer below, with all software relying on the functionality provided by the hardware on which it executes. Similarly, when we build secure software, we define security in terms of high level application policies and rely on a stack of abstractions to enforce those policies. Therefore, all of software security relies on the guarantees provided by processor hardware. However, those guarantees offer less protection than we have traditionally assumed, and real processor implementations routinely exhibit vulnerabilities that undermine traditional assumptions about hardware behavior. Modern processors incorporate a host of optimizations to execute software as quickly and efficiently as possible; unfortunately, these optimizations are at the root of some serious security weaknesses. In particular, researchers have recently discovered easily exploitable timing-channel vulnerabilities that arise due to processor speculation, like Spectre, Meltdown, and the many variants that have since been uncovered. Concerningly, these vulnerabilities are not the result of cutting-edge, untested optimizations; they are fundamental to the de- signs of almost all processors in the last 20 years. The existence of these vulnerabilities highlights the need for a well-defined contract between software and hardware that does not allow the hardware to leak software’s secrets arbitrarily, especially via timing channels. Furthermore, we need tools to enable the construction and verification of secure processors that adhere to these new contracts. As functional processor correctness is al- ready a difficult verification problem, we likely need new approaches to prove processor security. This dissertation addresses the above concerns by applying Information Flow Control (IFC) to both the hardware–software interface and to Hardware Description Languages (HDL) themselves. By using IFC as the de facto language of security, we can define a hardware–software contract capable of providing timing-channel security without exposing extraneous details about processor internals. Intuitively, using IFC as a tool to then build processors also enables proving that real processor implementations refine this IFC contract. This dissertation also addresses the problem of constructing correct processors by introducing a high-level HDL that targets the design of efficient processor pipelines. By raising the abstraction of hardware design, we can more easily connect the implementation’s semantics to the hardware–software contract. We can also reason statically about complex optimizations such as speculation by providing abstractions that generate correct circuitry by construction. We hope that future processors and interfaces are designed with timing- channel security in mind, and that these new abstractions will percolate back up the software stack to make timing-channel security available and efficient for all applications.