SE547: Sequential noninterference [9/23]

Static analysis for noninterference satisfying:

1. In x = e, if e reads from an H variable, then x is an H variable.

2. In if (e) { c } else { d }, if e reads from an H variable, then c and d only write to H variables.

3. In while (e) { c }, if e reads from an H variable, then c only writes to H variables.

Which of these pass static analysis?

1. x_H=y_L;
2. y_L=x_H;
3. x_H=0; if(even(y_L)) { x_H=1; }
4. y_L=0; if(even(x_H)) { y_L=1; }