Pith. sign in

REVIEW 4 major objections 6 minor 64 references

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

T0 review · 4 major / 6 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Picachv claims that data-use policies can be enforced soundly at the relational-algebra level, proving that every released value has been declassified by exactly the cell's required operations.

desk verdict The relational-algebra policy monitor is a genuinely useful idea, but the headline 'formally verified enforcement' isn't yet supported: the soundness theorem never forces released cells to be low, and the sink that does this lives outside the verified calculus. read the letter →

arxiv 2501.10560 v1 pith:XWRMX4GM submitted 2025-01-17 cs.CR cs.DBcs.PL

Haobin Hiroki Chen , Hongbo Chen , Mingshen Sun , Chenghong Wang , XiaoFeng Wang This is my paper · ORCID
classification cs.CRcs.DBcs.PL
keywords datausepolicyenforcementrelationalalgebradeclassificationinformationflowcontrolformalverificationruntimesecuritymonitorTrustedExecutionEnvironmentqueryplan
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper tries to establish that data-use policies—conditions like "aggregate to groups of at least 20 before release"—can be enforced automatically and with mathematical certainty by monitoring query plans rather than source code. The trick is to view every analytical program as relational algebra: each cell of data carries a policy describing which operations may downgrade it, and a runtime monitor traces every operation applied to each cell, blocking the query with an error if a forbidden step is attempted. The authors formalize this policy-carrying relational algebra in a proof assistant and prove a soundness theorem: if a value is released, its trace shows it was downgraded exactly along the chain its source cells required, and when no declassification is allowed the guarantee reduces to strict non-interference. They integrate the monitor into a popular dataframe engine and report that on a standard decision-support benchmark the overhead is roughly 1.2x to 15x, with the largest costs in projection and aggregation. If the theorem holds for the implementation, data owners can rely on a verifiable guarantee that analytics in untrusted cloud environments comply with the policies they set.

What carries the argument

The load-bearing object is a policy-carrying relation: a relational algebra (RAP) whose every cell is a tagged value (primitive value plus unique id), with a policy store mapping each id to a declassification policy and a program trace recording every operation applied. The trace is what makes the semantics honest: when a unary or binary operation is applied, the trace checks the cell's current policy, downgrades it if the operation is in the allowed set, and otherwise either preserves it or raises an error; aggregate and join operations fold and compose policies respectively. The refined flows-to relation $\ell_1^{O_1} \sqsubseteq^* \ell_2^{O_2}$ and the composition rules for policy join are what let policies be chained and merged across datasets. The main formal result is that this operational semantics is sound with respect to relaxed non-interference, proved by induction in a proof assistant.

What would settle it

Compare the monitor's recorded per-cell traces against a ground-truth log of every primitive operation the execution engine actually performs on each cell; if any released low-tagged cell's true computation includes an operation absent from its trace, or omits a required downgrade, the soundness theorem would not hold for the implemented system. A cheaper test is to feed the monitor a plan whose physical executor intentionally computes an aggregate via an unvetted foreign function: a release would falsify the enforcement claim, and an error would confirm the monitor is at least conservative.

Watch

Extended reading notes

Core claim

The central claim is Theorem 5.1: the semantics enforces relaxed non-interference. Concretely, for any data store and query, either evaluation errors, or every low-tagged cell in the output has a trace showing that the operations applied to its source cells declassified it through the allowed policy chain; queries that cannot produce such traces never return. To make this work, policies are not just labels but chains $p ::= L \mid \ell^O \leadsto p$, where the label records what kind of use a cell requires (e.g., transformation, aggregation, or noise addition) and the set $O$ records which specific operations count as satisfying that requirement. Relational operators update per-cell traces, joins compose the two input policies, and a sink check refuses to release any cell still carrying a non-low policy. A second theorem states that with no declassification allowed, the system enforces strict non-interference, so the relaxed guarantee is a conservative extension of ordinary information-flow security.

Load-bearing premise

The guarantee covers only what query plans say: the system trusts the query planner to produce correct and policy-compliant plans, so a planner that drops, miscompiles, or reorders an operation would let Picachv's tags miss the actual behavior.

Editorial extensions

