[PRL] Fwd: [Programming] PL Seminar April 30 at 4pm -- Arjun Guha

[Vincent St-Amour]

May be of interest to some people here. It's at Harvard.

Vincent


At Mon, 28 Apr 2014 20:58:11 +0000,
Waye, Lucas wrote:
> 
> Arjun Guha from UMass Amherst will be speaking Wednesday, April 30th at 4pm in MD 323.
> 
> Reclaiming Security for Web Programmers
> 
> The Web enables new classes of programs that pose new security risks.  For
> example, because Web programs freely “mashup” 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.
> 
> 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 languages 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 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. He has developed and contributed to several
> software systems, such as LambdaJS, Frenetic, and Flapjax.
> 
> 
> Programming mailing list
> Programming at eecs.harvard.edu
> https://lists.eecs.harvard.edu/mailman/listinfo/programming