Substructural Information Flow via Polymorphism
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.
Substructural Information Flow via Polymorphism (main.pdf) | 201KiB |
Mon 21 OctDisplayed time zone: Pacific Time (US & Canada) change
11:00 - 12:30 | |||
11:00 30mTalk | Capabilities, Effects, Ownership, and Behaviors IWACO Colin Gordon Drexel University | ||
11:30 30mTalk | Modular Borrowing Without Ownership or Linear Types IWACO Lionel Parreaux HKUST (The Hong Kong University of Science and Technology) Media Attached File Attached | ||
12:00 30mTalk | Substructural Information Flow via Polymorphism IWACO Hemant Gouni Carnegie Mellon University, Pittsburgh, Pennsylvania, United States, Jonathan Aldrich Carnegie Mellon University Media Attached File Attached |