Secure diffuse computing: class #7

Teacher: Castellani

First part slides: need to get them.

Type rules

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


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

Type rules for expressions

\begin{align} \Gamma \vdash e: \tau \end{align}

Rule "Val":

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

Rule "Var":

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

Rule "Op":

\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":

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

Type rules for commands

\begin{align} \Gamma \vdash: c: \tau \end{align}

Rule "Nil":

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

Rule "Ass":

\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):

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

Rule "Cond":

\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":

\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":

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


\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):

\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:

\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:

\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.