一句话:提出流敏感类型系统 MinIF,静态消除动态 IFC 的运行时检查与标签跟踪开销,并保持程序行为与执行决策不变。
动态信息流控制(IFC)在运行时用安全标签标记值,并通过终止系统来阻止违反机密性策略的输出;然而普遍的标签跟踪与检查带来高昂运行时开销,使 IFC 只能用于性能不敏感的场景。本文提出 MinIF:一种类型导向的程序变换,可为现有动态 IFC 系统静态消除开销。其核心是一个流敏感类型系统,能够追踪哪些敏感输入影响了某个值,并判断执行机制是否会接受对该值的操作——即便类型系统并不知道被执行的策略。基于该类型系统,MinIF 静态预测执行结果,删除冗余检查及其对应的标签跟踪代码,并证明优化后的程序保持原程序的行为与执行决策。对于具备 introspection 的 IFC 系统,程序中已有的 introspection 查询即可提供所需权限信息,因而优化完全自动、无需程序员标注。无法判定的检查会以警告形式暴露,而无警告则给开发者提供了“系统不会因执行机制而终止”的静态保证。作者在 WebTTC 动态 IFC 平台上的 Python 程序上进行评估:基准测试中 MinIF 消除了 13% 至 99% 的执行开销,原先在强制执行下超时的计算密集型负载现在可在毫秒级完成。
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.
@article{paperbot12142,
title = {A Type System for Optimizing Dynamic IFC},
author = {Daniel Galán Pascual and François Hublet and Srđan Krstić and Roman Fischer and Colin Pfingstl and David Basin},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839456}
}