ACM SIGSAC 15^th Workshop on Programming Languages and Analysis for Security (PLAS 2020)

Friday November 13, 2020 - Virtual Event
(Co-located with ACM CCS 2020)

News

The videos of the workshop are available here.
The proceedings of the workshop are available here.

Program

Friday November 13, 2020

Time EST CET	Session	Chair
16:00 - 16:10 10:00 - 10:10	Opening Remarks
16:10 - 17:10 10:10 - 11:10	Invited Talk 1 From Verified Compilation to Secure Compilation: a Semantic Approach Sandrine Blazy (University of Rennes, France)	Marco Vassena
17:10 - 17:25 11:10 - 11:25	Virtual Coffee Break
17:25 - 18:15 11:25 - 12:15	Secure Multiparty and Oblivious Computation Short Paper: Secure Multiparty Logic Programming Alisa Pankova, Joosep Jääger Short Paper: Probabilistically Almost-Oblivious Computation Ian Sweet, David Darais, Michael Hicks	Deian Stefan
18:15 - 19:15 12:15 - 13:15	Lunch / Dinner Break
19:15 - 20:05 13:15 - 14:05	Types for Gradual Security and Verification of Security Protocols Short Paper: Weak Runtime-Irrelevant Typing for Security Matthías Páll Gissurarson, Agustín Mista Short Paper: Modular Black-box Runtime Verification of Security Protocols Kevin Morio, Dennis Jackson, Marco Vassena, Robert Künnemann	Anitha Gollamudi
20:05 - 20:20 14:05 - 14:20	Virtual Coffee Break
20:20 - 21:20 14:20 - 15:20	Invited Talk 2 How APIs Are Both the Illness and the Cure Jean Yang (Akita Software, USA)	Alley Stoughton
21:20 - 21:35 15:20 - 15:35	Virtual Coffee Break
21:35 - 22:25 15:35 - 16:25	Program Synthesis and Blockchain Automatic Discovery and Synthesis of Checksum Algorithms from Binary Data Samples Lauren Labell, Jared Chandler, Kathleen Fisher Short Paper: Blockcheck the Typechain Sergio Benitez, Jonathan Cogan, Alejandro Russo	Scott Moore
22:25 - 22:55 16:25 - 16:55	Discussion and Closing Remarks

Accepted Papers

Automatic Discovery and Synthesis of Checksum Algorithms from Binary Data Samples
Lauren Labell (Tufts University), Jared Chandler (Tufts University), Kathleen Fisher (Tufts University)
Short Paper: Blockcheck the Typechain
Sergio Benitez (Stanford University), Jonathan Cogan (Stanford University), Alejandro Russo (Chalmers University of Technology)
Short Paper: Modular Black-box Runtime Verification of Security Protocols
Kevin Morio (CISPA Helmholtz Center for Information Security), Dennis Jackson (ETH Zurich), Marco Vassena (CISPA Helmholtz Center for Information Security), Robert Künnemann (CISPA Helmholtz Center for Information Security)
Short Paper: Probabilistically Almost-Oblivious Computation
Ian Sweet (University of Maryland, College Park), David Darais (University of Vermont), Michael Hicks (University of Maryland, College Park)
Short Paper: Secure Multiparty Logic Programming
Alisa Pankova (Cybernetica AS), Joosep Jääger (Cybernetica AS)
Short Paper: Weak Runtime-Irrelevant Typing for Security
Matthías Páll Gissurarson (Chalmers University of Technology), Agustín Mista (Chalmers University of Technology)

Invited Speakers

Sandrine Blazy
(University of Rennes, France)

Abstract. A formally verified compiler is a compiler that comes with a machine-checked proof that no bug is introduced during compilation. This correctness property states that the compiler preserves the semantics of programs. Formally verified compilers guarantee the absence of correctness bugs, but do not protect against other classes of bugs, such as security bugs. This limitation partly arises from the traditional form of stating compiler correctness as preservation of semantics that do not capture non-functional properties such as security. Moreover, proof techniques for compiler correctness, including the traditional notions of simulation, do not immediately apply to secure compilation, and need to be extended accordingly. This talk will address the challenges of secure compilation from the specific angle of turning an existing formally-verified compiler into a formally-verified secure compiler. Two case studies will illustrate this approach, where each case study addresses a notion of security and uses modular reasoning (first proving correctness then security) to show that compilation preserves security. Specifically, we consider the problem of secure compilation for CompCert, a formally-verified moderately optimizing compiler for C programs, programmed and verified using the Coq proof assistant. CompCert evolved significantly over the last 15 years, starting as an academic project and now being used in commercial settings. The first case study focuses on software fault isolation and considers a novel security-enhancing sandboxing transformation; it ensures that an untrusted module cannot escape its dedicated isolated address space. The second case study focuses on side-channel protection, and considers crypto-graphic constant-time, a popular software-based countermeasure against timing-based and cache-based attacks. Informally, an implementation is secure with respect to the cryptographic constant-time policy if its control flow and sequence of memory accesses do not depend on secrets.

Bio. Sandrine Blazy is a professor of computer science at the University of Rennes. Her research interests include semantics, theorem proving, static analysis, verified compilation and software security. She made several contributions to the CompCert formally verified C compiler (for which she received the LaRecherche team award in information sciences in 2011) and to the Verasco formally verified static analyzer. She is a member of the VESTA project funded by ERC from 2018 to 2023.

