一句话：提出基于单子效应语义的框架，为信息流控制中程序计数器标签建立语义基础与新非干涉证明技术。
信息流控制类型系统常用程序计数器（PC）标签跟踪敏感上下文，并防止带效应计算造成泄漏，但此前对 PC 标签的推理多为非形式化，安全证明也依赖特定技巧。本文基于效应的单子语义建立统一框架，为 PC 标签给出语义解释。由此得到三方面结果：提出一种新的非干涉性证明技术，非干涉性是带效应语言中信息流控制的核心安全定理；统一了状态、异常与非终止等不同效应的安全概念；形式化了“PC 标签是效应下界”的民间说法，并表明其虽非普遍成立，却具有良好语义基础。
Type systems designed for information-flow control commonly use a program-counter label to track the sensitivity of the context and rule out data leakage arising from effectful computation in a sensitive context. Currently, type-system designers reason about this label informally except in security proofs, where they use ad-hoc techniques. We develop a framework based on monadic semantics for effects to give semantics to program-counter labels. This framework leads to three results about program-counter labels. First, we develop a new proof technique for noninterference, the core security theorem for information-flow control in effectful languages. Second, we unify notions of security for different types of effects, including state, exceptions, and nontermination. Finally, we formalize the folklore that program-counter labels are a lower bound on effects. We show that, while not universally true, this folklore has a good semantic foundation.
@article{paperbot1171,
title = {Giving semantics to program-counter labels via secure effects},
author = {Andrew K. Hirsch and Ethan Cecchetti},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434316}
}