First, I will introduce a light-weight software-hardware contract which enables precise reasoning about timing channels in programming languages. The contract brings just enough timing information to the language level. With such information, a novel type system is sufficient to provably control all possible timing leakage in the entire computer system, assuming the hardware obeys the contract. On the hardware side, enforcing the contract is not only possible, but also can be done efficiently. A new hardware description language, SecVerilog, enables formal verification of an efficient MIPS processor that obeys the contract.
In the second part of my talk, I will introduce SHErrLoc, a general tool that diagnoses static errors arising from a large class of program analyses, including those enforcing security. Based on Bayesian reasoning, SHErrLoc provides high-quality error localization without any language-specific knowledge. Evaluation shows that, SHErrLoc identifies error locations significantly more accurately than existing tools for OCaml, Haskell and Jif.
Danfeng Zhang is a Ph.D. candidate in the Department of Computer Science at Cornell University, advised by Andrew Myers. His research interests lie in the intersection of security and programming languages, with a focus on designing programming models with rigorous security guarantees and minimal burden on programmers.