Software sandboxing or software-based fault isolation (SFI) is a lightweight approach to building secure systems out of untrusted components. The idea of SFI is old. Its use in production, to sandbox third-party libraries in Firefox, is new. We describe the PL techniques—notably static information flow control—that were key to deploying SFI in practice and their use in tackling software security more generally.
Sensitivity properties study how the output of a program changes when we make small changes to its input. How can we reason about sensitivity of programs that have probabilistic behavior?
A brief farewell from Mike Hicks, outgoing co-editor at PL Perspectives, and a brief hello by Adrian Sampson, co-editor incoming!
How can types and formal reasoning tools improve the lives of people who write software? This is the focus of the HATRA (Human Aspects of Types and Reasoning Assistants) workshop. At the 2020 meeting, we discussed exciting opportunities for these key PL techniques to make developers more effective.
