Language-Based Information Erasure

Abstract

Real computing systems sometimes need to forget sensi- tive 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 infor- mation flow policies, corresponding to a noninterference re- quirement, 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 enforce- ment either statically or dynamically. Further, the signifi- cance of these policies to security is formally explained in terms of trace-based semantic security properties: general- izations of noninterference that accommodate erasure and declassification.