poc: security barrier views via security levels, with property-checked ordering

[jubrad]

Motivation

Self-contained: this branch carries the design doc, the mechanism, and the
verification, so the whole story reads in one place. It supersedes #38566, which
is the same mechanism without the design doc merged in. #38562 implements the
same SQL surface by a different mechanism and is the thing to compare against.

The exposure. Our RBAC documentation says SELECT on a view is what governs
access to it, which invites using a view as a row-level access control boundary.
The privilege half of that works. The optimizer half does not: a reader's
predicate crosses the view boundary and is evaluated against rows the view
excludes, and error messages embed the offending value, so
SELECT * FROM my_orders WHERE ssn::int > 0 exfiltrates another tenant's ssn
in one query. Materializing is not a workaround, because an index only applies
on the cluster holding it and a current_user view cannot be indexed at all.

Description

CREATE VIEW ... WITH (SECURITY BARRIER). A barrier view is inlined like any
other, so its body is still optimized jointly with the reader's query, and an
ordering constraint rather than an object boundary carries the guarantee.

Each predicate carries the security level it was introduced at. inline_views
raises the consumer's non-leakproof predicates a level before splicing a barrier
in; raising rather than assigning is what makes nested barriers compose. Three
seams enforce it: movement, where a levelled predicate may not sink below a
lower level nor be reported at a Get; derivation, where an equivalence
class is seeded only from leakproof or unconstrained predicates; and
ordering, where MapFilterProject sorts by level first.

MapFilterProject reuses the same Predicate type the mid-level plan uses
rather than introducing a second notion. level is declared before expr so the
derived Ord puts lower levels first, and one sort_predicates is the single
place evaluation order is decided.

Leakproof means infallible. We have no user-defined functions, so a builtin's
only value-dependent channel is the error it raises, and could_error already
answers that with a fail-safe, type-derived default. =, <, >, and AND
come out leakproof automatically, which is why the measured cost is nil.

Verification

Borrowing the ladder from #38186, whose Layers 0 and 1 apply almost unchanged.

Layer 0b, the failure mode is a type error. Predicate::level is private. It
can be read and it can be raised, and there is no operation that lowers it:
raise is the only assignment to that field in the tree. Losing a constraint
requires constructing a fresh predicate through Predicate::unconstrained, a
named call a reviewer can grep for, rather than an assignment that reads like
nothing. Same move as the Authorized<Plan> typestate that design proposes, and
it earns the same thing: monotonicity by construction rather than by review.

This is not decoration. There is no blanket From<MirScalarExpr>, so every one
of ~30 conversion sites had to state whether it was creating a new unconstrained
predicate or re-applying an existing one. That is how three real level-dropping
bugs surfaced, in into_map_filter_project, literal_constraints, and
canonicalize_mfp. A blanket conversion would have compiled all three silently,
and one of them made the mechanism look like it worked while levels were quietly
zero.

Layer 1, an executable specification.
src/expr/tests/test_security_levels.rs states the requirement once,
declaratively, as is_admissible, written from the intended semantics rather
than derived from sort_predicates, so the two are independent and can disagree.
Five properties over arbitrary predicate lists: sorting yields an admissible
order; it neither invents, drops, nor relabels; optimize re-establishes the
order after rebuilding the list; optimize never invents a level; and level
outranks position. Verified red before green — removing the level from the
sort key fails three of the five.

Layer 0a is already present: levels render in EXPLAIN when non-zero, and
security_barrier.slt is the golden that makes a change show up as a diff in the
PR that causes it.

Layer 2 (Kani on sort_predicates) is a reasonable follow-up and is not done
here. Layer 3 does not apply; the property is not temporal.

What remains unverified, in that design's Class C sense: that every fallible
predicate crossing a barrier gets raised. That is a property of
raise_security_level covering every place a predicate can live, and it is the
direct analogue of P9, the keystone lemma held up by convention.

Results

• 1768 sqllogictest assertions pass across the EXPLAIN corpus, privileges,
  joins, subqueries, and the barrier tests. bin/fmt and clippy clean.
• No text plan in the EXPLAIN corpus changes. Only the JSON goldens move,
  for the serialization shape, which implies an expression-cache format bump.
• The guarantee is pinned by physical plans over a table whose column order
  would otherwise schedule the reader's cast first:

plain   filter=((text_to_integer(#0{secret}) > 0) AND (#1{tenant} = "alice"))
barrier filter=((#1{tenant} = "alice") AND (text_to_integer(#0{secret}) > 0))

Both are fully inlined, so ordering is the only difference. A leakproof
predicate stays at level 0 and still reaches the source import.

Costs

Predicate is 104 bytes against MirScalarExpr's 96. The level reaches LIR and
the compute protocol, though the runtime does not need it: SafeMfpPlan already
evaluates in vector order, so the sort discharges the constraint. It crosses
because MapFilterProject is one generic type shared by both plan levels.

Unlike #38562, this mechanism generalizes to row-level security, which needs
exactly this per-predicate ordering and has no object boundary to hang a gate on.

🤖 Generated with Claude Code