Reconciling progress-insensitive noninterference and declassification
Practitioners of secure information flow often face a design challenge: what is the right semantic treatment of leaks via termination? On the one hand, the potential harm of untrusted code calls for strong progress-sensitive security. On the other hand, when the code is trusted to not aggressively exploit termination channels, practical concerns, such as permissiveness of the enforcement, make a case for settling for weaker, progress-insensitive security. This binary situation, however, provides no suitable middle point for systems that mix trusted and untrusted code. This work connects the two extremes by viewing progress-insensitivity as a particular form of declassification. Our novel semantic condition reconciles progress-insensitive security as a declassification bound on the so-called progress knowledge (in an otherwise progress-sensitive setting). We show how the new condition can be soundly enforced using a mostly standard information-flow monitor.