Graded Modal Types for Integrity and Confidentiality

Graded type systems, such as the one underlying the Granule programming language, allow various different properties of a program's behaviour to be tracked via annotating types with additional information, which we call grades. One example of such a property, often used as a case study in prior work on graded types, is information flow control, in which types are graded by a lattice of security levels allowing noninterference properties to be automatically verified and enforced. These typically focus on one particular aspect of security, however, known as confidentiality; public outputs are prohibited from depending on private inputs. Integrity, a property specifying that trusted outputs must not depend on untrusted inputs, has not been examined in this context. This short paper aims to remedy this omission. It is well-known that confidentiality and integrity are in some sense dual properties, but simply reversing the ordering of the security lattice turns out to be unsatisfactory for the purpose of combining both kinds of property in a single system, at least in our setting. We analogize the situation to recent work on embedding both linear and uniqueness types in a graded framework, and use this framing to demonstrate that we can enforce both integrity and confidentiality alongside one another. The main idea is to add an additional flavour of modality annotated for integrity, such that the existing graded comonad for tracking confidentiality now also acts as a relative monad over the new modality, with rules allowing information to flow from trusted to public to private.