Existence is a leak.

Access control, as usually practiced, guards the contents of things. Can this user read that record, edit that row, open that file. Answer correctly and the secrets are safe. Except contents are not the only thing a system discloses. Sometimes the damaging bit is not what a record says but that the record exists at all.

The cheapest version of the attack is a naming collision. Try to create something with a guessed name. If the system says "already exists," it has just confirmed the existence of an object you were never cleared to see, through an error message that touched no data. The pattern generalizes: search results that count what they will not show, timing that differs between "denied" and "not found," an ID sequence with a conspicuous gap. In a multi-level system, where one identity may hold some compartments and not others, every one of these is a covert channel from the compartments you are outside of.

What makes this problem nasty is that it lives in the corners. No feature test writes assertions about the error message a wrong user gets when creating a duplicate name in a compartment they cannot see. The channel sits in exactly the code paths a test suite treats as uninteresting failure cases.

Closing it, provably

In n0de, our verified access engine, existence is treated as data. The design answer is polyinstantiation: names are scoped so that what you can collide with is exactly what you are cleared to observe, and a creation attempt from outside a compartment learns nothing from the outcome. The stronger statement is how that property is held: not by a test that probes a few names, but by a machine-checked proof, with the naive shared-namespace leak formalized as the motivating counterexample. Non-interference gives the general form, activity inside a compartment provably cannot change what an outside observer sees, and observation includes errors, collisions, and counts.

This is the kind of property that justifies the cost of proof. It is quantified over all names and all traces, precisely where testing thins out and where an assertion like "cannot" has to mean cannot. It is one instance of the general habit we keep arguing for: match the strength of the guarantee to the cost of being wrong. For most of a system, tests earn their keep. For the channel that leaks the existence of what you are sworn to protect, we want a theorem.