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

Displayed time zone: Tijuana, Baja California change

10:30 - 12:00
Session 2-1PEPM at Crocker
Chair(s): Fritz Henglein DIKU, Denmark
Challenges in the Design and Compilation of Programming Languages for Exascale Machines (Invited Talk)
Alex Aiken Stanford University
Checking Cryptographic API Usage with Composable Annotations (Short Paper)
Duncan Mitchell Royal Holloway, University of London, L. Thomas van Binsbergen Royal Holloway University of London, Blake Loring , Johannes Kinder Royal Holloway, University of London