English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Graded type systems, such as the one underlying the Granule programminglanguage, allow various different properties of a program's behaviour to betracked 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 ongraded types, is information flow control, in which types are graded by alattice of security levels allowing noninterference properties to beautomatically verified and enforced. These typically focus on one particularaspect of security, however, known as confidentiality; public outputs areprohibited from depending on private inputs. Integrity, a property specifyingthat trusted outputs must not depend on untrusted inputs, has not been examinedin this context.  This short paper aims to remedy this omission. It is well-known thatconfidentiality and integrity are in some sense dual properties, but simplyreversing the ordering of the security lattice turns out to be unsatisfactoryfor the purpose of combining both kinds of property in a single system, atleast in our setting. We analogize the situation to recent work on embeddingboth linear and uniqueness types in a graded framework, and use this framing todemonstrate that we can enforce both integrity and confidentiality alongsideone another. The main idea is to add an additional flavour of modalityannotated for integrity, such that the existing graded comonad for trackingconfidentiality now also acts as a relative monad over the new modality, withrules allowing information to flow from trusted to public to private.

Graded Modal Types for Integrity and Confidentiality