Preventing Information Leaks with Policy-Agnostic Programming with Jean Yang
Most will agree that information leaks are becoming increasingly prevalent. What people may not know, however, is that many leaks are entirely preventable. In this TechTalk, we explain what it means to be an information flow leak, discuss challenges in information flow security, and convince you that the solution is in using secure-by-construction programming models. More specifically, we will convince you that the solution is the policy-agnostic programming model, where the machine becomes responsible for implementing security and privacy policies with respect to policy-agnostic programs. Using this model for information flow security, a program needs to implement each information flow policy only once, instead of as repeated access checks across the code base. We formally explain what it means for a program to be policy-agnostic, as well as the security guarantees that we have proven. We present both static and dynamic solutions, and extensions of each for database-backed applications. We discuss results showing that, compared to traditional programs, policy-agnostic programs have 1) a smaller trusted computing base, 2) fewer lines of policy code, and 3) reasonable, often negligible, additional overheads (and no overheads with the repair-based solution).
In this TechTalk, James Mickens and Jean Yang convey this information by playing an interviewer and interviewee for a reality show.
Jean Yang is an assistant professor in the Computer Science Department at Carnegie Mellon University. She received her A.B. from Harvard and Ph.D. from MIT. Her research mission is to develop programming models and tools towards making provable guarantees ubiquitous. During her Ph.D. she created a programming language, Jeeves, that factors information flow checks out of the rest of the program. Her paper on Verve, an operating system verified for type safety, received Best Paper Award at PLDI 2010. Jean also works on analysis tools for modeling intracellular signalling using rule-based graph-rewrite programs. Jean has been studying humorous communication of scientific ideas under the patient tutelage of James Mickens since 2009.