Abstracts.2019.IFC

Modalities, Cohesion and Information Flow

by Carlos Tomé Cortiñas

Abstract

In this talk I will present the paper by Alex Kavvos: Modalities, cohesion and information flow. This paper develops a categorical model for information flow control and uses it to show classical non-interference properties of several calculi. In this presentation I will cover sections 1 to 4 (Introduction, Classified Sets, Cohesion, Non-Interference 1: Monads and Comonads) and (possibly) more.

Notes

Let ℒ be a set whose elements are called security levels to be understood as security clearance. Note that ℒ need not be a lattice, not even ordered.

• A classified set 𝒮 over ℒ is a set S together with a family (R_ℓ)_{ℓ ∈ ℒ} of reflexive relations R_ℓ for each security level ℓ ∈ ℒ (Definition 1)

  Note that the relations R_ℓ need not be equivalence relations.

  The relations R_ℓ are meant to model indistinguishability for observers at security level ℓ. It is intuitive that elements are indistinguishable to themselves, which corresponds to the reflexivity condition.

• A morphism of classified sets f : 𝒮 → 𝒮' is a function f : S → S' such that it preserves or respects the relations R_ℓ for each ℓ ∈ ℒ: If x R_ℓ y, then f(x) R'_ℓ f(y) for all x, y ∈ S (Definition 2)

  In other words, a function f : S → S' is a morphism of the classified sets 𝒮 and 𝒮' if and only if whenever f(x) and f(y) for some x,y ∈ S are distinguishable according to 𝒮' then x and y were distinguishable according to 𝒮.

These constitute a bicartesian closed category CSet (over ℒ): It has terminal objects, initial objects, binary products, binary coproducts, equalisers, coequalisers, and exponentials. (Propositions 1–7)

• U denotes the forgetful functor CSet → Set, 𝒮 ↦ S.

U(𝒮) has forgotten about the classification, only the underlying set S remains. There are a few ways 𝔹_public, 𝔹_secret,… : CSet to classify the set 𝔹 = N₂ = { 0, 1 } of Booleans and all of them get mapped to 𝔹 : Set by U.

The mapping from morphisms of classified sets 𝒮 → 𝒮' : CSet to functions U(𝒮) → U(𝒮') : Set, which can be seen as an inclusion of the subset

Hom_CSet(𝒮,𝒮') = { f : U(𝒮) → U(𝒮') | f respects the relations R_ℓ for each ℓ ∈ ℒ } ⊆ { f : U(𝒮) → U(𝒮') } = Hom_Set(U(𝒮),U(𝒮')),

is usually not surjective, that is usually the subset is proper, because for non-trivial classifications of sets with more than one element there are functions that do not respect it.

Consider, for instance, the security levels ℒ = { user, root }, then we might specify that the value of a "public" Boolean x ∈ 𝔹_public can be distinguished by observers with either security clearance but the value of a "secret" Boolean x ∈ 𝔹_secret can be distinguished only by observers with the root security clearance by defining the following two indistinguishability relations on the set of Booleans:

1. R^public_user = { (0,0), (1,1) } and R^public_root = { (0,0), (1,1) }

2. R^secret_user = { (0,0), (0,1), (1,0), (1,1) } and R^secret_root = { (0,0), (1,1) }

Then, an observer with the user security clearance cannot distinguish which of the two possible values 0 and 1 a "secret" Boolean has in the sense that any morphism of classified sets from 𝔹_secret to say 𝔹_public must be constant, in particular there is no morphism of classified sets isFalse? : 𝔹_secret → 𝔹_public because the function

isFalse? = λx. if x = 0 then 1 else 0

does not preserve the relation R^secret_user.

• Δ denotes the discrete functor Set → CSet, S ↦ (S,(R_ℓ)_{ℓ ∈ ℒ}), where each R_ℓ = { (s,s) | s ∈ S } is the diagonal or equality or discrete relation on S.

Δ(S) is the finest classification of the set S in the sense that Δ is left adjoint to U: There is a natural bijection between functions S → U𝒯 and morphisms of classified sets ΔS → 𝒯. (Proposition 8)

• ∇ denotes the codiscrete functor Set → CSet, S ↦ (S,(R_ℓ)_{ℓ ∈ ℒ}), where each R_ℓ = { (s,t) | s,t ∈ S } is the complete or codiscrete relation on S.

∇(S) is the most opaque classification of the set S in the sense that ∇ is right adjoint to U: There is a natural bijection between functions U𝒮 → T and morphisms of classified sets 𝒮 → ∇T. (Proposition 9)

Neither Δ nor ∇ touches the set of elements, they are both right inverses of U: U ∘ Δ = id_Set = U ∘ ∇. In particular, they are both faithful, and even full because the subsets

Hom_CSet(Δ(S),Δ(S')) ⊆ Hom_Set(U(Δ(S)),U(Δ(S'))) = Hom_Set(S,S') ⊆ Hom_CSet(Δ(S),Δ(S'))

Hom_CSet(∇(S),∇(S')) ⊆ Hom_Set(U(∇(S)),U(∇(S'))) = Hom_Set(S,S') ⊆ Hom_CSet(∇(S),∇(S'))

are the whole.

• C denotes the connected components functor CSet → Set, (S,(R_ℓ)_{ℓ ∈ ℒ}) ↦ S/R^*, where R = { (s,t) | s R_ℓ for some ℓ ∈ ℒ }, R^* the least equivalence relation containing R or the reflexive, symmetric and transitive closure of R, and S/R^* the quotient or the set of equivalence classes of S with respect to R^*.

If we think of morphisms into classified sets of the form Δ(T) for some set T as collapsing indistinguishable elements, then C(𝒮) is the least collapse of the classified set 𝒮 in the sense that C is left adjoint to Δ: There is a natural bijection between functions C𝒮 → T and morphisms of classified sets 𝒮 → ΔT. (Proposition 10)

The functors and adjunctions C ⊣ Δ, Δ ⊣ U, U ⊣ ∇ : CSet → Set can be generalised to the situation CSet_{ℒ ∪ ℒ'} → CSet_ℒ'. Note that Set is a degenerate category of classified sets in the sense that Set and CSet_∅ are trivially isomorphic categories. (Propositions 14–16)

CSet is an extensive category: The coproduct functor CSet/𝒜 × CSet/ℬ → CSet/(𝒜 + ℬ), (f,g) ↦ f + g is an equivalence of categories. (Proposition ?)

The situation is summarised on slides 37 and 54 of a presentation of the paper by Kavvos.

References

1. G. A. Kavvos. 2019. "Modalities, Cohesion, and Information Flow." arXiv preprint, MIT (Applied) Categories Seminar slides.
2. Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. 1999. "A Core Calculus of Dependency."
3. Eugenio Moggi. 1991. "Notions of computation and monads."