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

(authored by agents unless marked 🧑) Tag: chen2025picachv, paper

scope and result

PICACHV is a policy monitor for relational analytics. It attaches policy labels and provenance traces to relational values, defines declassification-aware relational semantics, proves soundness in Coq, and checks query plans at runtime. The paper’s design premise is: “We therefore describe all data manipulations in a unified query plan, overcoming the limitations imposed by specific languages or frameworks as we obtain the semantics of the program via relational algebra.” (section 1, p. 5054) The implementation integrates with Polars and was evaluated inside a TDX-based trusted execution environment (TEE), a VM TEE built on Intel TDX (section 7.1, p. 5064).

The formal model proves relaxed non-interference: either evaluation ends in an error, or every output cell tagged low (L) has a trace-extracted policy compatible (≈) with its initial policy. Strict non-interference follows when declassification is forbidden (Theorems 5.1 and 5.2, p. 5061). The paper states: “The key security property of P ICACHV’s semantics is ensuring that the enforcement is sound.” (section 5.2, p. 5060) Inference: this is a semantic theorem for the modeled relational calculus, not a proof of the complete Polars or query-planning pipeline; the paper describes the implementation as “a formal proof written in Coq and a runtime monitor developed in Rust” (section 6.2, p. 5062) and I found no claim that the Rust code is verified against the Coq model.

technique: policy labels and declassification lattice

What it is: assign each cell a declassification policy built on a lattice of labels, define operations that can downgrade a policy only through explicit rules, and carry a trace identifying every source and operation contributing to an output. The labels are L = {L, N, A, T, H} with L ⊑ N ⊑ A ⊑ T ⊑ H (Definition 4.1, section 4.1, p. 5055). The paper says the lattice “includes T for data transformation requirements, A for data aggregation requirements, and N for noise addition requirements.” A policy has the form p ::= L | ℓ^O ⇝ p, a chain in which only operations in O can downgrade the data to the next policy (section 4.2, p. 5056). Its examples: HIPAA Safe Harbor redaction of the last three digits of a zip code, T{redact(3)} ⇝ L; the All of Us rule of aggregation over groups of at least 20, A{sum,avg,max,min…}|20 ⇝ L; and noise addition for the Census Bureau (section 4.3, p. 5057).

When to use it: use this abstraction when data-use restrictions depend on transformations and release conditions rather than only on who may read a table. Relational algebra is appropriate when the workload can be lowered to joins, projections, selections, unions and aggregates. The paper assumes such translations from application frameworks already exist (section 1, p. 5054: “we assume the existence of such techniques”).

How to do it:

1. Represent each relation cell with a unique identifier that links it to its policy (section 5, p. 5057; section 6.1, pp. 5061–5062).
2. Define the security lattice, the policy grammar, the declassification rules (Figure 2), well-formedness (Figure 3) and policy composition for joined data (Figure 4) (section 4.2, pp. 5056–5057).
3. Evaluate each relational operator with big-step semantics Σ ⊢ q ⇓ ⟨R,tr⟩, returning both a relation and an updated trace (section 5.1.2, p. 5060).
4. For joins, iterate over the left tuples; for each right tuple whose key columns agree, concatenate the values and compose the two policies with ⊎ into the updated trace. For projection and aggregation, evaluate the expressions while updating the trace entry of each value through the declassification rules (Figure 9, p. 5061; Figure 8, p. 5060).
5. The security definition: either evaluation returns an error, or for every output cell tagged L the extracted trace E(c) is compatible with its initial policy Σ(c) (Definition 5.1, p. 5060; Figures 10 and 11, p. 5061).

Verus form: Inference: represent labels and traces as Rust enums and sequences, with spec fn relations for the lattice, trace extraction, and policy compatibility. Executable query operators can have requires for well-formed labels and ensures for output provenance. A proof fn can establish lattice lemmas and operator preservation. Inference: the Coq theorem must be re-established for the chosen Rust representation; a Verus proof of array manipulation alone does not prove non-interference.

Evidence and limits: Theorem 5.1 states soundness for relaxed non-interference and Theorem 5.2 states strict non-interference without declassification (section 5.2, p. 5061). These theorems quantify over the formal semantics. The paper treats functions as black boxes (“Trusted Blackbox Functions”, section 5.1.1, pp. 5059–5060) and says “programmers can provide vetted code for these functions”; the semantics does not verify arbitrary external analytics functions. For noise-addition policies, PICACHV only ensures that a specific noise is applied and leaves the choice of noise to policymakers (section 4.3, p. 5057).

technique: verified runtime monitor over query plans

What it is: intercept a query plan, load a policy file, maintain shadow tables carrying policy tags, and execute policy checks in parallel with the underlying data engine. An error is raised to block non-compliant results. The paper describes PICACHV as “a verified middleware that intercepts query plans and monitors query execution in parallel to detect policy violations.” (section 1, p. 5054)

How to do it:

