论文标题
通过安全效果将语义给节目符号标签
Giving Semantics to Program-Counter Labels via Secure Effects
论文作者
论文摘要
设计用于信息流控制的类型系统通常使用程序表演标签来跟踪上下文的敏感性，并排除在敏感上下文中有效计算引起的数据泄漏。当前，类型系统设计师的理由是非正式的，除了在安全证明中使用临时技术。我们开发了一个基于Monadic语义的框架，以使效果为程序表标签提供语义。该框架导致有关计划场标签的三个结果。首先，我们开发了一种用于非干扰的新证明技术，即有效语言中信息流控制的核心安全定理。其次，我们将安全性概念统一，包括州，异常和非终止。最后，我们正式化了节目竞赛标签是对效果的下限。我们表明，虽然不是普遍真实的，但这个民间传说是一个良好的语义基础。
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.
