Picachv: Formally Verified Data Use Policy Enforcement for Secure Data Analytics

• URL: http://arxiv.org/abs/2501.10560v1
• Date: Fri, 17 Jan 2025 21:30:55 GMT
• Title: Picachv: Formally Verified Data Use Policy Enforcement for Secure Data Analytics
• Authors: Haobin Hiroki Chen, Hongbo Chen, Mingshen Sun, Chenghong Wang, XiaoFeng Wang,
• Abstract summary: We introduce Picachv, a novel security monitor that automatically enforces data use policies. It works on relational algebra as an abstraction for program semantics, enabling policy enforcement on query plans generated by programs during execution. We integrate Picachv into Polars, a state-of-the-art data analytics framework, and evaluate its performance using the TPC-H benchmark.
• Score: 10.630556229470681
• License:
• Abstract: Ensuring the proper use of sensitive data in analytics under complex privacy policies is an increasingly critical challenge. Many existing approaches lack portability, verifiability, and scalability across diverse data processing frameworks. We introduce Picachv, a novel security monitor that automatically enforces data use policies. It works on relational algebra as an abstraction for program semantics, enabling policy enforcement on query plans generated by programs during execution. This approach simplifies analysis across diverse analytical operations and supports various front-end query languages. By formalizing both data use policies and relational algebra semantics in Coq, we prove that Picachv correctly enforces policies. Picachv also leverages Trusted Execution Environments (TEEs) to enhance trust in runtime, providing provable policy compliance to stakeholders that the analytical tasks comply with their data use policies. We integrated Picachv into Polars, a state-of-the-art data analytics framework, and evaluate its performance using the TPC-H benchmark. We also apply our approach to real-world use cases. Our work demonstrates the practical application of formal methods in securing data analytics, addressing key challenges.

Related papers

• Few-shot Policy (de)composition in Conversational Question Answering [54.259440408606515]
  We propose a neuro-symbolic framework to detect policy compliance using large language models (LLMs) in a few-shot setting. We show that our approach soundly reasons about policy compliance conversations by extracting sub-questions to be answered, assigning truth values from contextual information, and explicitly producing a set of logic statements from the given policies. We apply this approach to the popular PCD and conversational machine reading benchmark, ShARC, and show competitive performance with no task-specific finetuning.
  arXiv  Detail & Related papers  (2025-01-20T08:40:15Z)
• PolicyLR: A Logic Representation For Privacy Policies [34.73520882451813]
  We propose PolicyLR, a new paradigm that offers a comprehensive machine-readable representation of privacy policies. PolicyLR converts privacy policies into a machine-readable format using valuations of atomic formulae. We demonstrate PolicyLR in three privacy tasks: Policy Compliance, Inconsistency Detection and Privacy Comparison Shopping.
  arXiv  Detail & Related papers  (2024-08-27T07:27:16Z)
• Offline Reinforcement Learning from Datasets with Structured Non-Stationarity [50.35634234137108]
  Current Reinforcement Learning (RL) is often limited by the large amount of data needed to learn a successful policy. We address a novel Offline RL problem setting in which, while collecting the dataset, the transition and reward functions gradually change between episodes but stay constant within each episode. We propose a method based on Contrastive Predictive Coding that identifies this non-stationarity in the offline dataset, accounts for it when training a policy, and predicts it during evaluation.
  arXiv  Detail & Related papers  (2024-05-23T02:41:36Z)
• Learning Optimal Deterministic Policies with Stochastic Policy Gradients [62.81324245896716]
  Policy gradient (PG) methods are successful approaches to deal with continuous reinforcement learning (RL) problems. In common practice, convergence (hyper)policies are learned only to deploy their deterministic version. We show how to tune the exploration level used for learning to optimize the trade-off between the sample complexity and the performance of the deployed deterministic policy.
  arXiv  Detail & Related papers  (2024-05-03T16:45:15Z)
• Automated Detection and Analysis of Data Practices Using A Real-World Corpus [20.4572759138767]
  We propose an automated approach to identify and visualize data practices within privacy policies at different levels of detail. Our approach accurately matches data practice descriptions with policy excerpts, facilitating the presentation of simplified privacy information to users.
  arXiv  Detail & Related papers  (2024-02-16T18:51:40Z)
• Offline RL with No OOD Actions: In-Sample Learning via Implicit Value Regularization [90.9780151608281]
  In-sample learning (IQL) improves the policy by quantile regression using only data samples. We make a key finding that the in-sample learning paradigm arises under the textitImplicit Value Regularization (IVR) framework. We propose two practical algorithms, Sparse $Q$-learning (EQL) and Exponential $Q$-learning (EQL), which adopt the same value regularization used in existing works.
  arXiv  Detail & Related papers  (2023-03-28T08:30:01Z)
• Mutual Information Regularized Offline Reinforcement Learning [76.05299071490913]
  We propose a novel MISA framework to approach offline RL from the perspective of Mutual Information between States and Actions in the dataset. We show that optimizing this lower bound is equivalent to maximizing the likelihood of a one-step improved policy on the offline dataset. We introduce 3 different variants of MISA, and empirically demonstrate that tighter mutual information lower bound gives better offline RL performance.
  arXiv  Detail & Related papers  (2022-10-14T03:22:43Z)
• Policy Information Capacity: Information-Theoretic Measure for Task Complexity in Deep Reinforcement Learning [83.66080019570461]
  We propose two environment-agnostic, algorithm-agnostic quantitative metrics for task difficulty. We show that these metrics have higher correlations with normalized task solvability scores than a variety of alternatives. These metrics can also be used for fast and compute-efficient optimizations of key design parameters.
  arXiv  Detail & Related papers  (2021-03-23T17:49:50Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.