Systems that require strong guarantees on security policies such as those used in banking and military rely on the proper implementation of the underlying hardware in respect to the flow of information. The most challenging task has been to design such systems with provable security properties without generating significant overhead. We show that it is possible and practical to design provably information flow secure embedded processors with minimum hardware overhead. Our insight is that programming language techniques for secure information flow can be applied to the field of hardware design to enable the creation of synchronous hardware designs that are statically-verifiable as secure. Such static techniques, when used in combination with dynamic information flow tracking, can achieve significant reduction in hardware overhead and increase in expressiveness.

This dissertation presents an exploration of various approaches in designing hardware with strong security guarantees. We start by introducing Execution Lease, an architectural enforcement mechanism built upon a completely dynamic information flow tracking infrastructure. The idea is to associate every bit of data with security tags and maintain them precisely at runtime. These information are then used to provide timing and space boundary when invoking untrusted program components. In order to be able to formally reason about security properties of the resulting hardware, we propose Caisson, a programming language extension of Verilog that allows designers to specify security policies through a security type system along with explicit state machined based model. To maintain the capability of static verification while completely eliminating the need of duplicating resource for different security levels, we combine dynamic tracking techniques with language-based static verification, and introduce a new programming language Sapper. Sapper also allows designers to specify security types for data and signals, which instead of being type checked, will physically exist after fabrication and serve for the purpose of dynamic tracking. Runtime tracking and enforcement logic is generated by static analysis on the language such that the hardware overhead can be minimized along with static guarantees. At the end, we use Sapper to build complex embedded processor that is guaranteed to enforce non-interference, and we show that the hardware overhead is minimum.