Language-based information erasure

Real computing systems sometimes need to forget sensitive information. This paper explores the specification and semantics of information erasure policies, which impose a strong, end-to-end requirement that information be either erased or made less accessible. Simple lattice-based information flow policies, corresponding to a noninterference requirement, are augmented with the ability to express explicit erasure and declassification policies. Examples are given of applying this expressive policy language to real systems. The paper gives tools for reasoning about policy enforcement either statically or dynamically. Further, the significance of these policies to security is formally explained in terms of trace-based semantic security properties: generalizations of noninterference that accommodate erasure and declassification.