If this is right

  • Any program that compiles to relational algebra—SQL, dataframe APIs, or other front ends—can be monitored with the same verified core, so the enforcement mechanism is portable across languages.
  • A data owner can verify compliance remotely: because the monitor runs inside a trusted execution environment with attestation, the owner can check that the attested binary enforces these policies before data is processed.
  • Policies from different sources compose: joining two relations merges their policy chains, and overlaying a stricter user-level preference onto a base policy is supported by the same composition rules.
  • When no declassification is allowed, the same mechanism gives strict non-interference, so the relaxed mode is a conservative extension rather than a weakening.
  • Policies that real regulations impose, such as redaction of certain fields or aggregation with minimum group sizes, are expressible directly as chains ending in $L$.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The authors leave the query planner trusted; if the planner itself were verified or if the monitor observed physical operators rather than plans, the same formal core would extend the guarantee to actual execution. This is the natural next step their limitation note points to.
  • The same relational-algebra enforcement idea could be transplanted to tensor relational algebras for machine learning, where the objects are matrices rather than cells and the declassification operations are things like clamped aggregate release; the paper mentions tensor relational algebra only as a limitation, not a plan.
  • An automated policy interpreter would turn natural-language regulations into these chains; the paper treats that as orthogonal, so combining the two would make the formalism deployable without hand-written policy files.
  • The reported overhead scaling suggests that the aggregate operation, not label checking, dominates cost; optimizing grouping or parallelizing policy evaluation for aggregates is a testable engineering direction not developed in the paper.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 6 minor

Summary. The paper presents Picachv, a runtime security monitor that enforces data use policies by operating on relational-algebra query plans rather than on any specific front-end language. It defines a security lattice with declassification policies, gives an operational semantics for a relational algebra calculus called RAP, and claims a Coq-mechanized soundness theorem in the form of relaxed non-interference. The implementation is a Rust dynamic library integrated into Polars, uses shadow tables for policy tags and a sink step before releasing results, and is intended to run inside TEEs to provide remote-attestation-based assurance. The evaluation reports overhead on TPC-H queries and two healthcare-related case studies. The central claim is that Picachv correctly enforces data use policies, with the formal result as the main evidence.

Significance. If the verification claim were fully supported, the paper would be a useful step: it targets an intermediate representation used by many analytics frameworks, builds on the established relaxed non-interference condition of Li and Zdancewic, and includes a real integration with Polars plus benchmark measurements. The shadow-table design and the separation of policy data from actual data are practical and clearly described. However, the central formal guarantee currently has a significant gap: the soundness theorem does not constrain high-labeled outputs, and the release sink described in the implementation is absent from the formal calculus and the Coq statement. As written, the paper demonstrates a policy-tracking semantics with plausible enforcement behavior, but it does not yet establish the claimed 'formally verified data use policy enforcement' for the released system.

major comments (4)
  1. [§5.2, Definition 5.1 and Figure 5] The soundness theorem is vacuous for result cells that are not tagged L. Definition 5.1 only requires E(c) ≈ Σ(c) when ⟨c,L⟩ ∈ tr; for a cell tagged with a higher label, the implication holds trivially. Since the RAP syntax in Figure 5 contains no release or sink operator, the semantics can return a relation containing H-labeled cells while Theorem 5.1 still holds. The actual release guard is the sink described in Section 6.2, which is not part of the formal syntax, the reduction rules, or the Coq development. Consequently, the paper's central claim that Picachv blocks non-compliant outputs before release is not entailed by the mechanized theorem.
  2. [Appendix A.2, Theorem 5.2] The proof of Theorem 5.2 (strict non-interference) invokes 'the finalization function at the end of the execution' and says it filters out data with remaining tags. No such finalization function is defined in RAP or in the formal model, and the sink is only described as an implementation component in Section 6.2. As a formal statement, Theorem 5.2 is therefore unsupported; if the intended meaning is that the implementation's sink performs this final check, that check must be formalized and proved over the actual execution pipeline.
  3. [Appendix A.1 and Open Science] The paper labels its contribution 'formally verified', but Appendix A.1 contains only a proof sketch ('mathematical induction over Σ ⊢ q ⇓ ⟨R,tr⟩'), and the Coq development is not shipped or identified by a commit hash. The reader cannot check whether Theorem 5.1 is actually mechanized, nor whether the Coq definitions match the rules in Figures 7–11. For a formal-verification claim, the artifact or a precise pointer to its version is essential; without it, the central soundness assertion is not verifiable from the manuscript alone.
  4. [§6.2 and §8] Even if Theorem 5.1 were fully proved for the RAP calculus, it governs the abstract semantics, not the Rust monitor, the FFI boundary, or the native Polars executor. Section 8 acknowledges that the query planner is trusted, but the FFI calls and native execution path are also outside the formal model. The remote-attestation claim in Section 6.2 that stakeholders receive 'provable policy compliance' therefore overstates what the formal results establish; an end-to-end refinement argument from RAP reduction to the implemented execution environment would be needed.
