ACM SIGSAC 15th 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
Session Chair
10:00 - 10:10
Opening Remarks
    10:10 - 11:10
    Invited Talk 1 From Verified Compilation to Secure Compilation: a Semantic Approach
    Sandrine Blazy (University of Rennes, France)
    Marco Vassena
    11:10 - 11:25
    Virtual Coffee Break
      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
      12:15 - 13:15
      Lunch / Dinner Break
        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
        14:05 - 14:20
        Virtual Coffee Break
          14:20 - 15:20
          Invited Talk 2 How APIs Are Both the Illness and the Cure
          Jean Yang (Akita Software, USA)
          Alley Stoughton
          15:20 - 15:35
          Virtual Coffee Break
            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
            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).

              Sponsorship Levels

              Bronze - $1,000 (USD)
              • Institution logo displayed on the workshop website
              • Links to sponsor website
              • Acknowledgment in the Chairs' statement for the proceedings
              Silver - $2,500 USD (USD)
              • Institution logo displayed on the workshop website
              • Links to sponsor website
              • Acknowledgment in the Chairs' statement for the proceedings
              • Shared table with supporter's materials available to attendees
              Gold - $5,000 USD (USD)
              • Institution logo displayed on the workshop website
              • Links to sponsor website
              • Acknowledgment in the Chairs' statement for the proceedings
              • Tabletop exhibit space at the workshop, if requested

              Program Committee


              Amal Ahmed

              (Northeastern University)

              Owen Arden

              (University of California, Santa Cruz)

              Musard Balliu

              (KTH Royal Institute of Technology)

              Ethan Cecchetti

              (Cornell University)

              Dominique Devriese

              (Vrije Universiteit Brussel)

              François Dupressoir

              (University of Bristol)

              Anitha Gollamudi

              (Harvard University)

              Marco Guarnieri

              (IMDEA Software)

              Scott Moore

              (Galois)

              Deian Stefan

              (University of California, San Diego)

              Alley Stoughton

              (Boston University, Co-Chair)

              Marco Vassena

              (CISPA, Co-Chair)

              Previous Meetings

              PLAS 2019, London, UK
              PLAS 2018, Toronto, CA
              PLAS 2017, Dallas, TX, USA
              PLAS 2016, Vienna, Austria
              PLAS 2015, Prague, Czech Republic
              PLAS 2014, Uppsala, Sweden
              PLAS 2013, Seattle, Washington
              PLAS 2012, Beijing, China
              PLAS 2011, San Jose, California
              PLAS 2010, Toronto, Canada
              PLAS 2009, Dublin, Ireland
              PLAS 2008, Tucson, Arizona
              PLAS 2007, San Diego, California
              PLAS 2006, Ottawa, Canada

              Contact us at plas2020@easychair.org