Learn · Chapter 13 of 14

Information-flow control

Capabilities decide which effects a function may use. Information-flow control decides where its data may go. This chapter is the second axis: mark a value @secret and the compiler tells you when it detects it reaching a log line or a network call without going through an audited bridge. By default that is a warning; under @strict_ifc it is an error. The check has real limits, and this chapter names them.

← All chapters

The problem

A capability lets a function do something powerful, like read environment variables or print to the console. But having the authority to read a secret and the authority to print are, on their own, two separate permissions. Nothing yet stops a function with both from doing this:

capa

fun leak(env: Env, stdio: Stdio)
    match env.get("API_KEY")
        Some(key) -> stdio.println(key)
        None -> stdio.println("no key")

That prints the API key to standard output, where it lands in logs, terminal scrollback, and CI output. It is the single most common way secrets leak. Capability discipline alone does not catch it: both Env and Stdio were legitimately granted.

Save that as leak.capa and check it:

terminal

$ capa --check leak.capa
warning: information-flow: a @secret value reaches Stdio.println
  (argument 1), a public sink that sends data out of the program.
  Route it through declassify(value, reason: "...") if this
  disclosure is intended.

The compiler already flagged it, with no annotation from you. The next sections explain why, and how to fix it properly.

Secret by default at the source

Environment variables are where API keys, tokens, and credentials live, so Env.get is a secret source: its result is @secret automatically. The value pulled out of the Some arm inherits that label, and printing it is what raised the warning. You did not have to mark anything; the headline leak is caught out of the box.

It is the only secret source: no other built-in method produces @secret data without an annotation. There is one other built-in source, and it is @public: Serve.recv, the bytes of an inbound request.

The lattice models confidentiality, not integrity

@public on the result of Serve.recv asserts only one thing: this is not a secret whose disclosure the analysis must prevent. It asserts nothing about the data being trustworthy, well-formed, or safe to act on, and an inbound request is attacker-controlled. Validate it exactly as you would in any other language.

Labelling inbound data @secret would put an integrity property into a confidentiality lattice, and the immediate effect would be that echoing a request back to the client that sent it, the most ordinary thing a server does, is reported as a violation. Integrity and taint tracking would be a second lattice, not a relabelling of this one, and Capa does not have one.

Labelling your own data

For data that does not come from a built-in source, you say so. A two-point lattice carries the label: @public (the default) sits below @secret. The annotation attaches to a type, on a parameter, a binding, a return type, or a struct field:

capa

fun charge(card_number: @secret String, stdio: Stdio)
    // card_number is @secret for the whole function body
    stdio.println(card_number)   // warning: secret reaches a public sink

The label is a compile-time property only. It does not change the value or cost anything at runtime; it just travels with the data through the type checker.

How the label travels

A value's label is the join of the labels that flow into it: if any input is @secret, the result is too. This holds through arithmetic, string interpolation, field reads, and function calls (a call with a secret argument returns a secret). So none of these escape the net:

capa

let tagged = "key=${card_number}"   // @secret: interpolation carries it
let first6 = card_number.substring(0, 6)   // @secret: derived from a secret

Inside one function body it also follows data into and out of containers: a secret put in a struct, list, tuple, or a mutable Map / Set / List, or iterated over in a for loop, stays secret. Stashing it somewhere and reading it back in the same body does not launder it.

What crosses a call boundary. A value carries its @secret label into a callee only through a parameter explicitly declared @secret; there is no implicit inference across a bare parameter, but a secret argument passed to a callee whose parameter reaches a public sink is still reported, at the call site, when the analysis detects the flow. Since 1.20.0, a container the callee mutates through such a parameter does carry the label back out: fun stash(bag: List<String>, s: @secret String) whose body is bag.push(s), called from a function that then reads bag into a public sink, is flagged exactly as the identical bag.push(key) inline is: a warning by default, a hard error under @strict_ifc. Earlier releases produced no diagnostic for the callee form.

The sinks

A sink is a point where data leaves the program. The built-in public sinks are:

Stdio.print, Stdio.println, Stdio.eprintln
Net.get, Net.post
Fs.write
Db.exec, Db.query
Serve.send (the payload argument only, not the connection id, which the runtime issued rather than the program)
panic, whose message goes to stderr. It needs no capability, which is exactly why it is easy to forget: a function that holds nothing at all can still disclose through a panic message. Only the built-in applies; a user-defined function named panic shadows it and is handled by the ordinary cross-function analysis.

A @secret value the analysis finds reaching any of them is reported. By default it is a warning, so existing code keeps compiling while labelled code surfaces its disclosures. To make it a hard error, opt the function into strict mode:

capa

@strict_ifc()
fun charge(card_number: @secret String, stdio: Stdio)
    stdio.println(card_number)   // now a compile ERROR, not a warning

Strict mode also turns on implicit-flow checking: a sink inside a branch whose condition is secret leaks one bit (whether the branch was taken) even if the printed value is a constant, and strict mode reports that too.

Declassify: the one way across

Sometimes you genuinely must disclose a derived form of a secret: the last four digits of a card on a receipt, a salted hash of a password for storage. The single sanctioned bridge from @secret to @public is declassify, and it demands a reason:

capa

fun mask(card_number: @secret String) -> String
    let n = card_number.length()
    let last4 = card_number.substring(n - 4, n)
    return declassify(
        "**** **** **** ${last4}",
        reason: "PCI DSS 3.4: display only the last four digits"
    )

The reason must be a plain string literal. declassify is the identity function at runtime (it returns its value unchanged); its whole job is at compile time, where it relabels the result @public. Declassifying a value that was not secret is reported as a no-op, so a stray bridge cannot hide.

Why the reason matters: the manifest

Every declassify call is recorded in the manifest. Ask for it:

terminal

$ capa --manifest app.capa | jq '.summary.declassification_sites'
1

$ capa --manifest app.capa | jq '.functions[] | select(.declassifications | length > 0) | .declassifications'
[ { "reason": "PCI DSS 3.4: display only the last four digits",
    "value": "...", "pos": "10:12" } ]

This is the regulatory payoff. The manifest does not just say which capabilities a program holds; it lists where, and why, the program deliberately discloses sensitive data through declassify, generated by the compiler rather than asserted in a document. An auditor reads that list alongside your data-handling policy.

The honest boundaries

The analysis is deliberately simple, and it is worth knowing its edges:

Summaries across calls. Inside a callee, a parameter is secret only when it is declared @secret; across the call the analysis works from per-function summaries, so a secret argument passed to a callee whose parameter reaches a public sink is reported at the call site when the analysis detects the flow.
Per-field for structs, whole-aggregate elsewhere. A struct field declared @secret keeps its label per field; a secret inside a list, map, or tuple taints the whole aggregate.
A check, not a proof. An accepted program, at either tier, is not thereby proved free of secret-to-sink flows; the analysis reports the flows it detects.

These keep the feature ergonomic and the diagnostics low-noise, which is the lesson IFC research learned the hard way: a checker that cries wolf gets turned off.

Where you go next

One chapter remains: chapter 14 turns everything you have learned into audit artefacts, generating the manifest, the SBOMs, the VEX, and the provenance attestation from one small program. The language reference has the full IFC rules, and the capa_paymentguard showcase puts capabilities, information-flow control, and a generated EU Cyber Resilience Act conformity pack together on a payment-security core, where a flow the compiler detects from a card number to a log or the network unmasked is a build error in its @strict_ifc function and a warning elsewhere.

If you build something with Capa, send it. Real use is the best feedback.

Keep going

← 12. A small project

Previous chapter.

14. From source to SBOM →

Next chapter.