糖心TV

I will present some work-in-progress on the semantics and enforcement of
data erasure policies. This is joint work with David Sands.

A now familiar example involving data erasure is that of online credit
card transactions. A customer typically provides credit card details to a
payment system on the understanding that the following promises are kept:
(i) Noninterference (NI): the card details may flow to the card issuer,
but not to other parties; (ii) Erasure: the payment system will not retain
any record of the card details once the transaction is complete. This
example shows that we need to be able to reason about NI and erasure in
combination, and that we need to consider interactive systems (were it not
for the interaction between payment system and card issuer, the card
details could be dispensed with altogether and erasure would be
unnecessary). We show first that an end-to-end erasure property can be
encoded -- by a relabelling of security levels -- as a ``flow sensitive''
noninterference property. Then, by a judicious choice of language
constructs to support erasure policies, we adapt this result to an
interactive setting. Finally, we use the noninterference encoding to
design a type system which guarantees that well typed programs are
properly erasing. Although erasure policies have been discussed in earlier
papers, this appears to be the first static analysis to enforce erasure.