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作为信息格的推广，为这类析取依赖性提供了形式化语义模型。本文旨在增进对数据库支持程序中析取依赖性的理解，并引入一个实用框架以静态实施析取安全策略。为此，我们提出了确定性Quantale——一种基于查询的新结构，用于捕捉数据库中析取信息的序关系。该结构可视为信息Quantale的查询对应物。基于此结构，我们设计了一个可靠的验证机制，用于检查数据库支持程序的析取策略。该机制通过为带有数据库查询的简单命令式语言建立基于类型的分析实现，既能灵活适配多种行级和列级数据库策略，又能追踪控制流导致的析取关系。我们通过工具DiVerT实现了该机制，并在多个用例上验证了其可行性。