Capture-internal-sink information-flow fix

1Summary

Capa 1.31.0 is an information-flow (IFC) soundness fix. Before it, a @secret value captured by a locally-resolved closure and sunk inside the closure body (a side effect, not the closure's returned result), where the taint arrives after the closure is defined, leaked with no diagnostic at either tier: capa --check reported ok, an @strict_ifc build reported zero errors, and the secret reached a public sink at run time on both backends. The analyzer type-checked the closure body once at its definition, when the captured field was still public, and never re-checked it at the invocation.

The fix adds a per-lambda capture-side sink-path summary and applies it at the invocation, so a live @secret capture that reaches an internal sink is flagged at the invocation position: a warning by default, a hard error under @strict_ifc. It ships under the STABILITY.md security exception as a MINOR bump, and closes the locally-resolved-direct and named-callee portion of 1.30.0's disclosed residual 1. Severity is low to moderate, confidentiality only.

2Problem and threat

Property at stake. Capa treats information-flow control over @secret data as a first-class, machine-checked security property: a @secret value must not reach a public sink (Stdio.println / eprintln, Net.post, panic, a sink-reaching parameter of a further function) without an explicit declassify. The noninterference guarantee is claimed only under @strict_ifc, where the check is a hard error; by default it is a warning.

Threat model. A silent false negative: the author writes @secret, believes they are protected, and a build that gates noninterference on @strict_ifc passes while the secret escapes at run time. There is no integrity or availability impact and no bypass of the capability discipline; the break is confidentiality only. The advisory's illustrative vector is CVSS:3.1/AV:L/AC:H/PR:N/UI:N/S:U/C:H/I:N/A:N (about 5.3), with AC:H reflecting that the specific closure shape and the @secret annotation must all be present.

Pre-fix behaviour (MEASURED). The 1.30.0 lambda-flow fix applied a lambda's latent per-lambda signature at the application site rather than at the definition, and its capture-side face re-read each captured binding's live label at the invocation and joined it into the closure's RESULT label. So a caller that sinks the closure's RESULT after a later mutation was caught. But a sink INTERNAL to the body (the closure returns Unit and prints the captured value itself) was type-checked once at the closure's definition, when the captured field was still public, and never re-checked at the invocation. Minimal reproduction:

const TOKEN: @secret String = "s3cr3t"

type Bag { data: String }

fun leak(stdio: Stdio, secret: @secret String)
    var bag: Bag = Bag { data: "public" }
    let log: Fun() -> Unit = fun() -> Unit => stdio.println(bag.data)
    bag.data = secret        // taint arrives after log is defined
    log()                    // sinks the secret inside the closure body

fun main(stdio: Stdio)
    leak(stdio, TOKEN)

The body stdio.println(bag.data) reads a field that was public when log was defined; the def-time body check saw nothing, and there was no invocation-side capture-internal check. The same shape held when the capture is read through an index, a tuple destructure, a chained method, a match scrutinee, a string interpolation, an alias into a local, a launder into another container, or a method that sinks self; when the sink is reached through a NAMED helper the closure calls; and when the taint is delivered by a named callee's field-write effect rather than an inline store.

3Model and prior art

First-class functions in an information-flow type system. The design frames a closure as carrying a latent flow signature that is instantiated at the application site, not the definition site. This is the model the advisory attributes to FlowCaml (the information-flow extension of Caml; Pottier and Simonet, "Information Flow Inference for ML", POPL 2002 and TOPLAS 2003). MEASURED: the advisory names "FlowCaml's model for first-class functions" as the basis for applying the signature at the application site. The novelty here is that the signature has TWO faces for a capture: a RESULT face (join the capture's live label into the returned value, delivered in 1.30.0) and a SINK face (the capture reaches a sink inside the body regardless of the return, delivered here). The sink face is the read-side mirror of the parameter sink-path summary Capa already computed for named callees.

Noninterference and declassification (background). The underlying property is noninterference (Goguen and Meseguer, 1982): a public observation must not depend on a secret input. declassify(value, reason: "...") is Capa's endorsed escape hatch, an intentional, audited downgrade, in the tradition of principled declassification (Sabelfeld and Sands, "Declassification: Dimensions and Principles", 2005). JUDGEMENT: these citations are the standard basis for the property Capa enforces; they were not re-derived here, they frame the mechanism below. What is MEASURED is that the summary is declassify-aware by construction (an in-body declassify records no sunk path).

4Mechanism

The fix is entirely in the analyzer. It has three parts across three commits: the summary (1daae28), the invocation check plus a shared live-label gate (cac7917), and the corpus that pins the no-suppression-gate decision (9771149). All references below are into the clean 1.31.0 install (site-packages/capa/analyzer/).

4.1 The capture-side sink-path summary (1daae28)

compute_ifc_summaries (_ifc_summary.py:250) now returns a sixth map, capture_sink_paths: {("lambda", id): {capture_name → frozenset(field_path)}}, the access paths of each captured free binding that reach a public sink inside the body (() is the whole capture). It is the capture-side mirror of the parameter sink_paths.

• Each lambda node is retained during the callable-collection walk (self._lambda_nodes[key] = lam, _ifc_summary.py:578; the field is declared at _ifc_summary.py:439), so the summary can recover the lambda's parameters and body after the fixpoint.
• The map is computed once, after the parameter fixpoint stabilises (the loop at _ifc_summary.py:822), because it only READS the now-final named summaries and feeds no other summary, so it needs no fixpoint of its own.
• _capture_sink_paths_of (_ifc_summary.py:1689) does the work: the lambda's FREE identifiers (its captures, via _lambda_free_names at _ifc_summary.py:1742, whose generic name-only walk is _collect_free_names at _ifc_summary.py:1764) are seeded as sources, each capture root name indexing to itself, and the SAME declassify-aware body walk records, per capture, the capture-relative paths that reach a sink. A sink reached via a NAMED helper composes in through that helper's own sink_paths; an in-body declassify yields no source, so it records no path and stays clean by construction.

The analyzer stores the extra map in self._ifc_capture_sink_paths (__init__.py:709, unpacked from compute_ifc_summaries at __init__.py:766). In 1daae28 nothing consumed it, so behaviour was unchanged until the next commit.

4.2 The invocation check and the shared live-label gate (cac7917)

cac7917 factors the per-capture live-label logic out of _fresh_capture_label (_ifc.py:1430) into a shared, side-effect-free _capture_live_label(sym, paths, whole) (_ifc.py:1512). It consults no cached def-time label; it is a pure function of the capture symbol, the accessed paths, and the LIVE channels:

• the branch-scoped container-taint map (_container_taint_at, _capture_container_taint), which is the 1.30.1 field-store (root, field-path) access-path channel;
• the flat container-seeded and whole-value-dirty marks (_container_seeded, _container_whole_dirty);
• the whole-value sym.label, re-read for a reference type but skipped for a value-typed (built-in immutable primitive) capture, which is captured by value.

For a WHOLE or undeterminable read it observes every container taint on the root plus (for a reference type) sym.label; for a FIELD-PRECISE read it observes only the taints prefix-compatible with a read path, so a disjoint clean sibling is not over-tainted. The RESULT re-read now joins this shared gate over the closure's READ paths, a behaviour-preserving refactor.

_apply_lambda_capture_sink_summary (_ifc.py:3146) is the new check. It looks up the lambda's capture_sink_paths summary, resolves the captures by IDENTITY and matches them by name (name to symbol is 1:1 inside one lambda body), then for each summarised capture takes the LIVE label at its SUNK paths through the shared gate and flags only when the normalized live label equals SECRET. It emits at the invocation position via _emit_ifc_call_leak (_ifc.py:3306), warn by default and hard error under @strict_ifc, the same two-tier discipline as the parameter check. It is wired into the same two hooks as the parameter check: the local-lambda call _check_ifc_local_lambda_call (applies the summary at _ifc.py:3091) and the IIFE _check_ifc_iife_call (applies it at _ifc.py:3102). It is orthogonal and additive to the parameter check: neither removes the other's flag.

The emitted diagnostic (exact runtime text, verified in section 6):

information-flow: a @secret value is passed to 'log' as the captured 'bag',
which reaches a public sink inside 'log' (it sends data out of the program).
Route it through declassify(value, reason: "...") if this disclosure is intended.

The callee label is the bound name ('log' for a let-bound lambda) or "the closure" for an IIFE; the captured binding is named (the captured 'bag').

4.3 No def-time suppression gate (9771149)

The check flags whenever a summarised sunk-path label is live @secret, with no attempt to suppress a capture that was "already secret at definition". This is a deliberate soundness decision, pinned by a masking regression guard: a per-name whole-value definition snapshot cannot tell a secret NON-sunk sibling from the sunk path, so such a gate would mask a real leak (a launder-through-a-captured-container shape whose actually-sunk field rises secret after the def while a different field was secret before it). Flagging on the live sunk-path label is always sound. The release commit 7ecbe00 reworded the __init__.py comment to state this precisely; it is a comment-only change, no code change.

4.4 Both backends

MEASURED: the three fix commits touch only capa/analyzer/__init__.py, capa/analyzer/_ifc_summary.py, capa/analyzer/_ifc.py, and test files. No code-generation or runtime file is touched. The check is a single analyzer implementation that runs before code generation, so the diagnostic is backend-independent by construction. The runtime leak is what the analyzer should reject; it was verified to reproduce identically on the Python interpreter and the Wasm Component Model backend (section 6). There is one disclosed, pre-existing code-generation caveat noted in section 7 (a value-typed scalar capture case), which concerns a clean no-false-positive shape, not the security guarantee.

5Alternatives considered and why rejected

• A def-time-secret suppression gate (rejected, 9771149). The obvious way to avoid the before-def duplicate diagnostic (section 7) is to suppress a capture that was already secret when the closure was defined. Rejected because a per-name whole-value snapshot reads a secret NON-sunk sibling and would mask a genuine leak whose actually-sunk field rises secret only after the def. The masking shape is pinned in TestCaptureInternalSinkWholeLaunderMaskingClosed. Flagging on the live sunk-path label, accepting the sound duplicate, was chosen instead.
• Carrying the capture taint into the RESULT only (the 1.30.0 design, insufficient). 1.30.0 re-read the capture at the invocation but joined it into the closure's returned value. A body that returns Unit and sinks the capture as a side effect carries no result to taint, so this missed the internal sink entirely. The SINK face here is additive to the RESULT face, not a replacement (the RESULT re-read is preserved via the shared gate).
• A whole-capture-only summary (rejected by design). Recording only "this capture reaches a sink" without field paths would over-report a field-precise clean sibling and lose the 1.30.1 precision. The summary keys capture-relative field paths and falls back to () only for an aliased or call-rooted sunk value. JUDGEMENT: this trade-off is evidenced by the field-precise no-false-positive pins (TestCaptureInternalSinkNoFalsePositive) rather than stated as a rejected fork in the commits.

6Verification

Before/after, run on both released binaries. Two isolated venvs, capa-language==1.30.1 and capa-language==1.31.0 (capa --version confirmed for each), plus wasmtime for the Wasm backend. The program is the section 2 reproduction; the strict variant is the same with @strict_ifc() on leak.

BEFORE, capa 1.30.1 (silent at both tiers, leaks on both backends):

$ capa --check leak.capa
leak.capa: ok (4 items, 15 expressions typed, 8 bindings)

$ capa --check leak_strict.capa            # @strict_ifc() on leak
leak_strict.capa: ok (4 items, 15 expressions typed, 8 bindings)

$ capa --run leak.capa                     # Python backend
s3cr3t

$ capa --run --wasm leak.capa              # Wasm backend
s3cr3t

AFTER, capa 1.31.0 (warns by default, errors under @strict_ifc; still leaks at run time because a warning does not block):

$ capa --check leak.capa
leak.capa:9:5: warning: information-flow: a @secret value is passed to 'log' as the captured 'bag', which reaches a public sink inside 'log' (it sends data out of the program). Route it through declassify(value, reason: "...") if this disclosure is intended.
   9 |     log()                    // sinks the secret inside the closure body
           ^

leak.capa: ok (4 items, 15 expressions typed, 8 bindings)

$ capa --check leak_strict.capa            # @strict_ifc() on leak
leak_strict.capa:10:5: error: information-flow: a @secret value is passed to 'log' as the captured 'bag', which reaches a public sink inside 'log' (it sends data out of the program). Route it through declassify(value, reason: "...") if this disclosure is intended.
  10 |     log()
           ^

leak_strict.capa: 1 error

The runtime leak is backend-independent (the analyzer is what should reject it); s3cr3t printed on both backends on both versions. Under @strict_ifc the default-tier exit code is 0 (warn only) and the strict exit code is 1.

Tests that pin it. All in tests/test_ifc_branch_scoped_container.py at 7ecbe00. Closed shapes: TestCaptureInternalSinkArrivalShapesClosed (index, tuple, two-helper hop, chained method, match scrutinee, interpolation, alias-into-local, launder-into-container, method-sinks-self, named-callee field-write effect), TestCaptureInternalSinkWholeLaunderMaskingClosed (the masking guard). No false positive: TestCaptureInternalSinkNoFalsePositive (public never-mutated, branch-exclusive, clean disjoint sibling, in-body declassify). Disclosed over-reports: TestCaptureInternalSinkWholeReadSiblingOverReportDisclosed, TestCaptureInternalSinkBeforeDefFlagged. Residuals: TestCaptureInternalSinkResidualStillDisclosed (nested_local_lambda_sink, escaping_alias, escaping_hof_invoked), TestHofInvokedClosureResidualDisclosed, TestEscapingLambdaSinkResidualDisclosed, TestFieldChainRenameResidualDisclosed, TestCallIndexRootedReceiverResidualDisclosed, TestLoopFamilyLeaksStayFlagged.

7Scope and residuals

MEASURED framing: 1.31.0 flags a live-@secret capture SUNK INSIDE the body of a LOCALLY-RESOLVED closure (a let-bound lambda invoked in the same scope, or an IIFE), where the sink is reached DIRECTLY or through a NAMED callee, the capture is read at a determinable field path or through a whole / interpolation / method read, and the taint is delivered by a field store, a container push, or a cross-function field-write effect, arriving AFTER the closure is defined (including the launder-through-a-captured-container masking shape). It closes nothing more. In particular this is NOT "capture-internal sinks are closed".

Open residuals (each a tested false negative that leaks at run time UNFLAGGED at both tiers on both backends, unless noted):

• A sink reached only through a NESTED LOCAL lambda. A closure whose body reaches the sink only through a nested local-lambda binding is opaque to the summary walk, which resolves body calls to NAMED callees only, never to a local-lambda binding. The outer closure IS locally resolved, so this is nested-lambda opacity, not an escaping case. Pinned in TestCaptureInternalSinkResidualStillDisclosed (nested_local_lambda_sink).
• Closures that ESCAPE local resolution. A closure the caller cannot resolve to one certain lambda literal is not reached by the invocation check: an alias (let g = f; g()), a closure passed to a higher-order callee and invoked there (apply(f)), a returned closure, a reassigned var, or a call-result binding. Closing them needs a higher-order control-flow / points-to analysis Capa does not have. Pinned in TestCaptureInternalSinkResidualStillDisclosed (escaping_alias, escaping_hof_invoked) and, result-sink side, in TestHofInvokedClosureResidualDisclosed and TestEscapingLambdaSinkResidualDisclosed.
• Different-root / element-rooted points-to (inherited). The check reads the capture's taint on the same (root, field-path) channel the container and field-store fixes use, so it inherits that channel's points-to residuals: a container renamed out of the struct (var lst = bag.items; lst.push(secret)), a mutator rooted at a call or an index (get_items(bag).push(secret), arr[0].items.push(secret)), and a struct reached through a container VALUE or ELEMENT read via .get(...). Pinned in TestFieldChainRenameResidualDisclosed, TestCallIndexRootedReceiverResidualDisclosed.
• Loop-carried read-before-write in the summary walk (inherited). The capture-side summary walks the body once in source order with no iteration fixpoint, so a capture read placed textually before a push inside a while / for that a later iteration would feed is not recorded as a sunk path. The intra-procedural loop-carried read IS caught by the two-pass loop walk (TestLoopFamilyLeaksStayFlagged); the summary-tier one is not.

Two disclosed sound over-reports (they FLAG though nothing secret reaches the sink; they over-report, never under-report):

• A WHOLE / method read of a CLEAN sibling of a mutated struct. A closure that sinks a captured struct through a whole / method read (bag.reveal(), returning only a public field) is FLAGGED when a DIFFERENT field is stored a secret after the def, because a whole read observes every field taint of the root and cannot tell the clean field it reveals from the stored sibling. It flags but leaks nothing. At parity with the 1.30.0 result-sink whole-read over-report. Pinned in TestCaptureInternalSinkWholeReadSiblingOverReportDisclosed.
• A before-def secret carries a duplicate diagnostic. When the taint arrives BEFORE the closure is defined, the def-time body check AND the new invocation-site check both fire, differing in message and position. Both are sound and land on genuinely-leaking code, so the duplicate is two findings, not a contradiction. No def-time suppression gate is used (section 5). Pinned in TestCaptureInternalSinkBeforeDefFlagged.

One pre-existing code-generation caveat (disclosed, not introduced here): the value-typed scalar no-false-positive case (TestCaptureInternalSinkScalarValueTyped) is asserted Python-only, under a known scalar-capture-sink Wasm code-generation bug recorded in 9771149. It concerns a CLEAN shape (no leak), so it does not affect the security guarantee. Not independently reproduced in this record.

8Cross-references

• Version. 1.31.0 (released 2026-08-11). MINOR bump under the STABILITY.md security exception, matching the earlier IFC soundness releases (1.2.0, 1.3.0, 1.4.0, 1.15.0, 1.26.0 through 1.30.0). 1.30.1 was by contrast a PATCH (precision only, no leak closed).
• Commits. 1daae28 (per-lambda capture-side sink-path summary), cac7917 (apply it at the locally-resolved invocation against the live field-precise capture label; shared _capture_live_label gate), 9771149 (pin the corpus; no def-time suppression gate), 7ecbe00 (release: version bump, advisory, CHANGELOG / DONE / SECURITY / STABILITY, comment reword only).
• Advisory. docs/advisories/2026-08-11-ifc-capture-internal-sink.md. DISCREPANCY (MEASURED): an external identifier (GHSA / CWE-200) is referenced by the release process, but no GHSA / CWE / CVE identifier appears in the committed 1.31.0 tree or in the advisory body itself. This record treats that identifier as an out-of-tree reference, not as tree content.
• Tests. tests/test_ifc_branch_scoped_container.py (section 6).
• Related records. The 1.30.0 lambda-flow advisory (2026-08-10-ifc-lambda-flow-sensitivity.md), whose residual 1 this closes for its locally-resolved-direct / named-callee portion, and its named blocker, the 1.30.1 field-store (root, field-path) access-path channel, which this consumes. The broader information-flow laundering line: 2026-06-16-soundness.md, 2026-07-03-soundness.md, and the 2026-08 advisories for 1.26.0 through 1.30.0.