CAREER: Explorable Formal Models of Privacy Policies and Regulations

数据收集和分析使数字技术取得了巨大的进步，但这些数据的管理者对社会负有责任，以确保收集、存储和用户控制的实践符合用户的期望。管理数据隐私的政策和法规在向用户传达隐私期望和定义允许的数据使用范围方面发挥着关键作用。然而，在实践中，用户期望和软件公司的实际做法之间存在严重的不匹配，即使这些做法符合他们的隐私政策。该项目的目标是实现对隐私政策和法规的自动推理，从而帮助用户、策略开发人员和监管机构理解数据实践和策略的意外后果。过去对隐私自动推理的研究导致了对规则的逻辑语义进行形式化建模和支持机械化正确性证明的努力。另一方面，对用户透明度的渴望导致了策略注释方案的建议，该方案通过自然语言和可视化支持更清晰的表示。该项目旨在通过开发技术来统一这些目标，以表示正式和可探索的政策和法规，回答“如果”？除了提供可证明的保证外，还提供有关具体场景的问题。该项目需要在形式方法、叙事生成、自然语言处理和人机交互方面取得技术进步。研究团队将使用一种称为答案集编程（ASP）的关系编程模型，将隐私法规正式化，例如欧盟的通用数据隐私法规，以及针对软件公司和服务提供商的隐私政策。研究团队计划发现与ASP作为轻量级语义建模框架进行互操作的新技术，支持回答查询，生成揭示隐私漏洞的场景，生成全局正确性条件的反例，建议修复损坏的策略，并使策略开发人员和用户能够探索假设的场景。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.