一句话：证明细粒度与粗粒度动态信息流控制表达能力等价，并给出语义保持的双向翻译。
本文研究动态信息流控制（IFC）中长期未决的表达能力问题：粗粒度动态 IFC 是否弱于细粒度动态 IFC。作者分别定义两种主流语言，一种采用细粒度动态 IFC，另一种采用粗粒度动态 IFC，并机器化其语义，构造两个方向上的语义保持翻译。借助已验证的翻译，他们从一种语言的非干涉性推导出另一种语言的非干涉性。结果表明确细粒度与粗粒度动态 IFC 系统表达能力相同：粗到细翻译可减轻细粒度系统强加的标签标注负担，细到粗翻译说明粗粒度系统也能像细粒度系统一样精确跟踪信息，并可用于自动改造遗留应用以运行在现有粗粒度系统上。
We show that fine-grained and coarse-grained dynamic information-flow control (IFC) systems are equally expressive. To this end, we mechanize two mostly standard languages, one with a fine-grained dynamic IFC system and the other with a coarse-grained dynamic IFC system, and prove a semantics-preserving translation from each language to the other. In addition, we derive the standard security property of non-interference of each language from that of the other, via our verified translation. This result addresses a longstanding open problem in IFC: whether coarse-grained dynamic IFC techniques are less expressive than fine-grained dynamic IFC techniques (they are not!). The translations also stand to have important implications on the usability of IFC approaches. The coarse- to fine-grained direction can be used to remove the label annotation burden that fine-grained systems impose on developers, while the fine- to coarse-grained translation shows that coarse-grained systems---which are easier to design and implement---can track information as precisely as fine-grained systems and provides an algorithm for automatically retrofitting legacy applications to run on existing coarse-grained systems.
@article{paperbot692,
title = {From fine- to coarse-grained dynamic information flow control and back},
author = {Marco Vassena and Alejandro Russo and Deepak Garg and Vineet Rajani and Deian Stefan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290389}
}