Precise Enforcement of Progress-Sensitive Security
Program progress (or termination) is a covert channel that may leak sensitive information. To control information leakage on this channel, semantic definitions of security should be progress sensitive and enforcement mechanisms should restrict the channel's capacity. However, most state-of-the-art language-based information-flow mechanisms are progress insensitive - allowing arbitrary information leakage through this channel - and current progress-sensitive enforcement techniques are overly restrictive. The authors propose a type system and instrumented semantics that together enforce progress-sensitive security more precisely than existing approaches.