Categorical Information Flow

Abstract

We propose a categorical model for information flows of cor- related secrets in programs. We show how programs act as transformers of such correlations, and that they can be seen as natural transformations between probabilistic constructors. We also study some basic properties of the construction.

A Compositional sequential composition

The sequential composition (8) assumes that the mutable secrets of H and K are represented by the exact same variables ranging in $\mathcal{X}$. A slightly more general version of that result is to assume that H and K may share a hidden variable ranging in $\mathcal{X}$ and that they also have other hidden variables specific to each HMM. In this case, if H contains another hidden secret with type $\mathcal{X}_1$ then this secret must be considered as a collateral secret in K—thus K leaks collateral information about it, but does not update that secret. More precisely, we have the following lemma.

Lemma 4

Let with be two HMM matrices. We have

$$\begin{aligned}{}[\![H{;}K]\!]^\mathcal{Z}= [\![H]\!]^{\mathcal{X}_2\times \mathcal{Z}}{;}[\![K]\!]^{\mathcal{X}_1\times \mathcal{Z}}. \end{aligned}$$

(10)

where the composition H; K is given by Eq. (2) and the composition operator (; ) on the right takes the isomorphism between $\mathcal{X}_1\times \mathcal{X}_2$ and $\mathcal{X}_2\times \mathcal{X}_1$ into account.

Proof

Firstly, we have the following types

• $[\![H{;}K]\!]^\mathcal{Z}{{:}\,}{\mathbb D}(\mathcal{X}\times \mathcal{X}_1\times \mathcal{X}_2\times \mathcal{Z}){\rightarrow }{\mathbb D}^2(\mathcal{X}\times \mathcal{X}_1\times \mathcal{X}_2\times \mathcal{Z})$

• $[\![H]\!]^{\mathcal{X}_2\times \mathcal{Z}}{{:}\,}{\mathbb D}(\mathcal{X}\times \mathcal{X}_1\times \mathcal{X}_2\times \mathcal{Z}){\rightarrow }{\mathbb D}^2(\mathcal{X}\times \mathcal{X}_1\times \mathcal{X}_2\times \mathcal{Z})$

• $[\![K]\!]^{\mathcal{X}_1\times \mathcal{Z}}{{:}\,}{\mathbb D}(\mathcal{X}\times \mathcal{X}_2\times \mathcal{X}_1\times \mathcal{Z}){\rightarrow }{\mathbb D}^2(\mathcal{X}\times \mathcal{X}_2\times \mathcal{X}_1\times \mathcal{Z})$

Let us assume that we have applied the isomorphism that permutes the positions of the $\mathcal{X}_1$ and $\mathcal{X}_2$ in the domain of $[\![K]\!]^{\mathcal{X}_1\times \mathcal{Z}}$ so that the right hand side composition is well defined and is given by the sequential composition in the Giry monad [6]. This type matching function is implicitly embedded into the right hand side composition in (10).

Let $\varPi {{:}\,}{\mathbb D}(\mathcal{X}\times \mathcal{X}_1\times \mathcal{X}_2\times \mathcal{Z})$, Eqs. (1) and (2) give

$$\begin{aligned} (\varPi {\rangle }(H;K))_{y_1y_2,x''x_1'x_2'z} = \sum _{xx_1x_2}\varPi _{xx_1x_2z}\sum _{x'}H_{xx_1y_1x'x_1'}K_{x'x_2y_2x''x_2'} \end{aligned}$$

(11)

On the other hand, $[\![H]\!]^{\mathcal{X}_2\times \mathcal{Z}}{;}[\![K]\!]^{\mathcal{X}_1\times \mathcal{Z}} = \mathsf{avg}\circ {\mathbb D}[\![K]\!]^{\mathcal{X}_1\times \mathcal{Z}}\circ [\![H]\!]^{\mathcal{X}_2\times \mathcal{Z}}$ uses the Kleisli lifting. Let us consider an inner $\delta$ of $[\![H]\!]^{\mathcal{X}_2\times \mathcal{Z}}{;}[\![K]\!]^{\mathcal{X}_1\times \mathcal{Z}}.\varPi$. There exists an inner $\alpha$ of $[\![H]\!]^{\mathcal{X}_2\times \mathcal{Z}}.\varPi$ such that $\delta$ is an inner of $[\![K]\!]^{\mathcal{X}_1\times \mathcal{Z}}.\alpha$. That is, there exist two observations y and $y'$ such that

$$ \alpha _{x'x_1'x_2z}^{y_1} = \frac{\sum _{xx_1}\varPi _{xx_1x_2z}H_{xx_1y_1x'x'_1}}{\overline{\alpha }^{y_1}} $$

where $\overline{\alpha }^{y_1}= \sum _{x'x_1'x_2z}\left( \sum _{xx_1}\varPi _{xx_1x_2z}H_{xx_1y_1x'x'_1}\right)$, and

$$ \delta _{x''x'_1x'_2z}^{y_1y_2} = \frac{\sum _{x'x_2}\alpha _{x'x'_1x_2z}^{y_1}K_{x'x_2y_2x''x_2'}}{\overline{\delta }^{y_1y_2}} $$

where

$$ \overline{\delta }^{y_1y_2} = \sum _{x''x_1'x_2'z}\left( \sum _{x'x_2}\alpha _{x'x'_1x_2z}^{y_1}K_{x'x_2y_2x''x_2'}\right) $$

By substituting $\alpha$ into the expression of $\delta$ and simplifying $\overline{\alpha }^{y_1}$, we have

$$\begin{aligned} \delta _{x''x'_1x'_2z}^{y_1y_2}= & {} \frac{ \sum _{x'x_2}\left( \sum _{xx_1}\varPi _{xx_1x_2z}H_{xx_1y_1x'x'_1}\right) K_{x'x_2y_2x''x'_2} }{ \sum _{x''x_1'x_2'z}\left( \sum _{x'x_2}\left( \sum _{xx_1}\varPi _{xx_1x_2z}H_{xx_1y_1x'x'_1}\right) K_{x'x_2y_2x''x_2'}\right) }\\= & {} \frac{ \sum _{xx_1x_2}\varPi _{xx_1x_2z}\sum _{x'}H_{xx_1y_1x'x'_1}K_{x'x_2y_2x''x'_2} }{ \sum _{x''x_1'x_2'z}\left( \sum _{xx_1x_2}\varPi _{xx_1x_2z}\sum _{x'}H_{xx_1y_1x'x'_1}K_{x'x_2y_2x''x_2'}\right) }\\ \end{aligned}$$

The inner $\delta ^{y_1y_2}$ corresponds exactly to a normalized $(y_1,y_2)$-column of $\varPi {\rangle }(H;K)$ as per Eq. (11).

Lemma 4 is a straightforward generalisation our sequential composition for systems independent of any other collateral type [8, 9] as well as our compositional, but single secret, semantics [10, 11]. That is, the closed sequential composition is obtained by setting $\mathcal{X}_1 = \mathcal{X}_2 = \mathcal{Z}= \{*\}$ while the context aware version is obtained by setting $\mathcal{X}_1 = \mathcal{X}_2 = \{*\}$. Lemma 4 is slightly more general than the composition we define in [10] because it allows the declaration of new variables “on the go”. For instance, if we set $\mathcal{X}_1 = \{*\}$, then a new secret variable of type $\mathcal{X}_2$ that is declared in K does not change in H. The lifted map $[\![H]\!]^{\mathcal{X}_2}$ is aware of this upcoming new secret and accounts for the correlation between the new variable and current secret of type $\mathcal{X}$.