一句话：提出结构化信息流类型系统，基于混合逻辑自然地支持解分类，并通过逻辑关系证明非干扰性。
信息流控制是建立程序非干扰性质长期研究的方法，但信息流类型系统虽成熟却采用有限，规范复杂且易失控；同时实际程序常需违背非干扰以完成功能，解分类（declassification）常削弱模块化推理。本文提出结构化信息流（structural information flow），从逻辑视角出发，借鉴模态逻辑文献，论证信息流推理源于混合逻辑（hybrid logic）而非传统模态逻辑。通过一系列例子展示结构化信息流规范易于编写和直观解析。特别地，解分类并非非干扰的异常，而是足够通用的信息流机制的自然且不可避免的结果，具有优秀的局部推理能力，能在不牺牲理论优雅性的前提下满足现实信息流需求。最后通过逻辑关系方法建立非干扰性，展示了其简洁性与表达力。
Information flow control is a long-studied approach for establishing non-interference properties of programs. For instance, it can be used to prove that a secret does not interfere with some computation, thereby establishing that the former does not leak through the latter. Despite their potential as a holy grail for security reasoning and their maturity within the literature, information flow type systems have seen limited adoption. In practice, information flow specifications tend to be excessively complex and can easily spiral out of control even for simple programs. Additionally, while non-interference is well-behaved in an idealized setting where information leakage never occurs, most practical programs must violate non-interference in order to fulfill their purpose. Useful information flow type systems in prior work must therefore contend with a definition of non-interference extended with declassification, which often offers weaker modular reasoning properties. We introduce structural information flow, which both illuminates and addresses these issues from a logical viewpoint. In particular, we draw on established insights from the modal logic literature to argue that information flow reasoning arises from hybrid logic, rather than conventional modal logic as previously imagined. We show with a range of examples that structural information flow specifications are straightforward to write and easy to visually parse. Uniquely in the structural setting, we demonstrate that declassification emerges not as an aberration to non-interference, but as a natural and unavoidable consequence of sufficiently general machinery for information flow. This flavor of declassification features excellent local reasoning and enables our approach to account for real-world information flow needs without compromising its theoretical elegance. Finally, we establish non-interference via a logical relations approach, showing off its simplicity in the face of the expressive power captured.
@article{paperbot2932,
title = {Structural Information Flow: A Fresh Look at Types for Non-interference},
author = {Hemant Gouni and Frank Pfenning and Jonathan Aldrich},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3764116}
}