Designing Programming Languages to Build Provably Secure Systems

Building systems with rigorous security guarantees is still difficult.
Language-based security is a promising approach, since it can offer strong
security assurance while giving programmers guidance in building secure
systems. Recent advances in language-based security show that many important
security policies can be provably enforced at the language level. However,
current research falls short in two aspects: 1) none of previous work fully
prevents timing channel attacks, an emerging threat to information security,
and 2) debugging is difficult when the program analyses that enforce security
report an error. In this talk, I will describe two of my research efforts to
tackle these limitations.

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.