The 19^th Workshop on Programming Languages and Analysis for Security (PLAS 2024)

October 14th, 2024 - Salt Lake City, U.S.A.
Co-located with ACM CCS 2024

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. It 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:

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

Tentative Program

Time	Event
8:50 AM - 9:00 AM	Opening remarks
Keynote talk
9:00 AM - 10:00 AM	A Step Toward Trustworthy Binary Verification. Binoy Ravindran (Virginia Tech)
10:00 AM - 10:30 AM	Coffee Break
10:30 AM - 12:00 AM	Paper Presentations
10:30 AM - 10:50 AM	Information Flow above Optimising Compilers With Weak Memory. (short) Jay Richards, Vineet Rajani, Mark Batty (University of Kent)
10:50 AM - 11:10 AM	Towards relating hyper- and epistemic-temporal logics. (short) Matvey Soloviev (Chalmers University); Vineet Rajani (University of Kent); Musard Balliu (KTH)
11:10 AM - 11:30 AM	Focusing on Testing Efficiency in Hardware-based C/C++ Memory Safety. (short) Konrad Hohentanner (Fraunhofer AISEC)
11:30 AM - 12:00 AM	An Information Flow Calculus for Non-Interference. Clément Aubert, Neea Rusch (Augusta University)
12:00 PM - 1:30 PM	Lunch Break
1:30 PM - 3:30 PM	Paper Presentations
1:30 PM - 2:00 PM	On Separation Logic, Computational Independence, and Pseudorandomness. Ugo Dal Lago (University of Bologna, Inria); Davide Davoli (Université Côte d’Azur, Inria); Bruce M. Kapron (University of Victoria)
2:00 PM - 2:30 PM	Is This the Same Code? A Comprehensive Study of Decompilation Techniques for WebAssembly Binaries. Wei-Cheng Wu (Dartmouth College); Yutian Yan, Hallgrimur David Egilsson, David Park, Steven Chan (University of Southern California); Christophe Hauser (Dartmouth College); Weihang Wang (University of Southern California)
2:30 PM - 3:00 PM	Robust Stack Smashing Protection for WebAssembly. Quentin Michaud (Thales Group / Télécom SudParis - Institut Polytechnique de Paris); Yohan Pipereau, Olivier Levillain (Télécom SudParis - Institut Polytechnique de Paris); Dhouha Ayed (Thales Group)
3:00 PM - 3:30 PM	Formalizing Discovery of Weird States and Weird Machine Primitives Using Program Semantics. Ramesh Balaji (Rutgers University, New Brunswick); Meera Sridhar (University of North Carolina at Charlotte); Matthew Revelle (Montana State University)
3:30 PM - 4:00 PM	Coffee Break
Keynote talk
4:00 PM - 5:00 PM	Quantitative information flow reasoning for differential privacy. Natasha Fernandes, (Macquarie University)
5:00 PM - 5:10 PM	Closing remarks

Invited Speaker

Natasha Fernandes
(Macquarie University)

Quantitative information flow reasoning for differential privacy

Abstract. Quantitative information flow (QIF) is an information-theoretic framework for analysing information leaks from secure systems. In its current form, QIF derives from the g-leakage framework proposed by Geoffrey Smith (FOSSACS, 2009) and has developed into a powerful mathematical toolkit for the analysis of probabilistic systems.
Differential privacy (DP) is the currently-accepted standard for privacy protection in the academic community, and has been adopted by industry giants such as Apple and Google. Despite intense research interest, there remain questions surrounding DP’s interpretability and how to manage the the fine-tuning of privacy so as to maximise utility, commonly called the "privacy-utility trade-off".
In this talk I will discuss some recent work on how QIF has helped to shed light on these questions, and present some interesting challenges which remain to be addressed.

Binoy Ravindran
(Virginia Tech)

A Step Toward Trustworthy Binary Verification

Abstract. Many production software systems are available only in binary form. This is due to several reasons including intellectual property and proprietary issues, outdated and decaying build processes and environments, and third-party libraries and tools that are no longer available or backwards compatible. Security vulnerability analysis of such software is still a necessary task due to the need to rapidly patch program errors, especially those that can be used to create security exploits, i.e., unintended, or malicious behaviors or leak sensitive data. A large body of work has focused on this problem space including disassembly, decompilation, and binary verification, among others. A common denominator of these approaches is binary lifting: raw unstructured data is lifted to a form for reasoning over behavior and semantics. Majority of existing binary lifting approaches are untrustworthy (e.g., misses jump targets, misidentifies code as data), which negatively affects the trust base of techniques that rely on them.
In this talk, I will present an approach for binary lifting that simultaneously disassembles, recovers control flow, and generates formal proofs on the correctness of the lifted representation and a class of sanity properties including return address integrity, bounded control flow, and calling convention adherence. Establishing these properties allows the binary to be lifted to a representation that contains an over-approximation of all possible execution paths of the binary. The lifted representation contains proof obligations that are sufficient to formally prove – by exporting to a theorem-prover – the sanity properties and correctness of the lifted representation, which removes the lifting algorithm and its implementation from the trust base. We apply this approach to Linux Foundation’s Xen Hypervisor covering about 400K instructions, providing evidence of its effectiveness and scalability for trustworthy binary lifting of off-the-shelf production software. I will argue that such a verified lifted representation not only reduces the trust base of downstream techniques (e.g., binary verification), but also exposes novel ways for reasoning about related problems (e.g., binary patching).

Call for Papers

We invite both short papers and long 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 papers: There is no page limit on long papers. Papers in this category are expected to have relatively mature content. Papers that present promising preliminary and exploratory work, or recently published work are particularly welcome in this category. Long papers may receive longer talk slots at the workshop than short papers, depending on the number of accepted submissions.
Short papers: should be at most 2 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. Authors submitting papers in this category must prepend the phrase "Short Paper:" to the title of the submitted paper.

The workshop has no published workshop proceedings and there is no restriction on paper format other than the page limits stated above. Presenting a paper (either short or long) at the workshop does not preclude submission to or publication in other venues that are before, concurrent, or after the workshop. Papers presented at the workshop will be made available to workshop participants only.

Submissions will be made (in PDF format) via the following HotCRP instance: https://hotcrp.software.imdea.org/plas24/.