Skip to main content

Information-Flow Control (IFC) Labels

AILANG v0.16.0 adds information-flow control (IFC) labels to the type system. Labels mark values as carrying source-level taint and let the compiler refuse to route untrusted data into sensitive sinks. The runtime cost is zero — labels exist only at the type-system layer.

The design follows Erik Meijer's Guardians of the Agents (CACM, January 2026) and its Python reference implementation metareflection/guardians (~1,900 LOC). Meijer's paper proposes a three-check guardian pipeline (taint + automata + Z3); AILANG already shipped the Z3 piece in v0.9.x, and this milestone adds the taint piece as a language feature rather than an external library.

This guide is the user-facing companion to the M-TAINT-TYPES design doc. For the motivating essay, see Half of guardians is already a language feature.

When to reach for labels

You want IFC labels when you have untrusted input flowing through your program toward sinks that must not see it raw — classic prompt-injection scenarios, SQL string assembly, shell-out builders, HTML rendering, or any boundary where "instructions" and "data" share a representation.

The Three Pieces of Syntax​

FormRead aloudUse it for
T<label>"T tainted with label"Mark a value as carrying source-level taint.
T{not LABEL}"T refining-out LABEL"Mark a parameter position as a sink that refuses LABEL.
! {Declassify}"may declassify"Effect-row entry on functions that intentionally lower a label.
-- A string carrying the <email> label (untrusted source)
let body: string<email> = fetchMailBody()

-- A function whose body parameter rejects any <email>-tainted input
pure func sendEmail(to: string, body: string{not email}) -> () ! {Net}

-- A declassifier: <email> in, <sanitized> out, must declare ! {Declassify}
pure func sanitize(raw: string<email>) -> string<sanitized> ! {Declassify}

Labels Are Open​

Labels are not a fixed vocabulary. <email> is just the demo label. You can use any lowercase identifier (kebab-case for compounds) and the type system will track it. There is no enum, no registry, no migration step — define labels at the point of use, in the type signature, in the language you already speak.

The same lattice machinery handles all of them. Combinations join naturally: a value with both <email> and <pii> taint has type string<email ⊔ pii>, and a sink that refuses either label (string{not pii}) will reject it.

Common patterns we expect you to write:

DomainSource labelsSink refinements
Agent / LLM<user-input>, <email>, <tool-output>{not user-input} on sendEmail, runShell, evalSql
Web / API<request-body>, <query-string>, <header>{not request-body} on executeSQL, renderHTML
Compliance<pii>, <phi>, <gdpr-eu>{not pii} on logEvent, analytics
Secrets<api-key>, <token>, <password>{not api-key} on httpResponseBody, errorReport
Multi-tenant<tenant-a>, <tenant-b>{not tenant-a} on serialisers crossing tenant boundaries

The runtime cost is zero regardless of how many labels you define — they all erase at compile time. Pick the labels that match your threat model and add new ones whenever a new source/sink shape appears.

Naming Convention​

Labels are names. They should be short, lowercase, and descriptive of the source of the taint — not the sink, and not the policy.

GoodWhy
<email>A string came from email content
<user-input>A string came from user input (kebab-case for compounds)
<sql-text>A string came from a SQL builder context
<pii>Personally identifiable info
<sanitized>Output of an explicit sanitiser (reset state)
AvoidWhy
<EMAIL>Use lowercase. Labels are not constructors.
<safe>Says nothing about provenance. Use <sanitized> or similar.
<bad> / <dirty>Subjective. Name the source, not the disposition.

The Two Rules​

1. The Sink Rule​

A parameter typed T{not LABEL} rejects any argument whose type carries the <LABEL> annotation.

pure func sendEmail(to: string, body: string{not email}) -> () ! {Net}

-- ✅ Caller passes a declassified value
sendEmail("alice@company.com", sanitize(rawBody))

-- ❌ Caller passes the raw body — refused
sendEmail("alice@company.com", rawBody)  -- string<email> ↛ string{not email}

2. The DECLASS Rule​

A function that changes a value's label must declare ! {Declassify} in its effect row. Identity (same label in and out) is free; any other transition needs the effect.

-- ✅ Allowed: explicit declassifier
pure func sanitize(raw: string<email>) -> string<sanitized> ! {Declassify}
{ "[sanitized]" }

-- ❌ Rejected: function changes label without declaring Declassify
pure func sneakySanitize(raw: string<email>) -> string<sanitized> ! {}
{ "[sanitized]" }

