  Noninterference is a popular semantic security condition because it offers
strong end-to-end guarantees, it is inherently compositional, and it can be
enforced using a simple security type system. Unfortunately, it is too
restrictive for real systems. Mechanisms for downgrading information are needed
to capture real-world security requirements, but downgrading eliminates the
strong compositional security guarantees of noninterference.
  We introduce nonmalleable information flow, a new formal security condition
that generalizes noninterference to permit controlled downgrading of both
confidentiality and integrity. While previous work on robust declassification
prevents adversaries from exploiting the downgrading of confidentiality, our
key insight is transparent endorsement, a mechanism for downgrading integrity
while defending against adversarial exploitation. Robust declassification
appeared to break the duality of confidentiality and integrity by making
confidentiality depend on integrity, but transparent endorsement makes
integrity depend on confidentiality, restoring this duality. We show how to
extend a security-typed programming language with transparent endorsement and
prove that this static type system enforces nonmalleable information flow, a
new security property that subsumes robust declassification and transparent
endorsement. Finally, we describe an implementation of this type system in the
context of Flame, a flow-limited authorization plugin for the Glasgow Haskell
Compiler.
