Formal methods for SQL RBAC: design and kernel implementation

[jasonhernandez]

EXPERIMENTAL

Motivation

The RBAC implementation in src/sql/src/rbac.rs is security-critical but verified almost entirely by example. The authorization policy is embedded in ~1,200 lines of pattern matching with no separate specification, making it difficult to review as a policy, impossible to tell omissions from deliberate decisions, and prone to divergence between multiple implementations of the same predicates.

This change introduces a formal methods framework to address these issues systematically, starting with the lowest-cost, highest-value steps: writing the policy down as reviewable data and building a verified kernel for the decision procedure.

Description

This PR implements the first two layers of a four-layer formal methods ladder for RBAC:

Layer 0a: Policy as data

• Adds RbacRequirementsDescription, a public owned type that describes what a plan requires, separate from the internal RbacRequirements representation
• Exposes describe_rbac_requirements() to dump the policy table as data, enabling review and assertion
• Adds a datadriven test harness (src/adapter/tests/rbac.rs) that renders requirements in human-readable form
• Includes initial test cases in src/adapter/tests/testdata/rbac demonstrating the policy for common statements

Layer 1: Verified kernel

• Adds src/sql/src/rbac/kernel.rs with integer-encoded implementations of role membership closure
• Implements membership_closure() as a fixpoint over machine words (bounded model checking friendly)
• Provides encode_membership() to convert catalog role graphs to the integer encoding
• Includes membership_closure_reference() as a set-based reference implementation
• Adds property-based tests verifying the encoded kernel matches the reference implementation on arbitrary graphs, including cyclic ones (property P4)

Key design decisions:

• The kernel uses single-word (u64) bitmasks to represent role sets, enabling bounded model checking with a practical bound (MAX_ROLES = 64). Graphs larger than this are reported as unanalyzable rather than truncated, preserving safety.
• The policy description type is deliberately separate from the internal representation, so the interface is stable even as implementation details change.
• The datadriven test format makes policy changes visible as diffs in the same PR that causes them, enabling review of the policy as a policy rather than as code.
• Property-based testing of the kernel against the reference implementation catches divergences automatically.

Verification

• New property-based tests in src/sql/src/rbac/kernel.rs verify closure correctness on arbitrary membership graphs
• New datadriven tests in src/adapter/tests/rbac.rs render the policy table for representative statements
• All tests pass with cargo test -p mz-sql and cargo test -p mz-adapter --test rbac
• The kernel implementation is total on all inputs (including cyclic graphs) and terminates by construction