Sheaf semantics of termination-insensitive noninterference

TL;DR

This paper introduces a sheaf semantics framework for secure information flow that inherently guarantees termination-insensitive noninterference, using synthetic domain theory and topos-theoretic concepts, offering an intrinsic alternative to traditional models.

Contribution

It develops a novel sheaf semantics based on synthetic domain theory for secure information flow, ensuring termination-insensitive noninterference intrinsically, and applies phase distinctions in a new way.

Findings

Semantics automatically satisfies termination-insensitive noninterference

Reconstruction of security syntax using phase distinctions

Verification of semantic adequacy with an extended dependency core calculus

Abstract

We propose a new sheaf semantics for secure information flow over a space of abstract behaviors, based on synthetic domain theory: security classes are open/closed partitions, types are sheaves, and redaction of sensitive information corresponds to restricting a sheaf to a closed subspace. Our security-aware computational model satisfies termination-insensitive noninterference automatically, and therefore constitutes an intrinsic alternative to state of the art extrinsic/relational models of noninterference. Our semantics is the latest application of Sterling and Harper's recent re-interpretation of phase distinctions and noninterference in programming languages in terms of Artin gluing and topos-theoretic open/closed modalities. Prior applications include parametricity for ML modules, the proof of normalization for cubical type theory by Sterling and Angiuli, and the cost-aware logical framework of Niu et al. In this paper we employ the phase distinction perspective twice: first to reconstruct the syntax and semantics of secure information flow as a lattice of phase distinctions between "higher" and "lower" security, and second to verify the computational adequacy of our sheaf semantics vis-\`a-vis an extension of Abadi et al.'s dependency core calculus with a construct for declassifying termination channels.