The {Declassify} effect makes label-lowering auditable — every sanitiser is locatable by grep -r '! {Declassify}'.

Why Identity Bypass Doesn't Work​

Pure operations propagate labels through their result via the APP-PURE rule: the output label is the join of all input labels. Identity functions carry the input's label forward.

-- Attempting to "launder" the label via an identity binding:
pure func attemptLaunder(rawBody: string<email>, recipient: string)
  -> SendAction ! {}
{
  let laundered = rawBody in    -- laundered: string<email> (label preserved)
  { to: recipient, body: laundered }  -- still rejected at the sink
}

There is no clever construction — wrapping in a record, routing through a let, calling an identity helper — that strips a label. Only an explicit ! {Declassify} function can lower it.

Worked Example: Inbox Injection​

The single-module demo:

examples/runnable/contracts/inbox_injection_v2.ail
-- examples/runnable/contracts/inbox_injection_v2.ail
--
-- Inbox-injection demo rewritten using M-TAINT-TYPES label annotations.
-- This is the v2 successor to inbox_injection.ail which used plain string types
-- and Z3 contracts alone. V2 adds T<label> source annotations and T{not LABEL}
-- sink refinements to express the taint policy at the type level.
--
-- The scenario mirrors "Guardians of the Agents" (Meijer, CACM Jan 2026):
-- a mail-processing agent must not let untrusted email body text flow to
-- network sinks without going through an explicit declassify step.
--
-- Label lattice used here:
--   <email>     -- raw text received from the mail inbox (untrusted source)
--   <sanitized> -- text that has been scrubbed by an explicit sanitize step
--   string{not email} -- sink refinement: refuses any value labelled <email>
--
-- With full label enforcement (M-TAINT-TYPES Phase 2+), the two ATTACK
-- functions below will be caught as TYPE ERRORS before Z3 runs.
-- Today (Phase 1 demo), Z3 catches them via the ensures contracts.
--
-- Run:    ailang verify examples/runnable/contracts/inbox_injection_v2.ail
-- Expect: 5 functions: 3 verified, 2 violations (injectedForward, attemptLaunder)

module examples/runnable/contracts/inbox_injection_v2

import std/string (endsWith, length as strLen)

-- The data shape placed on the wire by the agent.
type SendAction = { to: string, body: string }

-- ---------------------------------------------------------------------------
-- Sanitize: the declassify gate
-- ---------------------------------------------------------------------------

-- sanitizeBody strips all raw content, replacing it with a constant.
-- Label typing: input is string<email> (untrusted), output is string<sanitized>.
-- The Declassify effect flags that this function intentionally changes the label.
-- Z3 contract pins the output: any call-site can prove the body is [sanitized].
export pure func sanitizeBody(rawBody: string<email>) -> string<sanitized> ! {Declassify}
ensures { result == "[sanitized]" }
{
  "[sanitized]"
}

-- ---------------------------------------------------------------------------
-- Helpers
-- ---------------------------------------------------------------------------

-- isInternal: domain check for allowlisted recipients.
export pure func isInternal(addr: string) -> bool ! {}
ensures { result == endsWith(addr, "@company.com") }
{
  endsWith(addr, "@company.com")
}

-- ---------------------------------------------------------------------------
-- SAFE: sanitize then send
-- ---------------------------------------------------------------------------

-- safeForward routes an email safely:
--   rawEmail: string<email>    (untrusted source — never touches the wire)
--   → sanitizeBody             (Declassify gate changes label to <sanitized>)
--   → body of SendAction       (sink accepts string{not email}: <sanitized> satisfies {not email})
--
-- Z3 verifies: result.body == "[sanitized]" — the raw content is provably absent.
export pure func safeForward(rawEmail: string<email>, recipient: string) -> SendAction ! {Declassify}
requires { endsWith(recipient, "@company.com") }
ensures  { endsWith(result.to, "@company.com"), result.body == "[sanitized]" }
{
  { to: recipient, body: sanitizeBody(rawEmail) }
}

-- ---------------------------------------------------------------------------
-- ATTACK 1: inject raw email body into the sink
-- ---------------------------------------------------------------------------

