Progress sensitive security

This is also known as termination sensitive security. Termination is considered a covert channel as a terminating program might reveal some information to the attacker. A program should be progress/termination sensitive to prevent information leakage in this channel. This is enforced via the language semantics and type system. A progress/termination insensitive language reveals arbitrary information at termination.

Termination Insensitive Noninterference (TINI)

TINI treats a diverging trace indistinguishable from any other trace. This indistinguishability is called weak indistinguishability (which is also timing insensitive). While, on other hand, TSNI (termination sensitive NI) distinguish between nonterminating and terminating traces.