Jean Yang
(Akita Software, USA)

Abstract. It is easier than ever before to build complex web applications that handle sensitive user data. At same time, regulatory shifts have made data breaches more costly than ever before. While starting Akita, I discovered just how difficult it is for software teams to maintain an up-to-date picture of how sensitive data flows across complex applications. A major challenge is that modern web applications run across many heterogenous components, often communicating via remote procedure calls. Unfortunately, network calls subvert all known software analysis methods for the application layer—and using network tools alone do not yield the full picture. The result is that developers end up piecing the whole story together through reading code, logs, and documentation. At Akita, we observed that network-based application programming interfaces (APIs) are both a root cause of what we call the Software Heterogeneity Problem—and also the key to the solution. The proliferation of APIs for both internal and external use, withthe rise of service-oriented architectures and the growth of the API economy, have made it easy to quickly build applications that are amalgams of cross-service network calls. At the same time, there is consolidation around a handful of interface definition languages for web APIs. This makes it possible for us to address the Software Heterogeneity problem by applying programming languages techniques at the API layer. In this talk, I will introduce the Software Heterogeneity Problem and its consequences, demonstrate one way to tackle it at the API layer, and outline API-level security problems I believe we can solve as a community.

Bio. Jean Yang is the founder and CEO of Akita Software, a developer tools company. Jean received her PhD at MIT in 2015 and was an Assistant Professor in the Computer Science Department at Carnegie Mellon University 2016-2018. Together with her collaborators, Jean won Best Paper Award at PLDI 2020 for the paper “Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System” and a Distinguished Paper Award at ICFP 2020 for the paper “Liquid Information Flow Control.”

The Workshop

PLAS provides a forum for exploring and evaluating the use of programming language and program analysis techniques for promoting security in the complete range of software systems, from compilers to machine-learned models and smart contracts. The workshop encourages proposals of new, speculative ideas, evaluations of new or known techniques in practical settings, and discussions of emerging threats and problems. We also host position papers that are radical, forward-looking, and lead to lively and insightful discussions influential to the future research at the intersection of programming languages and security.

The scope of PLAS includes, but is not limited to:

*NEW THIS YEAR*: Language-based techniques for detecting and eliminating side-channel vulnerabilities
Programming language techniques and verification applied to security in other domains (e.g. adversarial learning and smart contracts)
Software isolation techniques (e.g., SFI and sandboxing) and compiler-based hardening techniques (e.g, secure compilation).
Compiler-based security mechanisms (e.g. security type systems) or runtime-based security mechanisms (e.g. inline reference monitors)
Techniques for discovering and detecting security vulnerabilities, including program (binary) analysis and fuzzing
Automated introduction and/or verification of security enforcement mechanisms
Language-based verification of security properties in software, including verification of cryptographic protocols
Specifying and enforcing security policies for information flow and access control
Model-driven approaches to security
Security concerns for Web programming languages
Language design for security in new domains such as cloud computing and IoT
Applications, case studies, and implementations of these techniques

Registration

Registration for PLAS is included in the registration for CCS (website):

Early registration: $35 until October 30 (AoE)
Late registration: $50 until November 6 (AoE)

Note: No registration is possible after November 6.

Call for Papers

We invite both full papers and short papers. For short papers we especially encourage the submission of position papers that are likely to generate lively discussion as well as short papers covering ongoing and future work. Full and short paper presentations will have equal time slots.

Full papers should be at most 11 pages long, plus as many pages as needed for references and appendices. Papers in this category are expected to have relatively mature content.
Short papers should be at most 3 pages long, plus as many pages as needed for references. Papers that present radical, open-ended and forward-looking ideas are particularly welcome in this category, as are papers presenting preliminary and exploratory work. Authors submitting papers in this category must prepend the phrase "Short Paper:" to the title of the submitted paper.

Submissions should be PDF documents typeset in the double-column ACM format using 10pt fonts. In particular, we recommend using the sigconf template, which can be downloaded from https://www.acm.org/publications/proceedings-template.

Both full and short papers must describe work not published in other refereed venues (see the SIGPLAN republication policy for more details). Accepted papers will appear in workshop proceedings, which will be distributed to the workshop participants and be available in the ACM Digital Library.

Submissions can be made via Easychair.

Important Dates

Paper submission: ~~Friday June 12, 2020 (AoE)~~ EXTENDED: Sunday June 28, 2020 (AoE)
Author notification: August 8, 2020
Camera ready version: Wednesday September 2, 2020
Workshop date: Friday November 13, 2020

Sponsorship Opportunities

PLAS is an academic workshop that brings together some of the brightest minds working on the intersection of programming languages and security. In previous years, PLAS was co-located with top programming languages conferences; this year, PLAS is co-located with a top security conference (ACM CCS 2020). As such, we anticipate participants from top universities all over the world with broad interests in security and programming languages.

If you are looking to expose your company's brand, logo, and messages to the world's leading researchers on security and programming languages (and potential future employees), PLAS is a great place to start. Your support will allow us to offer travel grants and reduced registration fees to students and underrepresented groups.

We offer several support levels for your consideration. Please contact the chairs at plas2020@easychair.org for more information on how your organization can participate or with any questions and requests (e.g., if you would like a custom sponsorship level).