It is our great pleasure to welcome you to the 11th ACM SIGSAC Workshop on Programming Languages and Analysis for Security (PLAS 2016). For the first time since PLAS began in 2006, PLAS 2016 is co-located with the ACM Conference on Computer and Communications Security (CCS). Over its now ten-year history, PLAS has provided a unique forum for researchers and practitioners to exchange ideas about programming language and program analysis techniques with the goal of improving the security of software systems.
This year, PLAS received its third-highest number of submissions, attesting to the continued vitality of the community whose work sits at the intersection of programming languages and security. PLAS has always welcomed the submission of both long research papers as well as short papers presenting preliminary or exploratory work. But, in a slight departure from previous years, the 2016 Call for Papers explicitly solicited short position papers presenting radical, open-ended and forward-looking ideas that are likely to generate lively discussion. The Call for Papers attracted 21 submissions---of which, 10 were short papers---from 13 countries (Australia, Belgium, Canada, Czech Republic, Denmark, Estonia, France, Germany, India, Italy, Romania, Sweden, USA), with authors spanning both academia and industry.
PLAS 2016 is delighted to have two excellent invited talks:
Flow: Analysis of JavaScript for type checking and beyond, Avik Chaudhuri (Facebook)
Verified Secure Implementations for the HTTPS Ecosystem, Cédric Fournet (Microsoft Research)
Proceeding Downloads
Flow: Abstract Interpretation of JavaScript for Type Checking and Beyond
Flow (https://flowtype.org) is a powerful type checker for JavaScript that we built at Facebook, with significant contributions from the open-source community. It is heavily used for web and mobile development at Facebook.
In this talk we give an ...
Static Detection of User-specified Security Vulnerabilities in Client-side JavaScript
Program defects tend to surface late in the development of programs, and they are hard to detect. Security vulnerabilities are particularly important defects to detect. They may cause sensitive information to be leaked or the system on which the program ...
On Formalizing Information-Flow Control Libraries
Many state-of-the-art IFC libraries support a variety of advanced features like mutuable data structures, exceptions, and concurrency, whose subtle interaction makes verification of security guarantees challenging. In this paper, we present a full-...
Future-dependent Flow Policies with Prophetic Variables
Content-dependency often plays an important role in the information flow security of real world IT systems. Content-dependency gives rise to informative policies and permissive static enforcement, and sometimes avoids the need for downgrading. We ...
In-Depth Enforcement of Dynamic Integrity Taint Analysis
Dynamic taint analysis can be used as a defense against low-integrity data in applications with untrusted user interfaces. An important example is defense against XSS and injection attacks in programs with web interfaces. Data sanitization is commonly ...
JSPChecker: Static Detection of Context-Sensitive Cross-Site Scripting Flaws in Legacy Web Applications
JSPChecker is a static analysis tool that detects context-sensitive cross-site scripting vulnerabilities in legacy web applications. While cross-site scripting flaws can be mitigated through sanitisation, a process that removes dangerous characters from ...
Short Paper: Rusty Types for Solid Safety
Programs operating "close to the metal" necessarily handle memory directly. Because of this, they must be written in languages like C or C++. These languages lack any kind of guarantee on memory or race safety, often leading to security vulnerabilities ...
Short Paper: Bounding Information Leakage Using Implication Graph
Quantitative information-flow analysis (QIF) is an important approach to assess confidentiality property of software systems. A crucial step towards its practical application is to develop automatic techniques for measuring the information leakage in a ...
Short Paper: Dynamic leakage: A Need for a New Quantitative Information Flow Measure
A number of measures for quantifying information leakage of a program have been proposed. Most of these measures evaluate a program as a whole by quantifying how much information can be leaked on average by different program outputs. While these ...
Verified Secure Implementations for the HTTPS Ecosystem: Invited Talk
The HTTPS ecosystem, including the SSL/TLS protocol, the X.509 public-key infrastructure, and their cryptographic libraries, is the standardized foundation of Internet Security. Despite 20 years of progress and extensions, however, its practical ...
Formal Verification of Smart Contracts: Short Paper
- Karthikeyan Bhargavan,
- Antoine Delignat-Lavaud,
- Cédric Fournet,
- Anitha Gollamudi,
- Georges Gonthier,
- Nadim Kobeissi,
- Natalia Kulatova,
- Aseem Rastogi,
- Thomas Sibut-Pinote,
- Nikhil Swamy,
- Santiago Zanella-Béguelin
Ethereum is a framework for cryptocurrencies which uses blockchain technology to provide an open global computing platform, called the Ethereum Virtual Machine (EVM). EVM executes bytecode on a simple stack machine. Programmers do not usually write EVM ...
Automatic Trigger Generation for Rule-based Smart Homes
To customize the behavior of a smart home, an end user writes rules. When an external event satisfies the rule's trigger, the rule's action executes; for example, when the temperature is above a certain threshold, then window awnings might be extended. ...
Short Paper: Superhacks: Exploring and Preventing Vulnerabilities in Browser Binding Code
In this paper, we analyze security vulnerabilities in the binding layer of browser code, and propose a research agenda to prevent these weaknesses with (1) static bug checkers and (2) new embedded domain specific languages (EDSLs). Browser ...
Index Terms
- Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security