Skip to content

Commit b6dfa58

Browse files
committed
spec: flow hardening + ratification asks; NEW trust.md (PROPOSED)
flow.md: implicit-channel closures enumerated, TACIT prior art, three asks (label lattice, refuse-by-default export, grant scoping). trust.md: trust record {origin, authority, exposure}, the pairing rule, postures (workbench/reviewed/hardened, non-transitive), trust profiles + harden op, the integrity dual, sandboxed-interpreter dividend, security-as-an-axis. Prototype-backed; nothing conformance surface until ratified.
1 parent f173406 commit b6dfa58

2 files changed

Lines changed: 371 additions & 12 deletions

File tree

‎spec/flow.md‎

Lines changed: 101 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
# Classified flow — capability-style non-exfiltration over the artifact
22

3+
> Secrecy is one of two dual flow modes; the integrity dual (prompt
4+
> injection: untrusted data must not steer power) and the trust
5+
> record/postures live in `spec/trust.md`. One walker serves both.
6+
37
**Status: PROPOSED (2026-08-10), awaiting ratification.** Nothing here is
48
conformance surface yet: no harness op, no fixtures, no schema change. A
59
working reference prototype exists (`reference/flow.py` +
@@ -65,16 +69,61 @@ LM's completion derives from its prompt). Output of a declassifier is
6569
clean.
6670

6771
**Honest limits (stated, not hidden):** the prototype tracks *explicit*
68-
data flow plus loop-to-fixpoint; **implicit flows** (branching on a
69-
tainted test, then signaling through untainted assignments) are flagged
70-
only coarsely — a tainted `If`/`While` test inside which a sink is
71-
called is reported as a `control` violation, but value laundering
72-
through control flow is not fully closed. This is a lint with teeth,
73-
not a proof system — the gap between "declared and machine-checked
74-
across the whole orchestration layer" and Scala's capture-checked
75-
leaves. The leaf boundary stays trust-by-declaration (`effects: pure`
76-
is probe-verified, not type-proven; spec/node-set.md's standing
77-
position).
72+
data flow plus loop-to-fixpoint, and closes the branch-shaped implicit
73+
channels the closed node set makes enumerable:
74+
75+
- **branch-assign laundering** (`if secret == k: y = "1" else: y =
76+
"2"`) — assignments under a tainted guard are tainted;
77+
- **the exception channel** — a `Raise` under a tainted guard taints
78+
every enclosing handler's assignments;
79+
- **the break channel** — a `Break`/`Continue` under a tainted guard
80+
taints the loop's assignments (guarded re-walk to fixpoint);
81+
- a sink *called* under a tainted test with clean args is a `control`
82+
violation.
83+
84+
What remains open, by design: **sink-selection signaling** (which of
85+
two lawful sinks fires encodes the bit — reported only as the coarse
86+
`control` violation), **iteration-count channels** into out-of-band
87+
observers, and timing/covert channels generally. This is a lint with
88+
teeth, not a proof system — the gap between "declared and
89+
machine-checked across the whole orchestration layer" and Scala's
90+
capture-checked leaves. The leaf boundary stays trust-by-declaration
91+
(`effects: pure` is probe-verified, not type-proven;
92+
spec/node-set.md's standing position).
93+
94+
## Prior art: TACIT / tracked capabilities (Odersky et al., CAIS 2026)
95+
96+
The design's inspiration is now a published system: *Securing Agents
97+
with Tracked Capabilities* (Odersky, Zhao, Xu, Bračevac, Pham; TACIT
98+
harness; best paper, CAIS 2026; substack: "Tracked Capabilities for
99+
Safer Agents"). Correspondences, recorded so ratification sees the map:
100+
101+
- their pure arrow `T -> U` ≈ our `effects: pure` + rung-0 placement —
102+
with one strengthening on our side: the "pure summarizing LLM" is a
103+
weights-baked entry whose manifest *has no endpoint*, a checkable
104+
file fact rather than an interface promise;
105+
- `Classified.transform(f: T -> U)` ≈ tainted data flowing only into
106+
non-sink leaves; `reveal(using CanAccess)` ≈ the receiver-held
107+
declassifier grant; `aggregate` ≈ the taint join (secret ⊔ x =
108+
secret), already in the prototype;
109+
- their "safe subset, escape hatches disabled" ≈ the closed node set
110+
refusing `import`/`lambda`/ambient context.
111+
112+
Two consequences adopted as open items:
113+
114+
1. **Their CaMeL critique** (dedicated DSL + whole-program-then-analyze
115+
vs on-the-fly checked snippets) does not reach the shipped-artifact
116+
case — a portable program is closed before analysis by premise — but
117+
it does reach CodeAct/PoT. The answer is theirs, transposed:
118+
model-generated snippets written in the exportable subset can be
119+
`node_compile`d + `flow_check`ed **per snippet, before the
120+
interpreter leaf executes them** — an incremental flow mode, named
121+
here as future work, not in this ratification.
122+
2. **Defense-in-depth gap:** TACIT grants are scoped to a computation;
123+
our declassifier grants are leaf-named but policy-global (every call
124+
of the granted leaf declassifies). A per-path or per-call-site grant
125+
scope is the faithful translation — added to the ratification asks
126+
below as question 3.
78127

79128
## Proposed conformance shape (on ratification, not before)
80129

@@ -84,5 +133,45 @@ position).
84133
`PIR-E-FLOW-001` refusal form for load-time enforcement mode.
85134
- fixture family `cases/flow/`: the two-LLM contracts scenario as the
86135
seed pair (clean topology accepts; one rebinding of the summarizer to
87-
an endpoint-bound LM violates), plus declassifier-grant and
88-
control-flow vectors.
136+
an endpoint-bound LM violates), plus declassifier-grant,
137+
control-flow, exception-channel, and break-channel vectors (the
138+
prototype selfcheck's nine, promoted).
139+
140+
## Ratification asks (positions taken, for decision)
141+
142+
Three open questions block ratification. The draft takes a position on
143+
each; deciding otherwise changes the schema below, not the analysis.
144+
145+
**1. Label shape: a three-point lattice, not a single marker.**
146+
Classification labels are `secret < internal < public` (default:
147+
`public`, i.e. unlabeled). The policy maps labels to sink classes it
148+
refuses: `{"secret": "no_egress", "internal": "declared_endpoints_only"}`.
149+
Rationale: the single-bit design cannot say "may go to *my* endpoints
150+
but not arbitrary ones," which is the common enterprise posture; and
151+
widening a serialized single-bit marker later is a breaking schema
152+
change, while shipping the lattice now costs one enum. Odersky's story
153+
is the `secret` row alone. A declassifier grant names the step it
154+
performs (`secret → internal` or `secret → public`); an ungraded grant
155+
is refused at policy validation.
156+
157+
**3. Grant scope (new, from the TACIT comparison).** Position: keep
158+
leaf-named global grants for this ratification (simple, receiver-
159+
auditable), and record per-path grant scoping as the named v1.x
160+
follow-up — the policy schema gains an optional `at: <call path>`
161+
qualifier then, an additive change. Deciding for per-path now would
162+
delay ratification for a scope no current scenario needs; deciding
163+
never would close the door on TACIT's defense-in-depth, which is the
164+
part of their design worth importing.
165+
166+
**2. Export-time enforcement defaults to refuse, not warn.**
167+
When any field carries a non-`public` label, `flow_check` runs at
168+
export and a violation refuses the export, naming the flow (source
169+
field → leaf → entry, the teaching-error voice). Opt-down is explicit
170+
and recorded: `export(..., flow="warn")` stamps
171+
`flow_policy: "warn"` into provenance, so a receiver can see the
172+
author bypassed the check. Rationale: the campaign's standing
173+
loud-refusal doctrine (Numba's silent-fallback lesson); a labeled
174+
field is the author *asking* for the guarantee; and an artifact that
175+
exports cleanly under refuse-mode is a checkable claim, not a hope.
176+
Receiver-side `flow_check` is unaffected: it is always the receiver's
177+
own policy and never trusts the author's mode.

0 commit comments

Comments
 (0)