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.

翻译：分级类型系统（如Granule编程语言所采用的）通过为类型添加额外信息（称为分级）来追踪程序行为的多种不同属性。这类属性中的一个典型例子是信息流控制——在先前关于分级类型的研究中常被用作案例——其通过安全等级格对类型进行分级，从而自动验证和执行非干扰属性。然而这些研究通常仅关注安全的一个特定方面，即机密性：禁止公开输出依赖私有输入。而完整性——确保可信输出不得依赖不可信输入的属性——尚未在此背景下得到考察。本短文旨在弥补这一缺漏。众所周知，机密性与完整性在某种意义上是相互对偶的属性，但仅仅反转安全等级格的顺序对于在单一系统中结合这两种属性而言并不理想（至少在我们的设定中如此）。我们将此情形类比于近期在线性类型和唯一类型嵌入分级框架方面的研究，并利用这一框架证明我们可以同时实施完整性与机密性。核心思想是增加一个标注了完整性的模态变体，使得现有的用于追踪机密性的分级伴子现在也作为相对单子作用于该新模态之上，并设置允许信息从可信流向公开再流向私有的规则。