Abstract
Information flow properties, such as differential privacy, are subtle, and systems which are intended to enforce them can be tricky to get right. In this talk I will describe some lessons learned in attempting to derive faithful models of information flow systems, taking examples from our work on the ProPer system, a PINQ-like API which uses personalised privacy budgets and provenance tracking to enforce differential privacy.