Mechanized Noninterference for Gradual Security

TL;DR

This paper provides the first machine-checked proof of noninterference for a language with gradual information-flow control, establishing a secure foundation for flexible enforcement of security policies.

Contribution

It introduces the first traditional semantics for the language $$ and mechanizes proofs of noninterference, type safety, and type preservation during compilation.

Findings

Uncovered a flaw in existing noninterference proofs in literature.

Provided a counterexample for a key lemma in prior proofs.

Validated the soundness of gradual security enforcement mechanisms.

Abstract

This paper presents the first machine-checked proof of noninterference for a language with gradual information-flow control, thereby establishing a rock solid foundation for secure programming languages that give programmers the choice between runtime versus compile-time enforcement. Along the way we uncovered a flaw in one of the noninterference proofs in the literature, and give a counterexample for one of the main lemmas. The particular language studied in this paper, $\lambda_{\mathtt{SEC}}^\star$, is based on the GLIO language of Azevedo de Amorim et al. [2020]. To make the design more accessible to other researchers, this paper contributes the first traditional semantics for the language, that is, we define compilation from $\lambda_{\mathtt{SEC}}^\star$ to a cast calculus and design a reduction semantics for the latter that includes blame tracking. In addition to the proof of noninterference, we also mechanize proofs of type safety, determinism, and that compilation preserves types.