-- injectedForward is the prompt-injection pattern: an LLM instruction inside
-- rawEmail causes the agent to forward the raw body instead of a summary.
--
-- Label violation (Phase 2+):
--   rawEmail has label <email>
--   result.body field is a {not email} sink
--   → TYPE ERROR: <email> flows into {not email} position
--   Source: rawEmail (<email>) → Sink: SendAction.body ({not email})
--
-- Z3 catches this today: result.body == "[sanitized]" fails when body = rawEmail.
export pure func injectedForward(rawEmail: string<email>, recipient: string) -> SendAction ! {}
requires { endsWith(recipient, "@company.com") }
ensures  { endsWith(result.to, "@company.com"), result.body == "[sanitized]" }
{
  { to: recipient, body: rawEmail }  -- SINK VIOLATION: <email> → {not email}
}

-- ---------------------------------------------------------------------------
-- ATTACK 2: attempt to launder the label via an identity binding
-- ---------------------------------------------------------------------------

-- attemptLaunder shows that wrapping rawEmail in a let-binding does not erase
-- its label. APP-PURE rule: every pure operation joins input labels into output.
-- Identity preserves labels: laundered inherits <email> from rawEmail.
--
-- Label violation (Phase 2+):
--   laundered: string<email>  (identity from rawEmail, label preserved by APP-PURE)
--   result.body is {not email} sink
--   → TYPE ERROR: <email> still flows — identity bypass is structurally impossible
--
-- Z3 catches this today: laundered == rawEmail, so result.body != "[sanitized]".
export pure func attemptLaunder(rawEmail: string<email>, recipient: string) -> SendAction ! {}
requires { endsWith(recipient, "@company.com") }
ensures  { endsWith(result.to, "@company.com"), result.body == "[sanitized]" }
{
  let laundered = rawEmail in  -- laundered: string<email> — label NOT erased by identity
  { to: recipient, body: laundered }  -- SINK VIOLATION: <email> → {not email}
}

-- ---------------------------------------------------------------------------
-- Entry point (not verified — no contracts)
-- ---------------------------------------------------------------------------

export func main() -> int ! {Declassify}
{
  let action = safeForward("confidential-body", "alice@company.com");
  if isInternal(action.to) then strLen(action.body) else 0
}

Run it:

ailang verify examples/runnable/contracts/inbox_injection_v2.ail

Output:

✓ VERIFIED safeForward
✓ VERIFIED sanitizeBody
✓ VERIFIED isInternal
✗ VIOLATION injectedForward
✗ VIOLATION attemptLaunder

5 functions: 3 verified, 2 violations

Real-World Scenarios​

Each of the patterns below has been documented in published security research or incident write-ups. The labels you'd reach for, and a sketched signature of the sink that would have caught it.

1. Indirect prompt injection via email or document​

An agent processes a document (email, PDF, web page, calendar invite) that contains instructions targeting the agent itself. Documented extensively in Greshake et al., 2023 and listed as OWASP LLM01. This is the headline scenario for IFC labels.

-- Source: any text fetched from external content
pure func fetchEmailBody() -> string<email> ! {FS}
pure func fetchWebPage(url: string) -> string<web> ! {Net}

-- Sink: tool calls that act in the world
pure func sendEmail(to: string, body: string{not email}) -> () ! {Net}
pure func runShell(cmd: string{not email, not web}) -> () ! {Process}

The runShell sink rejects both <email>-tainted and <web>-tainted arguments, so a model that reads a PDF and tries to execute a shell command described inside it gets a structural type error before the shell runs.

2. PII leakage in agent summaries​

An agent reads a customer record, summarises it for a downstream analytics call, and accidentally includes raw PII (names, account numbers) in the summary body. Categories: GDPR Art. 5(1)(c) (data minimisation), HIPAA §164.312(e). See NIST AI RMF Profile: Generative AI, GV-1.3-006.

-- PII source from a customer record
pure func loadCustomer(id: string) -> Customer<pii> ! {FS}

-- A redactor is the only path from <pii> → <redacted>
pure func redactPII(c: Customer<pii>) -> Summary<redacted> ! {Declassify}

-- Analytics sink refuses raw PII
pure func logEvent(name: string, payload: string{not pii}) -> () ! {Net}

A model that calls logEvent("customer_seen", customer.name) is rejected: customer.name carries <pii>, the sink refuses it. The only way through is redactPII — which has ! {Declassify} and is grep-able for audit.

3. Secret exfiltration via error responses​

