Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus

TL;DR

This paper establishes noninterference for sealing calculus through a fully complete translation to simply typed lambda-calculus, correcting prior errors and clarifying relationships among related calculi.

Contribution

It introduces a fully complete translation to simply typed lambda-calculus for sealing calculus, enabling a correct proof of noninterference and clarifying calculus relationships.

Findings

Corrected noninterference proof for sealing calculus

Established equivalence among sealing calculus, DCC, and extended DCC

Demonstrated importance of full completeness in logical relation preservation

Abstract

Tse and Zdancewic have formalized the notion of noninterference for Abadi et al.'s DCC in terms of logical relations and given a proof of noninterference by reduction to parametricity of System F. Unfortunately, their proof contains errors in a key lemma that their translation from DCC to System F preserves the logical relations defined for both calculi. In fact, we have found a counterexample for it. In this article, instead of DCC, we prove noninterference for sealing calculus, a new variant of DCC, by reduction to the basic lemma of a logical relation for the simply typed lambda-calculus, using a fully complete translation to the simply typed lambda-calculus. Full completeness plays an important role in showing preservation of the two logical relations through the translation. Also, we investigate relationship among sealing calculus, DCC, and an extension of DCC by Tse and Zdancewic and show that the first and the last of the three are equivalent.