Data collection and analysis enable great advancements in digital technology, but the stewards of this data have a responsibility to society to ensure that the practices of collection, storage, and user control abide by user expectations. Policies and regulations governing data privacy play a critical role in communicating privacy expectations to users and defining the bounds of permissible data use. However, in practice, there are severe mismatches between user expectations and the actual practices of software companies, even when those practices conform with their privacy policies. This project's goal is to enable automated reasoning over privacy policies and regulations that can assist users, policy developers, and regulators in understanding unintended consequences of data practices and policies. Past research on automated reasoning for privacy has led to efforts to formally model the logical semantics of regulations and support mechanized correctness proofs. The desire for transparency to users, on the other hand, has led to proposals for policy annotation schemes that support clearer presentation through natural language and visualization. This project aims to unify these goals by developing techniques to represent policies and regulations that are both formal and explorable, answering 'what if'? questions about specific scenarios in addition to providing provable guarantees. The project requires technical advances in formal methods, narrative generation, natural language processing, and human-computer interaction. The research team will formalize privacy regulations such as the European Union's General Data Privacy Regulation, as well as privacy policies specific to software companies and service providers, using a relational programming model known as Answer Set Programming (ASP). The research team plans to discover new techniques for interoperating with ASP as a lightweight semantic modeling framework, with support for answering queries, generating scenarios that reveal privacy loopholes, generating counterexamples to global correctness conditions, suggesting repairs for broken policies, and enabling the exploration of hypothetical scenarios by policy developers and users.
CAREER: Explorable Formal Models of Privacy Policies and Regulations