Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Disjunctive Policies for Database-Backed Programs

Amir M. Ahmadian, Matvey Soloviev, Musard Balliu

TL;DR

This work addresses enforcing disjunctive security policies for database-backed programs by developing a semantic framework that models disjunctive dependencies and their security implications. It introduces the Determinacy Lattice (DL) and its extension, the Determinacy Quantale (DQ), to capture how query results may reveal information from one of several branches, and relates these to the Quantale of Information (QoI). The authors provide a type-based, path-sensitive dependency analysis and a query abstraction (symbolic tuples) that, together with a static enforcement mechanism, prove sound with respect to a knowledge-based security condition. The approach is implemented in a prototype tool, DiVerT, and evaluated on a suite of tests and practical use cases including privacy-preserving location, data publishing, secret sharing, and online item access. The framework unifies database security and information-flow perspectives and offers a scalable, sound method for enforcing complex disjunctive policies in real database-backed applications.

Abstract

When specifying security policies for databases, it is often natural to formulate disjunctive dependencies, where a piece of information may depend on at most one of two dependencies P1 or P2, but not both. A formal semantic model of such disjunctive dependencies, the Quantale of Information, was recently introduced by Hunt and Sands as a generalization of the Lattice of Information. In this paper, we seek to contribute to the understanding of disjunctive dependencies in database-backed programs and introduce a practical framework to statically enforce disjunctive security policies. To that end, we introduce the Determinacy Quantale, a new query-based structure which captures the ordering of disjunctive information in databases. This structure can be understood as a query-based counterpart to the Quantale of Information. Based on this structure, we design a sound enforcement mechanism to check disjunctive policies for database-backed programs. This mechanism is based on a type-based analysis for a simple imperative language with database queries, which is precise enough to accommodate a variety of row- and column-level database policies flexibly while keeping track of disjunctions due to control flow. We validate our mechanism by implementing it in a tool, DiVerT, and demonstrate its feasibility on a number of use cases.

Disjunctive Policies for Database-Backed Programs

TL;DR

This work addresses enforcing disjunctive security policies for database-backed programs by developing a semantic framework that models disjunctive dependencies and their security implications. It introduces the Determinacy Lattice (DL) and its extension, the Determinacy Quantale (DQ), to capture how query results may reveal information from one of several branches, and relates these to the Quantale of Information (QoI). The authors provide a type-based, path-sensitive dependency analysis and a query abstraction (symbolic tuples) that, together with a static enforcement mechanism, prove sound with respect to a knowledge-based security condition. The approach is implemented in a prototype tool, DiVerT, and evaluated on a suite of tests and practical use cases including privacy-preserving location, data publishing, secret sharing, and online item access. The framework unifies database security and information-flow perspectives and offers a scalable, sound method for enforcing complex disjunctive policies in real database-backed applications.

Abstract

When specifying security policies for databases, it is often natural to formulate disjunctive dependencies, where a piece of information may depend on at most one of two dependencies P1 or P2, but not both. A formal semantic model of such disjunctive dependencies, the Quantale of Information, was recently introduced by Hunt and Sands as a generalization of the Lattice of Information. In this paper, we seek to contribute to the understanding of disjunctive dependencies in database-backed programs and introduce a practical framework to statically enforce disjunctive security policies. To that end, we introduce the Determinacy Quantale, a new query-based structure which captures the ordering of disjunctive information in databases. This structure can be understood as a query-based counterpart to the Quantale of Information. Based on this structure, we design a sound enforcement mechanism to check disjunctive policies for database-backed programs. This mechanism is based on a type-based analysis for a simple imperative language with database queries, which is precise enough to accommodate a variety of row- and column-level database policies flexibly while keeping track of disjunctions due to control flow. We validate our mechanism by implementing it in a tool, DiVerT, and demonstrate its feasibility on a number of use cases.
Paper Structure (32 sections, 25 theorems, 50 equations, 12 figures)

This paper contains 32 sections, 25 theorems, 50 equations, 12 figures.

Table of Contents

  1. Introduction
  2. Background
  3. Lattice of Information
  4. Quantale of Information
  5. Information Ordering in Databases
  6. A Primer on Relational Database Models
  7. Determinacy Lattice
  8. Determinacy Quantale
  9. Security Framework
  10. Language
  11. Security Model
  12. Enforcement of Disjunctive Policies
  13. Conjunctive Queries
  14. Type-based Dependency Analysis
  15. Query Abstraction
  16. ...and 17 more sections

Key Result

Lemma 1

For all $\mathcal{Q}$, there is a complete lattice homomorphism from the Determinacy Lattice $DL(\mathcal{Q})$ to the Lattice of In-formation defined on $\{{Q}_{\sim} \mid Q \in DL(\mathcal{Q})\}$.

Figures (12)

  • Figure 1: Some equivalence relations on $\{-2,-1 ,0, 1 , 2 , 3 \}$
  • Figure 2: Database schema for employees and managers
  • Figure 3: Table $t$
  • Figure 4: A portion of the DQ for queries q1, q2, v1, v2
  • Figure 5: Language syntax
  • ...and 7 more figures

Theorems & Definitions (65)

  • Example 1
  • Example 2
  • Definition 1
  • Example 3
  • Definition 2
  • Definition 3
  • Definition 4
  • Lemma 1
  • Definition 5
  • Definition 6
  • ...and 55 more