Giving Semantics to Program-Counter Labels via Secure Effects
This work addresses foundational issues in secure programming language design, providing formal semantics for program-counter labels to improve security proofs and unify effect handling, though it is incremental in building on existing monadic and type system theories.
The paper tackles the problem of informal reasoning about program-counter labels in information-flow control type systems by developing a monadic semantics framework, which leads to a new proof technique for noninterference, unifies security notions across effects, and formalizes the folklore about program-counter labels as lower bounds on effects.
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.