SE547: Sequential noninterference [9/23] Previous pageContentsNext page

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. xH=yL;
  2. yL=xH;
  3. xH=0; if(even(yL)) { xH=1; }
  4. yL=0; if(even(xH)) { yL=1; }

Previous pageContentsNext page