minor comments (6)
  1. [§2] There is a typo in the related work section: 'renforce' should be 'enforce'.
  2. [§5.2] The phrase 'oututting a final relation R' appears to be a typo for 'outputting'.
  3. [§5.1.2] The text says 'We present reduction rules for relational operators in Figure 7', but the operator rules are in Figure 9; Figure 7 contains the expression evaluation rules.
  4. [Figure 9] In the JOIN T rule, the premise 'tr = Stri' and the use of 'tr′' inside the tuple-level rule are difficult to parse; please clarify how the trace is threaded through the join and how policies p1 ⊎ p2 are inserted.
  5. [Table 2] The columns 'Execution Time (ms)' and 'Checking Time (ms)' are presented with values such as '32 .69 469 .394'; the formatting makes it hard to tell which number is the baseline and which is the checking overhead. Please use separate clear columns.
  6. [Open Science] The code repository is given as https://github.com/picachv, but no commit hash or versioned artifact is provided; please link to a permanent release of the Coq development and the Rust monitor.

Circularity Check

1 steps flagged · score 6.0 of 10

Release guarantee in Theorem 5.2 is obtained by defining the sink/finalization to filter out non-L data, so the system-boundary enforcement claim reduces to an unformalized definition rather than to the Coq-verified RAP semantics.

  1. self definitional [Section 6.2 (Sink); Appendix A.2 (Proof of Theorem 5.2); RAP syntax Figure 5 and reduction rules Figure 9]
    "After execution, a sink function (see Figure 13) is applied before results are returned. This step prevents data with remaining tags from inadvertently leaving the protected environment. ... By the definition of the finalization function at the end of the execution, we immediately filter out data with the remaining tags. Thus, if the program returns valid data, then following the soundness theorem, due to invocation of the sink function, we know that ∀c ∈ R,E(c) ≡ L, meaning that the query trace is equivalent to a computation that involves no secret."

    The claimed formal guarantee that every released cell has been declassified along its policy chain is not entailed by Theorem 5.1: Definition 5.1 imposes a condition only on cells satisfying ⟨c,L⟩ ∈ tr, so RAP reductions (Figure 9) can return cells with higher labels while the theorem holds vacuously, and the RAP syntax (Figure 5) contains no sink or release operator. Theorem 5.2's proof injects the missing release condition by appealing to a 'finalization function' that 'filter[s] out data with the remaining tags.' Once the function is defined as a filter, the conclusion ∀c ∈ R, E(c) ≡ L is true by construction of that filter, not by the Coq-verified reduction semantics.

full rationale

No fitted-parameter or self-citation circularity is present: the security condition is adapted from external work (Li and Zdancewic, POPL 2005, ref [35]) and declassification policies from Chong and Myers (CCS 2004, ref [19]). The proof of Theorem 5.1 is an internal soundness argument that the trace-update rules preserve a relationship between recorded operation chains and initial policies, which has independent content. The significant circular/definitional issue is at the release boundary: the paper's headline claim that PICACHV enforces data-use policies before results leave the system depends on the sink/finalization step described in Section 6.2, which is not part of the RAP syntax or reduction rules and is not covered by the Coq development. Theorem 5.2 obtains strict non-interference by defining that finalization to filter out any remaining tags, making the release-side guarantee true by definition rather than by the verified semantics. Section 8's explicit reliance on a trusted query planner is an acknowledged end-to-end gap but is an orthogonal trust assumption, not a circular reduction. The score reflects this one load-bearing by-construction release guarantee while recognizing that the main relaxed non-interference theorem is not itself a tautology.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

No numeric parameters are fitted to data. The load-bearing inputs are modeling assumptions about query planning, TEE security, well-formed policies, and UDF vetting. The formal soundness theorem is a property of the paper's own operational semantics, relative to the relaxed non-interference definition borrowed from Li-Zdancewic.

assumptions (5)
  • domain assumption Program semantics can be represented as relational algebra query plans.
    Section 1 says we assume the existence of such techniques and cites translators; Section 8 says the planner is trusted, so the guarantee does not cover planner bugs.
  • domain assumption The TEE environment is completely safe.
    Section 3 Threat Model: hardware side-channels and TEE exploits are outside scope, assumed mitigated.
  • domain assumption Policies are well-formed descending chains of labels.
    Section 4.2 defines wf, and the compatible relation in Figure 11 uses wf(p), but Theorem 5.1 does not state well-formedness as a premise, leaving an implicit invariant on the policy store.
  • domain assumption User-defined functions are vetted blackboxes.
    Section 5.1.1 treats functions as blackboxes and states programmers can provide vetted code for these functions.
  • domain assumption new_id generates collision-free identifiers.
    Section 5.1.1 assumes the identifier generator is like a UUID generator, so id conflicts are not a concern.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Picachv: Formally Verified Data Use Policy Enforcement for Secure Data Analytics." pith.science (2026). https://pith.science/paper/XWRMX4GM