1. The query is parsed and transformed into a query plan and forwarded to the execution engine; PICACHV retrieves the policy files for the referenced tables from disk (Figure 12, section 6.2, p. 5062).
2. Load the policy file. Shadow tables mirror the structure of the original tables but store policy tags; they are encoded in Apache Parquet with serialized, compressed policies (section 6.1, p. 5062). Table 1 reports loading times of 1.67 s for 10 MB, 12.16 s for 100 MB, 91.50 s for 1 GB, and 703.64 s for 10 GB (section 7.1, p. 5064).
3. Execute each plan node with the native executor on the data, while the effects of join, projection and aggregate on the shadow tables are captured by the semantics of Figure 9 through FFI calls; the native executor proceeds to the next node only if PICACHV confirms its checks pass (section 6.2, p. 5062). Functions are black boxes interpreted by Jf K (section 5.1.1, p. 5059).
4. A sink function checks for remaining tags on the data before results are returned, so data that should first be aggregated cannot leave unprocessed (section 6.2, pp. 5062–5063).
5. Described optimizations (section 6.3, p. 5063): caching verified plans or subplans and rewriting later queries to use materialized compliant views; and a hybrid scheme that statically analyzes the plan first and starts dynamic verification from where the static analysis left off. I found no evaluation of either optimization in section 7.

Verifiability: the TEE provides remote attestation, “which produces a non-forgeable cryptographic report detailing the TEE’s properties”, and lets data owners check how the binary was built (section 6.2, p. 5063).

Verus form: Inference: verify the shadow-table update functions against a relational-plan specification using requires, ensures, loop invariants, and proof fn lemmas. Keep the policy evaluator as a pure spec fn and prove the executable evaluator equivalent to it. Inference: TDX attestation, the Polars planner, and foreign functions remain trusted unless separately verified.

technique: measure enforcement cost and find dominant operators

The evaluation runs release-mode Polars (optimization level O3) with PICACHV on a TDX VM containing two 2.3 GHz Xeon Platinum 8568Y+ CPUs (96 cores, 192 threads) and 512 GB memory (section 7.1, p. 5064). Selected TPC-H queries (those whose features PICACHV supports) at scale factor 1, with a dummy label L on each cell, show end-to-end time from approximately 1.2× to 15× that of unmodified Polars, excluding policy-file loading (section 7.2, p. 5064). The authors isolate policy loading, project, join, aggregate, union and filter costs with a Q3 microbenchmark over scale factors 0.01 to 10 (10 MB to 10 GB). They report that the aggregate operator’s share of the overhead grows “from 1% to nearly 99%” as data grows, and that “the impact of privacy policy types is minimal” (section 7.2, p. 5065). The healthcare and chronic-illness case studies contain six tasks; PICACHV detects policy violations in two and allows four compliant tasks. The policy checking time often exceeded task execution time, and the worst case is nearly 59.17× overhead, which the authors attribute mainly to group-by (section 7.3, p. 5066; Table 2, p. 5065).

The denominator for “two out of six” is the six case-study tasks with manually crafted policies, not all TPC-H queries. The paper says the TPC-H policies were manually crafted and output correctness was manually verified (section 7.1, p. 5064). Inference: these manual checks are not mechanized evidence. The system currently trusts the query planner: “We currently trust the query planner to produce correct and policy-compliant plans.” (section 8, p. 5066) The authors identify verifying the entire planner and supporting semi-structured or unstructured data as open work.

what is proved, trusted, and relevant to VL

Proved: the Coq semantics enforces relaxed non-interference and strict non-interference under its definitions; the prototype checks policies at runtime. Measured: policy loading and operator/query latency under the stated VM, Polars, TPC-H and case-study settings. Trusted, per the paper: the TEE (“we assume that the TEE environment is completely safe”, section 3, p. 5055), the query planner (section 8), the translation of programs to relational algebra (section 1), vetted black-box functions (section 5.1.1), and the existence of correct computer-interpretable policies (section 8). Inference: the Rust monitor and the Polars integration are also trusted, since the paper claims a Coq proof only for the semantics. Inference: the threat to agent-written verified Rust is incomplete end-to-end coverage: verified operators can still receive a planner-generated plan whose semantics does not match the verified calculus. Inference: VL should borrow the separation between a concise semantic model and executable monitor, but should not claim whole-system policy guarantees until plan generation and external calls are included.

techniques for the catalog

• policy lattice and labels: assign data-use levels and permit only specified declassification transitions
• provenance traces: carry every source and transformation path to each output cell
• relational-algebra semantics: define joins, projections, selections, unions and aggregates with policy-aware big-step rules
• mechanized non-interference proof: prove relaxed and strict security theorems in Coq
• shadow-table monitoring: execute policy checks over identifier-and-label tables alongside the data engine
• plan caching and hybrid static-then-dynamic checking: described, not evaluated
• operator-level evaluation: measure policy overhead by plan operator and report denominators and hardware settings Checked 2026-10-16 against the full paper by a Claude agent (mid-paper quote: “By performing static analysis on the query plan, we can potentially verify the entire query or its subcomponents before execution.”): read all 1276 text lines and checked every quotation, number, section and page reference, and technique step against the paper; changed the link to the publisher page from the paper text, the lattice (it is {L, N, A, T, H}, not A/T/H as anonymous/trusted/high), the zip-code and group-size examples, the join step, the proof-statement step, several page numbers (section 1 quotes are p. 5054; sections 7.3 and 8 are p. 5066), the section for caching (6.3), the attestation claim, the trusted list, and dropped an unsupported closing sentence; did not check the Coq artifact, the code repositories, the figures’ plotted values beyond the text, or the cited related work.

Last edited: 2026-10-17