Realtime Postgres Row Level Security

Realtime Postgres Row Level Security
supabase.com

Probably the main problem with RDBMS is also it's biggest benefit: you write code that naively looks some bad polynomial time, and then query planner does the magic and use indices. The problem is, of course, when the index doesn't exist or the query planner doesn't do a good job.

What would be nice is a way to mandate that queries must go through certain indices. But this is in fact good for row level security too!

Functional programming is deeply related to capability-based security, in that both try to get rid of all ambient authority and mediate all actions through some sort of reference. Rust, with it's many types of reference makes the relationship even clearer. From these vantage points, it is very natural to use data structure both to make things performant and enforce certain invariant.

Indices are the closes data structures in RDBMSs, because they do promote only certain access patterns. With the rule that queries must go through the indices, they enforce those access pattern, and thus we have the same proven tool. Combine them with views for filtering out data, (which we can think in conjunction with more indices of as sort of a curried indexes Map> even if they aren't implemented that way), and now we have very powerful tools for guaranteeing performance and security.

As an icing on the cake, I think enforcing limited access patterns could get us closer to that long-sought goal of a RMBDS that automatically knows how to distribute itself. The limited access patterns open up possible options, because we which of the pathological joins that every sharding possibility run into are no longer allowed. Reusing the same query planner tricks, "cardinality analysis" type stuff can be used to choose between those possibilities.

Here's a worked out concrete example:

Tables:

   User: { k: UserID PK, t: TennentId, n: Name, isAdmin: Bool },
   Todo: { k: TodoID PK, u: UserID, d: Date, m: Msg } 

# exists_classical means proof of existence but we don't care which.

    Map
    Map

# exists_constructive means need to show existence and we do see what item witness it

    Map>

    Map>

1. When we do a comprehension syntax, we are "returning the whole table" i.e. an unconstrained view that can be queried in an arbitrary way. A joined table has to be joined in the given way, but is otherwise unconstrained.

2. exist_constructive is the same as a { ... } comprehension, but the cardinality must be 1 as proven by the unique constraints. exists_classical is a comprehension for an arbitrary number of stuff, that is then truncated in the type theory sense. https://xenaproject.wordpress.com/2021/05/19/the-trace-of-an... is a good discussion of an example of this truncation.

3. Normally one puts the TennentID on every table, even though it is denormalizing. Now the access patterns enforce this.

Clearly this is a few PhD theses away from actually existing :), but all the embryonic theory comes from good well-established things, which makes me confident.