@misc{pith2026250110560,
  author       = {Pith},
  title        = {Pith review of: Picachv: Formally Verified Data Use Policy Enforcement for Secure Data Analytics},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/XWRMX4GM}},
  note         = {Machine review of arXiv:2501.10560}
}
read the original 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

Figures reproduced from arXiv: 2501.10560 by the authors.

Figure 2
Figure 2. The declassification rules p , op,ℓ −−→ p ′ for policy p. Well-formed policy. Specifically, because our policy focuses on declassification, policies must be ordered (in the sense of ⇝) in the descending way. This reflects a practical basis: policies often specify the operations required to make data disclosable rather than to restrict it further. As shown in Fig￾ure 3, a policy p is well-formed if it consists of a c… view at source ↗
Figure 3
Figure 3. The well-formedness property of policy p. Policy Composition. Policy composition is essential for sce￾narios where data from multiple sources converge. For in￾stance, consider a medical dataset combining patient data from hospitals located in different states, such as California and Texas, each governed by its distinct data use policies. In cases where researchers aim to analyze the socioeconomic factors affecting p… view at source ↗
Figure 1
Figure 1. The refined lattice flows-to rules ℓ O1 1 ⊑∗ ℓ O2 2 . We present the declassification rules in [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figures from the paper (12 more)
Figure 4
Figure 4. Figure 4: The composition rules for policy p. 4.3 Policy Expressiveness We argue that the declassification policies presented in this paper provide a practical abstraction, grounded in real-world scenarios. We provide three different privacy policy use cases to strengthen our ar…
Figure 5
Figure 5. Figure 5: The syntax for RAP . predicate ϕ. The aggregate operator γe|g|ϕ(q) is slightly more complex. It computes aggregates e, groups rows by g, and fil￾ters groups satisfying ϕ (i.e., the having clause). Additionally, it specifies lists of aggregate expressions e. Here, the g…
Figure 6
Figure 6. Figure 6: The relational model. Program trace. The program trace tr serves two purposes when performing expression evaluations which be introduced next. First, it ensures that all data undergoes the appropriate operations before being released by recording the history of operati…
Figure 7
Figure 7. Figure 7: Main expression evaluation rules for ⟨ tr,T ⟩ e −→ ⟨ tr′ , v ⟩ . value v along with an updated trace tr′ . To highlight expres￾sion evaluation that involves policy transformation, we define an auxiliary expression evaluation relation as follows. ⟨ tr,T ⟩ f,v −→ [PITH_…
Figure 8
Figure 8. Figure 8: Auxiliary rules for ⟨ tr,T ⟩ f,v −→ ⟨ tr′ , v ′ ⟩ that di￾rectly manipulates policy checks and transitions that are highlighted . a wide array of programming languages. Second, it is more practical and secure to establish a barrier between third-party code and PICACHV.…
Figure 9
Figure 9. Figure 9: Selected reduction rules for RAP . E(TrNone ℓ) = ℓ T = U ti∈E(t) (ti , op −→ ℓ)  E(TrSingle t,op, ℓ) = T T = U ti∈t E(ti)  E(TrMulti t,op, ℓ) = U t∈T (t , op −→ ℓ)  [PITH_FULL_IMAGE:figures/full_fig_p009_9.png]
Figure 11
Figure 11. Figure 11: Rules for the compatible relation ≈ Theorem 5.2 (Strict non-interference). If no declassifica￾tion is permitted, then our semantics enforces strict non￾interference. 6 Implementation In this section, we explain how the PICACHV runtime monitor operates and how policies…
Figure 12
Figure 12. Figure 12: The high-level query execution workflow where we put the query execution engine and [PITH_FULL_IMAGE:figures/full_fig_p010_12.png]
Figure 13
Figure 13. Figure 13: The query execution phase. Verifiability. The primary motivation for leveraging TEEs to host PICACHV is to provide verifiable guarantees for private data processing on the server side to external parties (data owners) who lack direct control over their data in the clo…
Figure 14
Figure 14. Figure 14: The result of the microbenchmark on each rela [PITH_FULL_IMAGE:figures/full_fig_p012_14.png]
Figure 15
Figure 15. Figure 15: The runtime overhead of TPC-H testbed of P [PITH_FULL_IMAGE:figures/full_fig_p013_15.png]
Figure 16
Figure 16. Figure 16: Detailed analysis on the project and aggregate operators in terms of the percentage of their sub-routines. these operators into their primitives and provide a cost break￾down in [PITH_FULL_IMAGE:figures/full_fig_p013_16.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

64 extracted references · 59 canonical work pages

  1. [1]

    https://www.kaggle

    analysis healthcare dataset — kaggle.com. https://www.kaggle. com/code/manarmohamed24/analysis-healthcare-dataset . [Ac- cessed 05-09-2024]

    work page 2024

  2. [2]

    https://www.kaggle.com/ code/donottalk/autoimmune-symptom

    autoimmune-symptom — kaggle.com. https://www.kaggle.com/ code/donottalk/autoimmune-symptom. [Accessed 03-09-2024]

    work page 2024

  3. [3]

    https://www.kaggle.com/datasets/flaredown/ flaredown-autoimmune-symptom-tracker/data

    Chronic illness: symptoms, treatments and triggers — kag- gle.com. https://www.kaggle.com/datasets/flaredown/ flaredown-autoimmune-symptom-tracker/data . [Accessed 02-09-2024]

    work page 2024

  4. [4]

    https://www.kaggle.com/code/dzmitryashkinadze/ flaredown-autoimmune-symptoms-prediction

    Flaredown Autoimmune Symptoms Prediction — kag- gle.com. https://www.kaggle.com/code/dzmitryashkinadze/ flaredown-autoimmune-symptoms-prediction . [Accessed 05-09-2024]

    work page 2024

  5. [5]

    https://www.kaggle.com/code/ultron2412/ flaredown-data-exploratory-analysis#Symptoms

    Flaredown Data Exploratory Analysis — kag- gle.com. https://www.kaggle.com/code/ultron2412/ flaredown-data-exploratory-analysis#Symptoms . [Accessed 05-09-2024]

    work page 2024

  6. [6]

    https: //github.com/electrum/tpch-dbgen

    GitHub - electrum/tpch-dbgen: TPC-H dbgen — github.com. https: //github.com/electrum/tpch-dbgen. [Accessed 12-08-2024]

    work page 2024

  7. [7]

    https://www.kaggle

    Health Care Data Analysis — kaggle.com. https://www.kaggle. com/code/vinod123kumar/health-care-data-analysis . [Ac- cessed 05-09-2024]

    work page 2024

  8. [8]

    https://www.kaggle.com/ datasets/prasad22/healthcare-dataset/data

    Healthcare Dataset — kaggle.com. https://www.kaggle.com/ datasets/prasad22/healthcare-dataset/data. [Accessed 02-09- 2024]

    work page 2024

Show all 64 references
  1. [9]

    https://pola.rs

    Polars. https://pola.rs. Accessed: 2023-07-03

    2023

  2. [10]

    https://www.tpc.org/tpch

    The tpc-h benchmark. https://www.tpc.org/tpch. Accessed: 2023- 07-16

    2023

  3. [11]

    https://www.kaggle.com/code/muhammadfurqan0/ unlocking-healthcare-trends-data-analysis

    Unlocking Healthcare Trends: Data Analysis — kag- gle.com. https://www.kaggle.com/code/muhammadfurqan0/ unlocking-healthcare-trends-data-analysis . [Accessed 05-09-2024]

    2024

  4. [12]

    Expressive declassification policies and modular static enforcement

    Anindya Banerjee, David A Naumann, and Stan Rosenberg. Expressive declassification policies and modular static enforcement. In 2008 IEEE Symposium on Security and Privacy (SP’08), pages 339–353. IEEE, 2008

    2008

  5. [13]

    Contextual and granular policy enforcement in database-backed appli- cations

    Abhishek Bichhawat, Matt Fredrikson, Jean Yang, and Akash Trehan. Contextual and granular policy enforcement in database-backed appli- cations. In Proceedings of the 15th ACM Asia Conference on Computer and Communications Security (AsiaCCS’20), pages 432–444, 2020

    2020

  6. [14]

    Disclosure avoidance for the 2020 census: An introduction, 2021

    US Census Bureau. Disclosure avoidance for the 2020 census: An introduction, 2021

    2020

  7. [15]

    Nonmalleable in- formation flow control

    Ethan Cecchetti, Andrew C Myers, and Owen Arden. Nonmalleable in- formation flow control. In Proceedings of the 2017 ACM SIGSAC Con- ference on Computer and Communications Security(CCS’17), pages 1875–1891, 2017

    2017

  8. [16]

    Intel tdx demystified: A top-down approach

    Pau-Chen Cheng, Wojciech Ozga, Enriquillo Valdez, Salman Ahmed, Zhongshu Gu, Hani Jamjoom, Hubertus Franke, and James Bottomley. Intel tdx demystified: A top-down approach. ACM Computing Surveys, 56(9):1–33, 2024

    2024

  9. [17]

    Static checking of dynamically − varying security policies in database −backed applications

    Adam Chlipala. Static checking of dynamically − varying security policies in database −backed applications. In 9th USENIX Symposium on Operating Systems Design and Implementation (OSDI’ 10), 2010

    2010

  10. [18]

    Myers, Xin Qi, K

    Stephen Chong, Jed Liu, Andrew C. Myers, Xin Qi, K. Vikram, Lan- tian Zheng, and Xin Zheng. Secure web applications via automatic partitioning. In Proceedings of Twenty-First ACM SIGOPS Symposium on Operating Systems Principles, SOSP ’07, page 31–44, New York, NY , USA, 2007. ...

    2007

  11. [19]

    Security policies for downgrad- ing

    Stephen Chong and Andrew C Myers. Security policies for downgrad- ing. In Proceedings of the 11th ACM conference on Computer and communications security (CCS’04), pages 198–209, 2004

    2004

  12. [20]

    Intel sgx explained

    Victor Costan and Srinivas Devadas. Intel sgx explained. Cryptology ePrint Archive, 2016

    2016

  13. [21]

    Differential privacy

    Cynthia Dwork. Differential privacy. In International colloquium on automata, languages, and programming, pages 1–12. Springer, 2006

    2006

  14. [22]

    Confidential federated computations

    Hubert Eichner, Daniel Ramage, Kallista Bonawitz, Dzmitry Huba, Tiziano Santoro, Brett McLarnon, Timon Van Overveldt, Nova Fallen, Peter Kairouz, Albert Cheu, et al. Confidential federated computations. arXiv preprint arXiv:2404.10764, 2024

    2024 arXiv

  15. [23]

    Rulekeeper: Gdpr-aware personal data compliance for web frameworks

    Mafalda Ferreira, Tiago Brito, José Fragoso Santos, and Nuno Santos. Rulekeeper: Gdpr-aware personal data compliance for web frameworks. In 2023 IEEE Symposium on Security and Privacy (SP’23), pages 1014–

    2023

  16. [24]

    Snakes on a plan: Compil- ing python functions into plain sql queries

    Tim Fischer, Denis Hirn, and Torsten Grust. Snakes on a plan: Compil- ing python functions into plain sql queries. In Proceedings of the 2022 International Conference on Management of Data, pages 2389–2392, 2022

    2022

  17. [25]

    Goldstein and Veda C

    Robert C. Goldstein and Veda C. Storey. Materialization [database design]. IEEE Transactions on Knowledge and Data Engineering , 6(5):835–842, 1994

    1994

  18. [26]

    A formal semantics of sql queries, its validation, and applications

    Paolo Guagliardo and Leonid Libkin. A formal semantics of sql queries, its validation, and applications. Proceedings of the VLDB Endowment, 11(1):27–39, 2017

    2017

  19. [27]

    Information-flow control for database-backed appli- cations

    Marco Guarnieri, Musard Balliu, Daniel Schoepe, David Basin, and Andrei Sabelfeld. Information-flow control for database-backed appli- cations. In 2019 IEEE European Symposium on Security and Privacy (EuroS&P), pages 79–94. IEEE, 2019

    2019

  20. [28]

    Putting pan- das in a box

    Stefan Hagedorn, Steffen Kläbe, and Kai-Uwe Sattler. Putting pan- das in a box. In Conference on Innovative Data Systems Research (CIDR);(Online), page 15, 2021

    2021

  21. [29]

    Establishing browser security guarantees through formal shim verification

    Dongseok Jang, Zachary Tatlock, and Sorin Lerner. Establishing browser security guarantees through formal shim verification. In Pro- ceedings of the 21st USENIX Security Symposium (USENIX Security 12), pages 113–128, Bellevue, W A, August 2012. USENIX Association

    2012

  22. [30]

    Extending relational query processing with ml inference

    Konstantinos Karanasos, Matteo Interlandi, Doris Xin, Fotis Psallidas, Rathijit Sen, Kwanghyun Park, Ivan Popivanov, Supun Nakandal, Subru Krishnan, Markus Weimer, et al. Extending relational query processing with ml inference. arXiv preprint arXiv:1911.00231, 2019

    1911 arXiv

  23. [31]

    Laputa: Secure data analytics in apache spark with fine-grained pol- icy enforcement and isolated execution

    Byeongwook Kim, Jaewon Hur, Adil Ahmad, and Byoungyoung Lee. Laputa: Secure data analytics in apache spark with fine-grained pol- icy enforcement and isolated execution. In Network and Distributed Systems Security, 2025

    2025

  24. [32]

    Expressing information flow properties

    Elisavet Kozyri, Stephen Chong, Andrew C Myers, et al. Expressing information flow properties. Foundations and Trends® in Privacy and Security, 3(1):1–102, 2022

    2022

  25. [33]

    Mtcache: Trans- parent mid-tier database caching in sql server

    P-A Larson, Jonathan Goldstein, and Jingren Zhou. Mtcache: Trans- parent mid-tier database caching in sql server. In Proceedings. 20th International Conference on Data Engineering, pages 177–188. IEEE, 2004

    2004

  26. [34]

    Storm: refinement types for secure web applications

    Nico Lehmann, Rose Kunkel, Jordan Brown, Jean Yang, Niki Vazou, Nadia Polikarpova, Deian Stefan, and Ranjit Jhala. Storm: refinement types for secure web applications. InUSENIX Symposium on Operating Systems Design and Implementation (OSDI’ 21), 2021

    2021

  27. [35]

    Downgrading policies and relaxed noninterference

    Peng Li and Steve Zdancewic. Downgrading policies and relaxed noninterference. In Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL’05), pages 158–170, 2005

    2005

  28. [36]

    Formally verified memory protection for a commodity multi- processor hypervisor

    Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John Zhuang Hui. Formally verified memory protection for a commodity multi- processor hypervisor. In Proceedings of the 30th USENIX Security Symposium (USENIX Security 21), pages 3953–3970. USENIX Asso- ciation, August 2021

    2021

  29. [37]

    A secure and formally verified linux kvm hypervisor

    Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John Zhuang Hui. A secure and formally verified linux kvm hypervisor. In 2021 IEEE Symposium on Security and Privacy (SP’21) , pages 1782–1799, 2021

    2021

  30. [38]

    Squirrel: A scalable secure {Two-Party} computation frame- work for training gradient boosting decision tree

    Wen-jie Lu, Zhicong Huang, Qizhi Zhang, Yuchen Wang, and Cheng Hong. Squirrel: A scalable secure {Two-Party} computation frame- work for training gradient boosting decision tree. In 32nd USENIX Security Symposium (USENIX Security 23), pages 6435–6451, 2023

    2023

  31. [39]

    Toward a verified relational database management system

    Gregory Malecha, Greg Morrisett, Avraham Shinnar, and Ryan Wis- nesky. Toward a verified relational database management system. In Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL’10), pages 237–248, 2010

    2010

  32. [40]

    Towards auto- mated regulation analysis for effective privacy compliance

    Sunil Manandhar, Kapil Singh, and Adwait Nadkarni. Towards auto- mated regulation analysis for effective privacy compliance. In Network and Distributed System Security Symposium (NDSS’24), pages 631– 647, 2024

    2024

  33. [41]

    Towards multiverse databases

    Alana Marzoev, Lara Timbó Araújo, Malte Schwarzkopf, Samyukta Yagati, Eddie Kohler, Robert Morris, M Frans Kaashoek, and Sam Mad- den. Towards multiverse databases. In Proceedings of the Workshop on Hot Topics in Operating Systems (HotOS’19), pages 88–95, 2019

    2019

  34. [42]

    Qapla: Policy compliance for database-backed systems

    Aastha Mehta, Eslam Elnikety, Katura Harvey, Deepak Garg, and Peter Druschel. Qapla: Policy compliance for database-backed systems. In 26th USENIX Security Symposium (Sec’ 17), pages 1463–1479, 2017

    2017

  35. [43]

    The health insurance porta- bility and accountability act of 1996 (hipaa) privacy rule: implications for clinical research

    Rachel Nosowsky and Thomas J Giordano. The health insurance porta- bility and accountability act of 1996 (hipaa) privacy rule: implications for clinical research. Annu. Rev. Med., 57:575–590, 2006

    1996

  36. [44]

    all of us

    All of Us Research Program Investigators. The “all of us” research program. New England Journal of Medicine, 381(7):668–676, 2019

    2019

  37. [45]

    Language-based information- flow security

    Andrei Sabelfeld and Andrew C Myers. Language-based information- flow security. IEEE Journal on selected areas in communications , 21(1):5–19, 2003

    2003

  38. [46]

    Dimensions and principles of de- classification

    Andrei Sabelfeld and David Sands. Dimensions and principles of de- classification. In 18th IEEE Computer Security Foundations Workshop (CSFW’05), pages 255–269. IEEE, 2005

    2005

  39. [47]

    Selinq: tracking information across application-database boundaries

    Daniel Schoepe, Daniel Hedin, and Andrei Sabelfeld. Selinq: tracking information across application-database boundaries. In Proceedings of the 19th ACM SIGPLAN international conference on Functional programming (ICFP’14), pages 25–38, 2014

    2014

  40. [48]

    Ifdb: decentralized information flow control for databases

    David Schultz and Barbara Liskov. Ifdb: decentralized information flow control for databases. In Proceedings of the 8th ACM European Conference on Computer Systems (EuroSys’13), pages 43–56, 2013

    2013

  41. [49]

    Strengthening vm isolation with integrity protection and more

    AMD Sev-Snp. Strengthening vm isolation with integrity protection and more. White Paper, January, 53:1450–1465, 2020

    2020

  42. [50]

    Pytond: Efficient python data science on the shoulders of databases

    Hesam Shahrokhi, Amirali Kaboli, Mahdi Ghorbani, and Amir Shaikhha. Pytond: Efficient python data science on the shoulders of databases. In 2024 IEEE 40th International Conference on Data Engineering (ICDE), pages 423–435. IEEE, 2024

    2024

  43. [51]

    PrivGuard: Privacy regulation compliance made easier

    Lun Wang, Usmann Khan, Joseph Near, Qi Pang, Jithendaraa Sub- ramanian, Neel Somani, Peng Gao, Andrew Low, and Dawn Song. PrivGuard: Privacy regulation compliance made easier. In 31st USENIX Security Symposium (Sec’ 22), pages 3753–3770, 2022

    2022

  44. [52]

    Precise, dynamic information flow for database-backed applications

    Jean Yang, Travis Hance, Thomas H Austin, Armando Solar-Lezama, Cormac Flanagan, and Stephen Chong. Precise, dynamic information flow for database-backed applications. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’16)...

    2016

  45. [53]

    A language for automatically enforcing privacy policies

    Jean Yang, Kuat Yessenov, and Armando Solar-Lezama. A language for automatically enforcing privacy policies. In Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL’12), pages 85–96, 2012

    2012

  46. [54]

    Tensor relational algebra for distributed machine learning system design

    Binhang Yuan, Dimitrije Jankov, Jia Zou, Yuxin Tang, Daniel Bour- geois, and Chris Jermaine. Tensor relational algebra for distributed machine learning system design. Proceedings of the VLDB Endowment, 14(8), 2021

    2021

  47. [55]

    Spark: Cluster computing with working sets

    Matei Zaharia, Mosharaf Chowdhury, Michael J Franklin, Scott Shenker, and Ion Stoica. Spark: Cluster computing with working sets. In 2nd USENIX Workshop on Hot Topics in Cloud Computing (HotCloud 10), 2010

    2010

  48. [56]

    Access control for database applications: Beyond policy enforcement

    Wen Zhang, Aurojit Panda, and Scott Shenker. Access control for database applications: Beyond policy enforcement. In Proceedings of the 19th Workshop on Hot Topics in Operating Systems, HOTOS ’23, page 223–230, New York, NY , USA, 2023. Association for Computing Machinery

    2023

  49. [57]

    Blockaid: Data access policy enforcement for web applications

    Wen Zhang, Eric Sheng, Michael Chang, Aurojit Panda, Mooly Sagiv, and Scott Shenker. Blockaid: Data access policy enforcement for web applications. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI’ 22), pages 701–718, 2022

    2022

  50. [58]

    Sectee: A software-based approach to secure enclave architecture using tee

    Shijun Zhao, Qianying Zhang, Yu Qin, Wei Feng, and Dengguo Feng. Sectee: A software-based approach to secure enclave architecture using tee. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, pages 1723–1740, 2019. A Proofs A.1 Proofs for...

    2019

  51. [60]

    People whose age > 89 must be generalized (Safe Harbor)

  52. [61]

    user_id should be removed (Safe Harbor)

  53. [62]

    Healthcare dataset [8]

    trackable_* should only be aggregated with one of MAX, MIN, SUM, COUNT , and size should be greater than 20 (NIH-like policy). Healthcare dataset [8]

  54. [63]

    name should be removed (Safe Harbor)

  55. [64]

    (Common aggregate requirements) Table 3: The dataset and its corresponding privacy policies used in case studies

    medical_condition must be aggregated with one of MAX, MIN, SUM, COUNT . (Common aggregate requirements) Table 3: The dataset and its corresponding privacy policies used in case studies

  56. [1031]

    IEEE Computer Society, 2022

    2022

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.