Timing channels have long been a difficult and important problem for computer security. The difficulty has been recognized since the 70's, but their importance has been reinforced by recent work that shows timing information can quickly leak sensitive information, such as private keys of RSA and AES. Such threats greatly harm the security of many emerging applications, including cloud computing.
In this talk, I will introduce novel programming languages for full-system control of timing channels. First, I will introduce a light-weight software-hardware contract which enables precise reasoning about timing channels in programming languages. Second, I will show that with such a contract, a novel type system is sufficient to provably control all timing leakage, assuming the hardware obeys the contract. Third, I will introduce a new hardware description language, SecVerilog, which enables formal verification of an efficient MIPS processor that obeys the contract. Evaluation on real-world security-sensitive applications suggest that the proposed approach has reasonable performance.
Danfeng Zhang is an Assistant Professor in Computer Science and Engineering at Penn State University. He received his BS and MS degrees from Peking University, and his PhD degree from Cornell University.
Dr. Zhang's research interests include computer security and programming languages. His research focuses on designing programming models with rigorous security guarantees and minimal burden on programmers. His recent projects include sound and practical methods for full-system timing channel mitigation, language-based differential privacy proofs, as well as general methods of error localization.