Skip to content
Logo

Capability confinement — what a bounded subset actually buys

The strongest claim available here is capability confinement, not proof of security. The first is demonstrable today. The second overreaches in a way a hostile reader will find in about five minutes, and this page is written to survive that reader.

The problem is that the TCB is not enumerable

A client application on this protocol handles keys, signs commits, and talks to enclaves. Its trusted computing base should be something you can list.

In an unbounded framework it isn't. A component can reach window, localStorage, navigator or fetch from inside a render body by ambient reference — no import, no injection, nothing at the call site to notice. Which of them a given component actually touched is not answerable by reading the type, and generally not answerable without running it.

That is not a criticism of React. It is what "unbounded" means, and it is the reason ⟦E⟧ = F needs a middle term at all.

In freact it is enumerable, and the enumeration is in the checker

freact-check is a decision procedure: a file is in the subset if and only if it exits 0. Every rule is stated against the capability it withholds, and the withheld sets are literal, closed sets in the source of the checker:

const HOOK_EFFECT = new Set(['useEffect', 'useLayoutEffect', 'useInsertionEffect'])
const HOOK_REF    = new Set(['useRef', 'useImperativeHandle'])
const DOM_GLOBALS = new Set(['document', 'window', 'globalThis',
                             'navigator', 'localStorage', 'sessionStorage'])
const TIMERS      = new Set(['setTimeout', 'setInterval',
                             'requestAnimationFrame', 'queueMicrotask', 'fetch'])
const VIEW_CALLS  = new Set(['t','cls','style','h','scalar','field','when','each','testid'])

A mechanically checkable statement about what a component can do is a different and much stronger artifact than a human having read the diff.

The second half is what makes it more than hygiene

The capabilities are not deleted. They are relocated to a closed effect algebra. So the client's authority stops being "whatever the ambient environment exposes" and becomes an enumerable list of Eff constructors — a manifest of what this app can do, derived from the source rather than written by hand.

That manifest is small enough to print. Today Eff has twelve constructors:

setConst · setInput · pushDraft · pushInput · setFromRow · setFromScalar
pushInputWith · routeIfHex64 · lookupRoute · appendFromScalars
appendFromScalarsIfAbsent · setUniqueFromScalar

Every one writes Doc. Set a scalar, push a row, route. Not one names a host capability — no clipboard, no storage, no network, no timer, no device. A view layer built from these can be read off as: this app's UI can change its own state and nothing else.

That is the security story, and it is a measured fact rather than an aspiration.

Reactivity is not the unbounded part

A recurring confusion worth settling: reactivity is formalizable, and here it is formalized. Doc is typed state, the view is a pure function of it, and transitions are named Eff constructors. That is a reactive system with a denotation — useState is not hard to formalize because it reacts to state.

What is unbounded is not the reaction. It is what the reacting code is allowed to do: a hook may run any effect at any time, close over any mutable value, and reach any ambient global. The bound is on capability and on serializability (Doc scalars are typed Atoms), not on reactivity itself.

Two places this must stay honest

"Formalized" does not mean "secure"

The subset bounds capability. It does not prove the key handling is correct. encapp's proven core is real but small and specific — refinement, replay idempotence, permutation of ordered lists. And the bridge is not finished:

node tools/freact-check.mjs --summary --max 0 \
  ../impl-super/sdk/emulator/{freact-tree,tree-pure,index,registry}.ts   # 0 — enforced
 
node tools/freact-check.mjs --summary ../impl-super/apps/web/src/superapp/
# 2323 constructs outside the subset

A gate not pointed at the code confines nothing. The subset is enforced at zero on four emulator files while the reference application sits at 2323 and falling. Any version of this argument that omits that number is refuted by the first person who runs the tool.

The escape hatch is the whole game

One Eff constructor meaning "run this arbitrary JS" reinstates every capability the subset excludes — and it would be invisible in a green build. Every rule above would still pass.

So "every addition carries a denotation, not just a name" stops being style advice and becomes the security invariant. It is the first thing a reviewer should check, and the reason the vocabulary is grown by attempting a value and having it fail to typecheck rather than by deciding what looks missing.

A theorem over an escape hatch is not a theorem.

Why this matters more as code volume grows

The sharp version of the agent argument is not "agents write insecure code."

It is that review capacity is the scarce resource, and machine-written volume grows faster than it. A decidable subset moves the security question from did someone notice to did the checker exit 0 — a property that scales with generated code instead of degrading under it.

For a crypto client specifically, that is the argument in one line: the boundary of what the UI layer can reach is a build artifact, not a review outcome.

Is any of this specific to React?

