Information flow policies like confidentiality and integrity are essential to the security of many software systems such as medical information systems, collaborative planning systems and voting systems. Confidentiality policies must ensure that unauthorised clients (attackers) cannot acquire sensitive information. Integrity policies must ensure that untrustworthy data does not flow into trusted sites.

Formal techniques such as program logics, type theory and abstract interpretation facilitate reasoning about information flow policies for application-level software. These techniques help capture policy semantics and permit specification of enforcement mechanisms for verifying complex application software, thus providing end-to-end security guarantees. A key challenge is to provide semantics to declassification policies which involve the deliberate, partial release of confidential information during system execution.