Discretionary Information Flow Control for Interaction-Oriented Specifications

Abstract

This paper presents an approach to specify and check discretionary information flow properties of concurrent systems. The approach is inspired by the success of the interaction-oriented paradigm to concurrent systems (cf. choreographies, behavioural types, protocols,...) in providing behavioural guarantees of global properties such as deadlock-absence. We show how some information flow properties are easier to formalise and check on a global interaction-oriented description of a concurrent system rather than on a local process-oriented description of the components of the system. We use a simple choreography description language adapted from the literature of choreographies and session types. We provide a generic method to instrument the semantics with information flow annotations. Policies are used to specify the admissible flows of information. The main contribution of the paper is a sound type system for statically checking if a system specification ensures an information flow policy. The approach is illustrated with two archetypal examples of distributed and parallel computing systems: a protocol for an identity-secured data providing service and a parallel MapReduce computation.

A Graphs with Interfaces

We recall and adapt a few definitions concerning graphs, and their extension with interfaces, referring to [6, 11, 15] for a more detailed presentation.

Definition 10

(graphs). A is a four-tuple $\langle V, E, s, t \rangle$ where V is the set of nodes, E is the set of edges and $s, t : E \rightarrow V$ are the source and target functions. A graph morphism is a pair of functions $\langle f_V, f_E \rangle$ preserving the source and target functions, i.e. $f_V \circ s = s \circ f_E$ and $f_V \circ t = t \circ f_E$.

Definition 11

(graphs with interfaces). A graph with interfaces is a span of graph morphisms $I \xrightarrow {_{i}} G \xleftarrow {_{o}} O$, where G is a body graph, I and O are the input and output graph interfaces, and $i: I \rightarrow G$, $o: O \rightarrow G$ are the input and output graph morphisms. An interface graph morphism $f:\mathbb {G} \Rightarrow \mathbb {H}$ is a triple of graph morphisms $\langle f_I, f, f_O \rangle$, preserving the input and output morphisms.

With an abuse of notation, we sometimes refer to the image of the input and output morphisms as inputs and outputs, respectively, and we use the term graph to refer to abbreviate graphs with interfaces. We restrict our attention to graphs with discrete interfaces, i.e., such that their set of edges is empty.

The following definitions define the sequential and parallel composition of graphs with interfaces, whose informal description can be found in Sect. 4.

Definition 12

(sequential composition of graphs). Let $\mathbb {G}=I \xrightarrow {_{i}} G \xleftarrow {_{j}} J$ and $\mathbb {G'}=J \xrightarrow {_{j'}} G' \xleftarrow {_{o}} O$ be graphs with interfaces. Then, their sequential composition is the graph  $\mathbb {G} \circ \mathbb {G'}= I \xrightarrow {_{i'}} G'' \xleftarrow {_{o'}} O$, for $G''$ the disjoint union $G \uplus G'$, modulo the equivalence on nodes induced by $j(x) = j'(x)$ for all $x \in N_{J}$, and $i', o'$ the uniquely induced arrows.

Definition 13

(parallel composition of graphs). Let $\mathbb {G} = I \xrightarrow {_{i}} G \xleftarrow {_{o}} O$ and $\mathbb {H} = I' \xrightarrow {_{i'}} H \xleftarrow {_{o'}} O'$ be two graphs with interfaces. Then, their parallel composition is the gwdi $\mathbb {G} \otimes \mathbb {H}= (I \cup I')\xrightarrow {_{i''}} G' \xleftarrow {_{o''}} (O \cup O')$, for $G'$ the disjoint union $G \uplus H$, modulo the equivalence on nodes induced by $o(y) = o'(y)$ for all $y \in N_{O} \cap N_{O'}$ and $i(y) = i'(y)$ for all $y \in N_{I} \cap N_{I'}$, and $i'', o''$ the uniquely induced arrows.

With an abuse of notation, the set-theoretic operators are defined component-wise. The operations are concretely defined, modulo the choice of canonical representatives for the set-theoretic operations: the result is independent of such a choice, up-to isomorphism of the body graphs.

A graph expression is a term over the syntax containing all graphs with discrete interfaces as constants, and parallel and sequential composition as binary operators. An expression is well-formed if all occurrences of those operators are defined for the interfaces of their arguments, according to Definitions 12 and 13; its interfaces are computed inductively from the interfaces of the graphs occurring in it, and its value is the graph obtained by evaluating all operators in it. For the axiomatic properties of the operations (e.g. associativity, identity of $\circ$, associativity, commutativity and identity of $\otimes$) we refer to [6, 11].