No. The core is renderer-agnostic: RView, Eff and Doc mention React only in doc-comment prose — not in a single type or constructor. And the shape is already carrying more than one target:

  • two style emitters from one Style type — CSS and React Native styles
  • three renderers consuming RView — the emulator's DOM renderer, freact, and the RN kit

So a fvue bridge would be the same construction with a different surface syntax: bound the framework's expression language to what has an image in RView/Eff/Doc, write the decision procedure, and grow the vocabulary by attempt-and-fail. That is a claim about structure and it is evidenced by the second emitter already existing — it is not a claim that the work is done, or that any particular framework bounds as cleanly as React's function components do.

What you must still trust — the complete list, and it is short

Theorems are conditionals: given these assumptions, this property holds of this model. So you get properties with named scopes, never "total security" — that would require the assumptions to be empty, and they never are.

The right claim is the stronger and truer one: formalization converts an open-ended question into an enumerable one. Without it, "what can this UI layer do?" has no answer short of reading everything. With it, the answer is a finite list — twelve Eff constructors — plus a named set of trusted components. The risk is not eliminated. It is made listable, and a list is auditable in a way that ambient authority never is.

Here is that list.

  1. freact-check is trusted, not proved. It is a JavaScript program with hand-written closed sets (DOM_GLOBALS, TIMERS, HOOK_EFFECT). If it misses a way to reach window, everything downstream inherits the miss. It is the TCB of the entire capability argument and it has no theorem about itself.
  2. The renderers are trusted. ⟦E⟧ = F relates two trees. A browser then interprets the result, and there is no formal model here of CSS layout, font metrics, or rasterization.
  3. The proof-to-artifact seam is partly proved and partly tested, and the distinction matters:
    • the style emitter's byte-identity is proved — 741 obligations of the form example : toCss [...] = "..." := by native_decide — but native_decide trusts the compiler's evaluator, introducing Lean.ofReduceBool. test/axiom-audit.mjs allows it by name, so it is a declared trusted axiom rather than a kernel-checked proof.
    • the whole-artifact fingerprint is a test, not a theorem.
  4. R ≡ F can never be a theorem. R is opaque by necessity, so that obligation permanently leaves the proof system and is discharged by the regression corpus.
  5. The classes the model does not address at all: key-handling correctness, supply chain, the Lean compiler, the browser, the machine.

Claim this as "here is the complete list of what you must still trust, and it is short." The other phrasing — "there is nothing left to trust" — invites a reader to find the thing you forgot, and there always is one.

Composing with a formalized protocol

The ENC protocol is itself specified in Lean (impl-spec/spec-lean, ~320 modules including Enc/Wire.lean and Enc/Oracle.lean). Having both sides formalized is the genuinely unusual part — most formal-methods stories cover one layer and hand-wave the boundary — because it means the boundary can be stated.

What composition buys that neither side has alone. A protocol proof says: given well-formed messages, the event-log semantics hold — ordering, replay, authorization. An app proof says: given Doc, the UI is a function of it and the app's authority is twelve constructors. Put together:

the set of messages this client can emit is finite and derived from source.

The protocol's guarantees are conditional on what it receives; the app's confinement is what bounds the sender. Without the app side, "given well-formed messages" is an assumption about an unbounded program.

Three seams composition does not close.

  • The interface must be the same object on both sides. A protocol theorem quantifies over its message type; an app theorem quantifies over Eff. Those are different Lean types today, and they do not meet: impl-encapp requires only impl-foundation, and nothing under Encapp/ imports Enc.*. Composition needs a proved mapping Eff → protocol message, or the two theorems are about different things and the chain does not join. Worth being paranoid about precisely because it looks like it should just work.
  • What the user authorizes is not what the app sends. The app can be confined and the protocol sound, and a signer can still approve a transaction they misread, because the pixels said one thing and the payload said another. pinned_perm is a fragment of exactly this property — a list cannot silently drop a row — which is why it is the most security-relevant theorem in the system. The general form, what was displayed corresponds to what was signed, needs the rendering chain, and that is where layout and rasterization sit unformalized. This is the seam a WYSIWYS attack lives in, and composing app-with-protocol does not touch it.
  • Trusted components stay trusted. Composition does not shrink the list above; it means the same list applies on both sides of the join.

The agent claim, stated so it survives review. Not "agents write insecure code." It is:

an agent writing client code cannot expand the app's authority, because authority is a closed constructor set checked at build time rather than a review outcome.

That is defensible about machine-written code. It is not "proved secure" — it is the capability surface an agent can reach is enumerable and enforced, and the protocol below it is proved sound given that surface.

And the honest addendum, which belongs in the same breath: ⟦E⟧ = F does not exist, F has not been produced, and the subset is enforced at zero on four emulator files while the reference app sits at 2323. The composition described here is a design that is reachable, not discharged.