Secrets as a Flow Property: Capability-Bound Secrets With Static Confinement and a Cross-Backend Value Registry

Pitch

A provider key can be confined, by a flow rule with no declassifier whose core statements are proved in Lean over an abstract model, to the emissions of one capability, and the honest cost of that claim, including the type guarantee the design note had to retract, is itself the result.

Abstract

Agent systems hand a provider key to exactly one call and then rely on discipline to keep it out of logs, prompts, tool returns and traces. We describe the secret machinery in revl, a typed language for capability-scoped agent programs. A top-level secret NAME for CAPABILITY declaration binds a value, supplied by the driver at run time and never present in the source or the manifest, into the extern bodies of one capability. The design note for the feature describes an adversarial review that retracted its first claim: the bound key lives in opaque host code, so no revl type can forbid its use there, and the guarantee is a flow guarantee over two disjoint origins, secret (the bound key, no declassifier, refused at every crossing kind) and confidential (the Secret[T] value qualifier, admitted only at a declared receiver and downgraded only at a declared endorse). We state three Lean theorems for the rule (secret_persists, secret_confined, confidential_needs_declassification) and the explicit gap between that model and the code. For values that escape the static rule, five backends carry a registry that scrubs registered values and their escaped renderings, and the wasm tier refuses at its one framing site. The trace funnel covers python, typescript and go; the roadmap states that java, rust and wasm are out of scope for it, and that the provider's return value channel has no funnel on any tier. We report the defect series that building the registry across backends exposed. We have no leak-rate measurement yet; we list the experiment that would supply one.

Problem and claim

