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

TL;DR

Picachv tackles the problem of enforcing complex data-use policies during analytics by modeling program semantics with a formal RA^P (relational algebra with policy declassification) and proving policy compliance in Coq. It implements a dynamic runtime monitor, embedded inside TEEs, that intercepts query plans, enforces per-cell declassification rules, and provides verifiable attestations to data owners. The system uses shadow-policy tables and a modular policy-logic lattice to support policy composition and overlays across diverse frontends, and it is integrated with Polars and demonstrated on the TPC-H benchmark with real-world case studies. Findings show that Picachv can enforce nuanced privacy requirements with manageable overheads, while identifying concrete optimization opportunities in projection and aggregation paths and highlighting future work in broader data-types and end-to-end planner verification.

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.

Figures (16)

• Figure 1: The refined lattice flows-to rules $\ell_1^{\mathcal{O}_1} \sqsubseteq^{\ast} \ell_2^{\mathcal{O}_2}$.
• Figure 2: The declassification rules $p \lhook\joinrel\xrightarrow{op, \ell} p'$ for policy $p$.
• Figure 3: The well-formedness property of policy $p$.
• Figure 4: The composition rules for policy $p$.
• Figure 5: The syntax for $\mathsf{RA^P}$.

Theorems & Definitions (5)

• Definition 4.1: Security lattice
• Definition 5.1: Relaxed non-interference
• Theorem 5.1: Soundness
• Theorem 5.2: Strict non-interference
• proof