SE547: Declassification [17/23]

Mandatory Access Control is usually too restrictive in practice: we need some way to declassify data.

  booleanL checkPwd (StringL uid, StringL guess, StringH pwd) {
    return (guess == pwd); // Does not pass static analysis!
  }

Declassification requires authority, either granted directly:

  booleanL checkPwd (StringL uid, StringL guess, StringH pwd)
  where authority(H) {
    return declassify(guess == pwd, L);
  }

or granted to the calling method and delegated:

  booleanL checkPwd (StringL uid, StringL guess, StringH pwd)
  where caller(H) {
    return declassify(guess == pwd, L);
  }