Reclaiming Security for Web Programmers Arjun Guha , University of Massachusetts, Amherst Thursday, November 21, 4:30pm Computer Science, 105 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, not users. 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 reason about even simple snippets of code. Several companies have developed "Web sandboxes" to make JavaScript programming safe. However, these Web sandboxes have no security guarantees. In this talk, I show how programing languages research can be used to verify properties of Web applications. I present a 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. Arjun Guha is an assistant professor of Computer Science at UMass Amherst. He enjoys tackling practical problems, while adhering to the mathematical foundations of programming languages. For example, his dissertation on JavaScript semantics and type-checking, from Brown University, is used by several other researchers as a foundation for their own work. As a postdoc at Cornell University, he developed a model of software-defined networking (SDN) in the Coq Proof Assistant, which is the foundation for a verified runtime and other SDN tools. For his research, he has developed and contributed to several software systems, such as LambdaJS, Frenetic, and Flapjax that are in active use.