CAREER: Explorable Formal Models of Privacy Policies and Regulations

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

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.