SE547: Concurrent noninterference [15/23]

Noninterference for concurrent programs is much harder. Thread α:

  while (trigger0H == 0) {}  resultL = 1;
  trigger1H++

Thread β:

  while (trigger1H == 0) {} resultL = 0;
  trigger0H++;

Thread γ:

  if (secretH == 0) { trigger0H++; } else { trigger1H++; }

What happens in initial memory { secretH = 0, everything else = 0 }?

What happens in initial memory { secretH = 1, everything else = 0 }?

Smith and Volpano scale this up to leak an n-bit PIN, not just one bit.