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.
翻译：用于信息流通控制的类型系统通常使用程序对帐标签来跟踪上下文的敏感度,并排除在敏感情况下有效计算产生的数据泄漏。 目前, 类型系统设计者非正式地解释这一标签的原因, 除了安全证明之外, 他们使用特殊技术。 我们开发了一个基于修道语语的语义框架, 以效果为程序对帐标签提供语义。 这个框架导致关于程序对帐标签的三种结果。 首先, 我们开发一种新的不干预证明技术, 即有效语言信息流通控制的核心安全标语。 其次, 我们统一了不同类型效果的安全概念, 包括国家、 例外和不消灭。 最后, 我们正式确定了程序对账标签的民俗, 即程序对效果的约束较低。 我们显示, 虽然并非普遍如此, 但民俗有一个良好的语义基础 。
相关内容
微信扫码咨询专知VIP会员