Secure diffuse computing: class #7

Teacher: Castellani

First part slides: need to get them.

Type rules

(1)
\begin{align} \Gamma:\ \textrm{Var}\ \rightarrow\ \textrm{SecLevels} \end{align}
(2)
\begin{align} \Gamma(x) = \tau \in\ \textrm{SecLevels} \end{align}

Soundness:

If $\Gamma \vdash c: \tau$ then c is secure w.r.t $\Gamma$

Type rules for expressions

(3)
\begin{align} \Gamma \vdash e: \tau \end{align}

Rule "Val":

(4)
\begin{align} \frac{} {\Gamma \vdash v: \perp} \end{align}

Rule "Var":

(5)
\begin{align} \frac {\Gamma(x) = \tau} {\Gamma \vdash x: \tau} \end{align}

Rule "Op":

(6)
\begin{align} \frac {\Gamma \vdash e_i: \tau \quad i = 1, 2} {\Gamma \vdash e_1\ \textrm{op}\ e_2: \tau} \end{align}

Rule "Sub-e":

(7)
\begin{align} \frac{\Gamma \vdash e: \tau \quad \tau \leq \tau'}{\Gamma \vdash e: \tau'} \end{align}

Type rules for commands

(8)
\begin{align} \Gamma \vdash: c: \tau \end{align}

Rule "Nil":

(9)
\begin{align} \frac {} {\Gamma \vdash \textrm{nil}: \Gamma} \end{align}

Rule "Ass":

(10)
\begin{align} \frac{\Gamma \vdash e: \tau \quad \Gamma \vdash x: \tau} {\Gamma \vdash x := e: \tau} \end{align}

Rule "Sub-c" (note that the ordering is inverted in respect to the Sub-e rule):

(11)
\begin{align} \frac{\Gamma \vdash c: \tau \quad \tau' \leq \tau} {\Gamma \vdash c: \tau'} \end{align}

Rule "Cond":

(12)
\begin{align} \frac{\Gamma \vdash e: \tau \quad \Gamma \vdash c_i: \tau \quad i = 1, 2} {\Gamma \vdash \textrm{if}\ e\ \textrm{then}\ c_1\ \textrm{else}\ c_2: \tau} \end{align}

Rule "Seq":

(13)
\begin{align} \frac{\Gamma \vdash c_1: \tau \quad \Gamma \vdash c_w: \tau} {\Gamma \vdash c_1; c_2: \tau} \end{align}

Rule "While":

(14)
\begin{align} \frac {\Gamma \vdash e: \tau \quad \Gamma \vdash c: \tau} {\Gamma \vdash\ \textrm{while}\ e\ \textrm{do}\ c: \tau} \end{align}

Examples

(15)
\begin{eqnarray} x_H := y_L \\ y_L := x_H & \textrm{insecure} \\ y_L := x_H + y_L & \textrm{insecure} \\ \textrm{if}\ x_H = 0 \ \textrm{then}\ y_L := 0 \\ \textrm{else}\ y_L := 1 & \textrm{insecure} \\ \textrm{if}\ x_H = 0 \ \textrm{then}\ y_L := 0 \\ \textrm{else}\ x_H := 1 & ? \\ x_H := 0; y_L := x_H & ? \\ x_H := 0; y_L := 0 & \textrm{secure} \\ \end{eqnarray}

This is not secure, nor typable (assigning incompatible variables):

(16)
\begin{align} \textrm{If}\ (Z_a \neq Z_b)\ \textrm{then}\ Z_a := Z_a + Z_b \ \textrm{else}\ nil \end{align}

Same, because of the expression types as the top type and then the if/then/else is not typable:

(17)
\begin{align} \textrm{If}\ (Z_a \neq Z_b)\ \textrm{then}\ Z_a := 1 \ \textrm{else}\ nil \end{align}

This is typable, as the assignment has the top type:

(18)
\begin{align} \textrm{If}\ (Z_a \neq Z_b)\ \textrm{then}\ x_H := 1 \ \textrm{else}\ nil \end{align}
Unclear, need to ask the teachers, since most is obviously derived works.