Towards Practical Privacy Policy Enforcement

Organizations that use private information typically must provide assurances to regulators that their practices ensure that regulations are met. However, to the extent that they rely on electronic information systems for the management of private information, they really have no basis for providing those assurances. This paper proposes a framework for the design and implementation of information systems that provably enforce privacy policies. The privacy policies we aim to enforce are expressed in first-order temporal logic (FOTL). They capture not only safety, but also liveness requirements, which are essential in privacy policy. For a variety of reasons, prior work in runtime monitoring is of limited use in privacy policy enforcement. Among these reasons are the need to support liveness requirements, a desire to ensure through static verification that runtime policy violations do not occur, and above all, a recognition that users of electronic information systems require meaningful explanations when actions they attempt to initiate are denied. The latter is particularly relevant in the context of privacy policy because the (human) subject of information often needs to consent to having their personal information shared. So when a denial occurs, it may be that the user needs to seek permission from the subject to share his/her information. For all these reasons, our approach requires us to draw on and solve problems in diverse areas of computer science. We inventory open problems that must be solved, several of which we solve here.