<html><head><style type='text/css'>p { margin: 0; }</style></head><body><div style='font-family: arial,helvetica,sans-serif; font-size: 12pt; color: #000000'><b>Reclaiming Security for Web Programmers</b>
<br>
<b><a href="http://people.cs.umass.edu/%7Earjun/">Arjun Guha</a></b>, <a href="http://www.umass.edu/">University of Massachusetts, Amherst </a>
<br>Thursday, November 21, 4:30pm<br>Computer Science, 105<br><br><br>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.<br><br><p>
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. <br></p><p><br></p><p>
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.
</p><p>
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. <br></p><p><br></p>
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.
<div><span name="x"></span><br></div><br></div></body></html>