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.

翻译：在指定数据库的安全策略时，通常需要表述析取依赖关系，即一条信息最多依赖于两个依赖P1或P2中的一个，但不能同时依赖两者。Hunt和Sands最近引入了一种形式化的析取依赖语义模型——信息量子格（Quantale of Information），作为信息格（Lattice of Information）的推广。本文旨在增进对数据库支持的程序中析取依赖的理解，并提出一个实用框架来静态强制执行析取安全策略。为此，我们引入了确定量子格（Determinacy Quantale），这是一种基于查询的新结构，能够捕捉数据库中析取信息的排序关系。该结构可理解为信息量子格的查询对应物。基于这一结构，我们设计了一个可靠的强制执行机制，用于检查数据库支持的程序中的析取策略。该机制基于对一种带有数据库查询的简单命令式语言进行类型分析，其精确性足以灵活适应多种行级和列级数据库策略，同时跟踪由控制流引起的析取。我们通过工具DiVerT实现了该机制，并在多个用例上验证了其可行性。