Title: Scheduler-Independent Declassification

Abstract:
The controlled declassification of secrets has received much
attention in research on information-flow security, though mostly for se-
quential programming languages. In this article, we aim at guarantee-
ing the security of concurrent programs. We propose the novel security
property WHAT&WHERE that allows one to limit what information
may be declassified where in a program. We show that our property
provides adequate security guarantees independent of the scheduling al-
gorithm (which is non-trivial due to the refinement paradox) and present
a security type system that reliably enforces the property. In a second
scheduler-independence result, we show that an earlier proposed security
condition is adequate for the same range of schedulers. These are the first
scheduler-independence results in the presence of declassification.