Existing secret handling falls in two camps. Secret managers and injected-credential agents control where a value is stored and delivered, and say nothing about where the process then sends it. Wrapper types (a Secret<T> newtype, Java's SecretKey) forbid reading in the host language but do not cross a language boundary or a serialization boundary, and an agent system crosses both constantly: into a model prompt, an MCP tool return, a write-ahead log, a console trace.

The claim is narrow and the design note insists on narrowness. No revl construct and no declared boundary crossing can carry a capability-bound key out of its capability's extern bodies (docs/design/256-capability-bound-secrets.md:76-107). It does not claim the process cannot send the key: a host body that splices the key into its own outbound request is outside revl's reasoning (the note's attack A3, status "CRITICAL, OPEN", line 796). The paper's contribution is the precise boundary of the guarantee, the disjointness argument that makes it sound, and the runtime registry that covers what the static rule cannot see.

A second claim is methodological. The first draft of the note asserted a no-eliminator Secret type for the bound key. Review showed this was vacuous because the checker never descends into host-body text (lines 38-54 and 215-243 of the note). The revision removed the mechanism and rebuilt the claim on flow alone. We present the retraction as a result: it is a concrete case of a type-level secret guarantee that does not exist when the secret is held in an untyped host scope.

Contributions

1. A declaration surface (secret NAME for CAPABILITY, a contextual keyword) with plug-time injection into one capability's extern bodies, fail-loud when the value is absent, name-only in the audit table, with a documented rotation seam (docs/design/256-capability-bound-secrets.md:159-215, docs/design/256-capability-bound-secrets.md:281-365).
2. Two disjoint origins, secret and confidential, so that a permissive receiver rule for Secret[T] is unreachable by the bound key. The note identifies the earlier single-token design as a critical flaw and gives the exploit (docs/design/256-capability-bound-secrets.md:23-36, attack A8 at line 878).
3. A per-crossing-kind refusal list (emit, plain extern call, unnameable callable, provide-method return, nested value) with a reach-completeness row in the test suite that fails if a crossing kind is added without the raise (docs/design/256-capability-bound-secrets.md:414-497, tests/test_reach_completeness.py:265-285).
4. Three Lean statements for the rule, with a non-vacuity witness showing the label algebra can clear a secret, so the theorem holds because of two explicit refusals (formal/RevL/Theorems/G9_NoAuthorityFromUntrusted.lean:55-64, formal/RevL/Theorems/G9_NoAuthorityFromUntrusted.lean:212-258), and a stated gap between the Lean model and the runtime registry (formal/STATUS.md:57).
5. A cross-backend value registry: leaf registration at the door a declared secret enters through, scrub of the escaped renderings (raw, JSON-escaped, repr-escaped), and a funnel at the host trace choke point (python, typescript, go); plus a catalogue of the defects found while porting it (roadmap item 421, F6 series).

Related work

The novelty is in the combination and in the honest accounting, not in a new label calculus. The Lean model is a rule-level statement over an abstract flow and adds less than a noninterference result; it should not be oversold.

Evidence on main

Numbers that exist

• Test counts by static grep of def test_ (not executed): tests/test_secret_flow.py 31, tests/test_secret_bound.py 30, tests/test_seam_leak_gaps_815.py 14, tests/test_tier_host_trace_secret_421_f6.py 8, go registry 19, java registry 32, rust registry 27, wasm leaf sinks 8, ts bound 6. These are counts of tests, not results.
• The roadmap lists a lettered defect series for the registry and its walks, F6(c) to F6(r) in item 421 (docs/v2.0-roadmap.md rows near 1587-1606): console bypass, escaped renderings, container faces, bytes faces, rust build defect, java bytes, rust leaves, cyclic walks on py, ts, java, go depth cap, map keys, variant payloads, and the Opt-is-not-indirection boxing defect (F6(k)). The letter range F6(c) to F6(r) holds 16 entries; how many of them count as registry-walk defects was not recounted.
• No leak-rate, overhead or false-scrub measurement exists. The minimum markable length (4) and minimum matchable argument length (3) are design constants (backends/python/confidential.py:65, backends/python/confidential.py:80), not measured.

Paper outline

1. Introduction: the provider key problem in an agent process; what is and is not claimed.
2. Threat model: host-body opacity (G8), the three sinks that matter (model context, durable file, tool return).
3. Design: declaration, injection, two origins, crossing-kind raises, no declassifier.
4. The retraction: why the no-eliminator type was vacuous (note lines 38-54) and the A8 exploit that forced disjoint origins.
5. Formalisation: the three theorems, the non-vacuity witness, the stated gap.
6. The registry: leaf registration, renderings, the single funnel, bounded matching; wasm as a refusal.
7. Evaluation (to be done): canary matrix, mutant study, expressiveness cost.
8. What the defect series teaches (short; the bug-class argument belongs to the reach-completeness paper).
9. Limits and related work.

Threats to validity and limits

• The note's own words: the guarantee is "no revl construct and no declared crossing carries the secret out", never "the process cannot send the key" (docs/design/256-capability-bound-secrets.md:104-107). Attack A3 is open.
• Exact-match scrubbing misses a value the host reformats (truncation, case fold, a %.2f); redact_call_text says so itself (backends/python/confidential.py docstring at line 661).
• The note says the secret raise lives in a flow analysis whose walk coverage is a separate obligation; formal/RevL/Theorems/G9_NoAuthorityFromUntrusted.lean:73 states that path coverage is not proved.
• The registry is per process and short values are not registered, so a short secret depends on positional marking alone.
• The note's header says its status section is stale in places; every status claim here was checked against code, not the note. The funnel lives in backends/python/confidential.py and src/revl/_process_runner.py.
• The trace funnel covers three tiers and the value channel none; a go host body that panics is a residual outside every funnel.
• The defect series was found by the authors and is not independent evidence. An outside red-team on the registry would strengthen it.

Fact-check

Claims in this draft were checked against revl main at commit 45bec431f: 45 checked, 10 corrected.

Cite this draft

@misc{revlp37,
  author       = {Thomas Moussajee},
  title        = {Secrets as a Flow Property: Capability-Bound Secrets With Static Confinement and a Cross-Backend Value Registry},
  year         = {2026},
  howpublished = {\url{https://inso1337.github.io/revl/research/P37.html}},
  note         = {Research draft, not peer reviewed. Written against revl commit 45bec431f. Licensed CC BY 4.0.}
}

Text licensed CC BY 4.0, author Thomas Moussajee.