Isolation you can check, gaps we declare.
This page is written for people evaluating UltraFabric. It states the guarantee the system makes, who has to be trusted for it, what it does not cover yet, and how to report a problem. It claims no certification we do not hold.
The guarantee
A plan the verifier accepts returns only data the requester may see, and its result does not change when other tenants' data changes.
Identity
RS256 tokens verified at the gateway and again at the data node; tenant, clearance and roles come only from verified claims.
Trusted base
The verifier, the operator definitions and the node's token check. The optimizer, cache, gateway and internal jobs are not trusted.
Evidence
994,405 paired-database isolation checks with no failures; the core theorem proved in Lean 4.
What the guarantee covers
Stated precisely, because a security claim is only as useful as its boundary.
Covered
- Rows of other tenants never reach a result, an aggregate, a sort or a limit that decides what you see.
- Rows hidden by the access policy and fields above the requester's clearance are treated the same way.
- The guarantee holds whoever produced the plan: optimizer, plan cache, internal job or a hand-written client.
- Raw key-value access to collection rows is refused; rows are reachable only through verified plans.
- Error messages carry no hidden-row identifiers and no byte counts that depend on hidden rows.
Not yet covered
- Row-level policies: today tenant isolation is the access boundary; policies compiled on the node are the next protocol version.
- Index probes (vector, text, graph) are specified with per-tenant partitions but not built.
- Timing and resource-use side channels. They are entered in a declared-leakage register with mitigations; anything observable and absent from it is treated as a bug.
- Multi-node distribution: single node today; the distributed operators are specified, not built.
How the code is built and tested
Specified first
The system and plan language have written specifications with a proof-obligation register; every rule change must add its case.
Mutation gates
52 of 53 deliberate defects caught across five passes; the harness itself carries self-checks after planted defects went unnoticed once.
Dependency policy
Engine crates have no third-party dependencies and forbid unsafe code; hashing, checksums and encodings are written and tested in the project.
Network surface
The data node listens only on a Unix socket. Network clients reach it through the gateway, which verifies the token before connecting.
Audit
Verifier decisions are recorded with the plan's fingerprint; security-relevant events append to a per-tenant hash chain (anchoring planned).
Cleartext tokens
Tokens travel inside the PostgreSQL password message, so the gateway accepts them only over TLS or from the same machine.
Report a vulnerability
We would rather hear it from you than read it elsewhere.
How
Email [email protected] with steps to reproduce. We acknowledge within one working day, keep you informed, and credit you if you wish. Please do not test against systems you do not own; early-access databases are provided for exactly this.
What we promise
No legal action for good-faith research that stays within the systems provided, a fix or a documented mitigation before public disclosure, and an entry in the declared-leakage register when a channel cannot be closed.
Certifications: UltraFabric holds no SOC 2, ISO 27001 or similar certification yet. We will say so on this page when that changes, not before.
Read the technical model.
Definitions, what the verifier checks, and the known gaps in full.