A Type System for Optimizing Dynamic IFC
This program is tentative and subject to change.
Dynamic information-flow control (IFC) enforces confidentiality policies at runtime by tagging values with security labels and blocking policy-violating outputs by terminating the running system. Pervasive label tracking and enforcement checks incur high runtime costs, which limits practical IFC deployment to performance-insensitive workloads. We present a novel alternative called MinIF, a type-directed program transformation that statically eliminates the overhead of dynamic IFC for existing systems.
The central contribution of MinIF is a flow-sensitive type system that tracks which sensitive inputs influence a value and whether the enforcement mechanism would accept operations on it, even though the enforced policy is unknown to the type system. Using the type system, MinIF statically predicts enforcement outcomes and removes redundant checks along with the label-tracking code that served them, and we prove that the optimized program preserves both the behavior and the enforcement decisions of the original. For IFC systems with introspection, the optimization is fully automatic, as the introspection queries already present in the program supply all the permission information MinIF needs, with no programmer annotations. Unresolved checks surface as warnings, and the absence of warnings gives developers a static guarantee against enforcement-induced system termination.
We evaluate MinIF on Python programs running on the WebTTC dynamic IFC platform. On benchmarks, MinIF eliminates between 13% and 99% of the enforcement overhead, and compute-intensive workloads that time out under enforcement now complete in milliseconds.
This program is tentative and subject to change.
Wed 7 OctDisplayed time zone: Pacific Time (US & Canada) change
13:30 - 15:00 | Security and Information FlowOOPSLA at Junior Ballroom 1&2 Chair(s): Mae Milano Princeton University | ||
13:30 18mTalk | (Dis)Proving Spectre Security with Speculation-Passing Style OOPSLA Santiago Arranz Olmos MPI-SP, Gilles Barthe MPI-SP; IMDEA Software Institute, Lionel Blatter MPI-SP, Xingyu Xie MPI-SP, Zhiyuan Zhang MPI-SP DOI | ||
13:48 18mTalk | Decompiling for Constant-Time Analysis OOPSLA Santiago Arranz Olmos MPI-SP, Gilles Barthe MPI-SP; IMDEA Software Institute, Lionel Blatter MPI-SP, Youcef Bouzid ENS Paris-Saclay, Sören van der Wall TU Braunschweig, Zhiyuan Zhang MPI-SP DOI | ||
14:06 18mTalk | Sound Enforcement of Dynamic Release Information Flow Policy OOPSLA DOI Pre-print | ||
14:24 18mTalk | A Type System for Optimizing Dynamic IFC OOPSLA Daniel Galán Pascual ETH Zurich, François Hublet ETH Zurich, Srđan Krstić ETH Zurich, Roman Fischer ETH Zurich, Colin Pfingstl ETH Zurich, David Basin ETH Zurich DOI | ||