An agent throws an error and the error handler embeds environment state — including an API key — in the response body returned to the user. Documented incident pattern after the 2024 OWASP LLM Top 10 v1.1 §LLM02 (Insecure Output Handling) update; analogous to log-injection bugs that have shipped credentials to telemetry pipelines for years.

-- Secrets are tainted at the source
pure func getEnv(name: string) -> string<api-key> ! {Env}

-- Error responses cannot contain api-key-tainted strings
pure func httpResponse(status: int, body: string{not api-key}) -> Response ! {}

A debug handler that does httpResponse(500, "config: ${getEnv("OPENAI_API_KEY")}") is rejected at the type level. The fix is either don't include the secret, or pass it through an explicit redactSecret(s) ! {Declassify} function.

4. SQL / command injection through LLM output​

An LLM generates a query fragment, which a tool runs against a database. The classic SQL injection problem reborn: the LLM output is indistinguishable from "trusted" template text by the time it reaches the executor. See NVIDIA AI Red Team writeups and the MathGPT DEFCON 2023 demonstration where an LLM-driven calculator was tricked into executing arbitrary Python.

-- Output of any LLM is tainted as <llm>
pure func askLLM(prompt: string) -> string<llm> ! {AI}

-- The query executor refuses LLM-derived text
pure func executeSQL(query: string{not llm}) -> [Row] ! {DB}

The only way to compose them is to run the LLM output through a parser/whitelister with ! {Declassify} — and now you have an audit trail for every place the boundary is crossed.

5. Multi-tenant data crossover​

A SaaS agent reads tenant A's data and serialises a response that gets dispatched to tenant B's webhook. Easy to do by accident in async pipelines; surfaced repeatedly in cross-tenant LLM scenarios where the prompt context is shared. Categories: SOC 2 CC6.6, ISO 27001 A.9.4.1.

-- Per-tenant labels - open vocabulary, you make these up
pure func loadOrders(tenant: TenantId) -> [Order<tenant-a>] ! {DB}

-- Per-tenant webhook sink
pure func dispatchToTenantB(payload: string{not tenant-a}) -> () ! {Net}

Routing tenant-A data into a tenant-B webhook produces a type error. This pattern is impractical to catch with runtime guards alone, since "the right tenant" is often a chain of let-bindings deep — but the compiler walks every binding.

Cross-Module Label Flow​

Labels travel across module boundaries through the iface JSON. The library exports a record with labelled fields:

examples/runnable/contracts/inbox_v2_lib.ail
-- examples/runnable/contracts/inbox_v2_lib.ail
--
-- Library module for the cross-module inbox-injection v2 demo.
-- Exports a record type whose fields carry IFC labels. Importing modules
-- see the labels at the iface level via M6 (iface JSON serialisation),
-- so reading `m.body` yields a value labelled <email> at the type system.
--
-- Companion file: inbox_v2_app.ail (consumer + sink + workflow).

module examples/runnable/contracts/inbox_v2_lib

-- Mail: an inbox message with tainted body and subject. Field labels
-- mark these as untrusted-source data; routing them directly to a
-- {not email} sink is structurally unsafe.
--
-- The label travels cross-module through the iface JSON: the importing
-- module sees `body: string<email>` even though the underlying value
-- is a plain string at runtime.
export type Mail = {
  body: string<email>,
  subject: string<email>
}

The consumer module imports the labelled type and operates on it:

examples/runnable/contracts/inbox_v2_app.ail
-- examples/runnable/contracts/inbox_v2_app.ail
--
-- Cross-module inbox-injection demo (M-TAINT-TYPES Phase 2).
-- The lib module (`inbox_v2_lib.ail`) defines a Mail record type with
-- labelled fields:
--   body: string<email>
--   subject: string<email>
--
-- This app module imports Mail and defines the workflow + sink + attacks.
-- The labels travel cross-module via M6 (iface JSON serialisation), so
-- when the app reads `m.body`, the type-system view is `string<email>`
-- even though the runtime value is a plain string.
--
-- Sink violations therefore surface a CROSS-MODULE binding chain:
--   source: inbox_v2_lib.Mail.body field (label <email>)
--     → app's binding via record access
--       → app's SendAction.body sink (expects {not email})
--
-- Run:    ailang verify examples/runnable/contracts/inbox_v2_app.ail
-- Expect: 5 functions: 3 verified, 2 violations (injectedForward, attemptLaunder)

module examples/runnable/contracts/inbox_v2_app

