W&M Featured Events
This calendar presented by
William & Mary
[PAST EVENT] Colloquium on Feb. 16 at 8AM in McGl 020
February 16, 2015
8am
Title: Designing Programming Languages to Build Provably Secure Systems
Speaker: Danfeng Zhang, Cornell University
Abstract: 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.
Short Bio: 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.
Speaker: Danfeng Zhang, Cornell University
Abstract: 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.
Short Bio: 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.
Contact
[[cs| liqun, Qun Li]]