Picachv：面向安全数据分析的形式化验证数据使用策略执行
密码学与安全
2025-01-22 v1 数据库
编程语言
摘要
在复杂隐私策略下确保分析中敏感数据的正确使用是一个日益严峻的挑战。许多现有方法在不同数据处理框架之间缺乏可移植性、可验证性和可扩展性。我们引入了 Picachv，一种自动执行数据使用策略的新型安全监控器。它基于关系代数作为程序语义的抽象，能够在程序执行期间对生成的查询计划执行策略。这种方法简化了跨不同分析操作的分析，并支持多种前端查询语言。通过在 Coq 中形式化数据使用策略和关系代数语义，我们证明了 Picachv 正确执行策略。Picachv 还利用可信执行环境来增强运行时的信任，向利益相关者提供可证明的策略合规性，即分析任务符合其数据使用策略。我们将 Picachv 集成到最先进的数据分析框架 Polars 中，并使用 TPC-H 基准评估其性能。我们还将我们的方法应用于实际用例。我们的工作展示了形式化方法在保护数据分析安全方面的实际应用，解决了关键挑战。
引用
@article{arxiv.2501.10560,
title = {Picachv: Formally Verified Data Use Policy Enforcement for Secure Data Analytics},
author = {Haobin Hiroki Chen and Hongbo Chen and Mingshen Sun and Chenghong Wang and XiaoFeng Wang},
journal= {arXiv preprint arXiv:2501.10560},
year = {2025}
}