Sound And Practical Methods For Full-System Timing Channel Control

Abstract

Building systems with rigorous security guarantees is difficult, because most programming languages lack support for reasoning about security. This situation is amplified by emerging timing attacks, which reveal secrets from computation time. Recent work shows that timing channels can quickly leak sensitive information, such as private keys of RSA and AES. Such threats greatly harm the security of many emerging applications, such as cloud computing, mobile computing, and embedded systems. This dissertation describes novel programming languages and run-time enforcement mechanisms for full-system control of timing channels. The proposed approach has two major components: A new software-hardware security interface, and control mechanisms present at separate levels of system abstraction. These control mechanisms include: 1) A type system for an imperative language, so that well-typed programs provably leak only a bounded amount of information via timing channels, 2) SecVerilog, a hardware description language that supports mostly-static, precise reasoning about information flows in hardware designs, and 3) Predictive mitigation, a general run-time mechanism that permits tunable tradeoffs between security and performance. Evaluation on real-world security-sensitive applications suggest that the proposed approach is sound and has reasonable performance.