Substructural Information Flow via Polymorphism (Video, IWACO 2024)
Hemant Gouni, and Jonathan Aldrich
(Carnegie Mellon University, Pittsburgh, Pennsylvania, United States; Carnegie Mellon University)
Abstract: Information flow control (IFC) is a long-studied approach for establishing non-interference properties of programs. For instance, IFC can be used to prove that a secret does not interfere with some computation, thereby establishing that it does not leak. Lattices are the dominant mechanism for enforcing information flow properties, with program data being organized into a lattice whose partial order determines safe flows. We discuss an alternative formulation of IFC based on parametric polymorphism which, in addition to usability benefits, highlights the structural properties lurking in all prior information flow systems. We show that relaxing these structural properties allows us to speak about sandboxing, resource exhaustion, quantitative information flow, capabilities, context-sensitive typestate, and much more using simple, intuitive types.
Presentation at the IWACO 2024 conference, October 20, 2024, https://2024.splashcon.org/home/iwaco-2024
Sponsored by ACM SIGPLAN,