On Graded Coeffect Types for Information-Flow Control

Graded types are an overarching paradigm that provides fine-grained reasoning by reflecting the structure of typing rules into a system of type annotations. A significant subset of graded type systems is that of coeffect systems, originally introduced by Petricek, Orchard, and Mycroft as a dual to effect systems, capturing the dataflow of values in a calculus by annotating variables and function types with elements of a semiring. A particularly useful instance of these graded coeffect systems is to capture security properties of data to enforce information-flow control. We examine this particular use case and give a new characterisation of a subclass of semirings which enable the key non-interference theorem of information-flow control: that less privileged observers are unable to distinguish the dependence of computations on more privileged inputs. The result relies on a logical relations proof and is mechanised in Agda. We consider its relationship to other characterisations of non-interference in the recent literature on graded types and in the historical context of coeffect and graded systems. We leverage these results for programming with security in the Granule programming language, a research language for graded types. We conclude with extensions to Granule that go beyond non-interference to declassification, leveraging graded types to control deliberate information leakage.