Capability Safety as Datalog: A Foundational Equivalence

TL;DR

This paper proves that capability safety can be exactly represented using propositional Datalog, enabling new algorithmic and structural results for security analysis.

Contribution

It establishes a formal equivalence between capability safety and propositional Datalog evaluation, addressing key limitations in existing frameworks.

Findings

Capability safety admits an exact propositional Datalog representation.

This enables efficient incremental maintenance and decision procedures.

The equivalence is tight, matching capability hypergraphs exactly.

Abstract

We prove that capability safety admits an exact representation as propositional Datalog evaluation (Datalogprop: the monadic, ground, function-free fragment of first-order logic), enabling the transfer of algorithmic and structural results unavailable in the native formulation. This addresses two structural limitations of the capability hypergraph framework of Spera [2026]: the absence of efficient incremental maintenance, and the absence of a decision procedure for audit surface containment. The equivalence is tight: capability hypergraphs correspond to exactly this fragment, no more.