Arjun Guha
Brown University
Computer Science
Computer Science Building, Room 151
Faculty Host: Emery Berger
The Web enables new classes of programs that pose new security risks. For example, because Web programs freely mix data and code from untrusted sources, major websites have been compromised by third-party components, such as malicious ads. In addition, users cannot fully control which programs run; Web programs are visited, not installed. Therefore, Web security is entirely in the hands of programmers.
I address the problem of securing existing Web programs, which are universally written in JavaScript. Unfortunately, JavaScript has several warts that make it difficult to secure even simple snippets of code. Several companies, including Google and Facebook, have developed "Web sandboxes" to make JavaScript programming safe. However, these Web sandboxes do not come with security guarantees. I present a new type-based verification method for JavaScript that we use to find bugs in and produce the first verification of an existing, third-party Web sandbox.
Programming language techniques can give us mathematical proofs of security, but attackers attack implementations, not theorems. I discuss our approach to doing principled, real-world Web security research, which combines semantics with systems. I also review additional projects that use our tools and techniques.
Biography:
Arjun Guha is a graduate student of Computer Science at Brown University. His work focuses on securing existing Web programs and designing new programming languages for the Web. He co-developed Flapjax (a reactive programming language), LambdaJS (a semantics for JavaScript), and Google Belay (a cloud authorization protocol). More recently, he has been working on the safe management of software-defined networks.
A reception will be held at 3:40 in the atrium, outside the presentation room.