Tue 9 Jan 2018 11:30 - 12:00 at Crocker - Session 2-1 Chair(s): Fritz Henglein

Application developers increasingly rely on cryptographic libraries but often lack the experience to use them correctly. Popular dynamic languages such as JavaScript make testing or verifying such applications particularly challenging. In this paper, we present our ongoing work toward a methodology for automatically checking security properties in JavaScript code. Our main idea is to attach security annotations to values that encode properties of interest. We illustrate our idea using examples and, as an initial step in our line of work, we present a formalization of security annotations in a statically typed lambda calculus. As next steps, we will translate our annotations to a dynamically typed formalization of JavaScript such as $\lambda_\textsf{JS}$ and implement a runtime checked type extension using code instrumentation for full JavaScript.

Tue 9 Jan (GMT-07:00) Tijuana, Baja California change

10:30 - 12:00: PEPM 2018 - Session 2-1 at Crocker
Chair(s): Fritz HengleinDIKU, Denmark
PEPM-201810:30 - 11:30
Alex AikenStanford University
PEPM-201811:30 - 12:00
Duncan MitchellRoyal Holloway, University of London, L. Thomas van BinsbergenRoyal Holloway University of London, Blake Loring, Johannes KinderRoyal Holloway, University of London