import examples/runnable/contracts/inbox_v2_lib (Mail)
import std/string (endsWith, length as strLen)

type SendAction = { to: string, body: string }

-- ---------------------------------------------------------------------------
-- Sanitize: the declassify gate
-- ---------------------------------------------------------------------------

-- sanitizeBody strips the raw content and returns a constant scrubbed
-- value. The Declassify effect documents that this function intentionally
-- changes the label of its input from <email> to <sanitized>.
export pure func sanitizeBody(rawBody: string<email>) -> string<sanitized> ! {Declassify}
ensures { result == "[sanitized]" }
{
  "[sanitized]"
}

-- ---------------------------------------------------------------------------
-- Helpers
-- ---------------------------------------------------------------------------

export pure func isInternal(addr: string) -> bool ! {}
ensures { result == endsWith(addr, "@company.com") }
{
  endsWith(addr, "@company.com")
}

-- ---------------------------------------------------------------------------
-- SAFE: declassify before sending
-- ---------------------------------------------------------------------------

-- safeForward declassifies the imported Mail.body before placing it on
-- the wire. Z3 verifies: result.body == "[sanitized]".
export pure func safeForward(m: Mail, recipient: string) -> SendAction ! {Declassify}
requires { endsWith(recipient, "@company.com") }
ensures  { endsWith(result.to, "@company.com"), result.body == "[sanitized]" }
{
  { to: recipient, body: sanitizeBody(m.body) }
}

-- ---------------------------------------------------------------------------
-- ATTACK 1: cross-module sink violation
-- ---------------------------------------------------------------------------

-- injectedForward forwards the imported Mail.body verbatim. The label
-- <email> originates in inbox_v2_lib.Mail.body and propagates straight
-- into the {not email} sink position.
--
-- Label violation (Phase 2+):
--   source: inbox_v2_lib.Mail.body (label <email>)
--   binding: m.body (record access, inherits <email>)
--   sink: SendAction.body field (expects {not email})
--   → cross-module SINK VIOLATION
--
-- Z3 catches this today: result.body == m.body fails the postcondition.
export pure func injectedForward(m: Mail, recipient: string) -> SendAction ! {}
requires { endsWith(recipient, "@company.com") }
ensures  { endsWith(result.to, "@company.com"), result.body == "[sanitized]" }
{
  { to: recipient, body: m.body }  -- SINK VIOLATION: <email> → {not email}
}

-- ---------------------------------------------------------------------------
-- ATTACK 2: identity-style launder, cross-module
-- ---------------------------------------------------------------------------

-- attemptLaunder routes the imported Mail.body through an identity
-- let-binding. APP-PURE rule: identity preserves labels, so `laundered`
-- still carries <email>.
export pure func attemptLaunder(m: Mail, recipient: string) -> SendAction ! {}
requires { endsWith(recipient, "@company.com") }
ensures  { endsWith(result.to, "@company.com"), result.body == "[sanitized]" }
{
  let laundered = m.body in
  { to: recipient, body: laundered }  -- SINK VIOLATION: <email> still flows
}

-- ---------------------------------------------------------------------------
-- Entry point
-- ---------------------------------------------------------------------------

export func main() -> int ! {Declassify}
{
  let m = { body: "confidential-body", subject: "subject" };
  let action = safeForward(m, "alice@company.com");
  if isInternal(action.to) then strLen(action.body) else 0
}

Run it:

ailang verify examples/runnable/contracts/inbox_v2_app.ail

Output: 5 functions: 3 verified, 2 violations — the <email> label flows from the lib's record field into the app's parameter type and on to the violating sink.

Limitations (v0.16.0)​

  • Phase 1 enforcement only. Sink violations and DECLASS rule violations are caught by Z3 contracts today, not by structural type errors. Phase 2+ work will lift label checking into the elaborator so violations surface as compile errors before Z3 runs.
  • Label aliases are not yet expanded. export type EmailBody = string<email> parses, but the type checker treats EmailBody as a nominal type rather than an alias for string<email>. Use record types with labelled fields for cross-module flow today.
  • Refinements are sink-side only. T{not LABEL} lives on parameter positions; you cannot annotate a return type with a refinement.
  • Cross-module function calls in Z3. Imported function calls cannot yet be encoded into the SMT context (the body lives in another Core program). Use cross-module types for cross-module label flow today; follow-up work tracked as M-SMT-CROSS-MODULE-FUNCTIONS.

Further Reading​

Prior art​