Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 9 additions & 6 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@

Capa is a small, capability-typed programming language. Every
function declares the authorities it holds (`Fs`, `Net`, `Stdio`,
`Clock`, `Random`, `Env`, `Db`, `Proc`, `Unsafe`), the analyzer
`Clock`, `Random`, `Env`, `Db`, `Proc`, `Serve`, `Unsafe`), the analyzer
enforces those declarations statically, and the compiler emits
**CycloneDX SBOM**, **SPDX 2.3**, **VEX**, and **SLSA Build L1
provenance** documents directly from the same capability signatures.
Expand Down Expand Up @@ -194,8 +194,10 @@ import is needed at the Component Model boundary.
## Standard library + seed libraries

The runtime ships built-in types (`Result`, `Option`, `List`,
`Map`, `Set`, `JsonValue`) and built-in capabilities (`Stdio`,
`Fs`, `Net`, `Env`, `Clock`, `Random`, `Db`, `Proc`, `Unsafe`).
`Map`, `Set`, `JsonValue`) and ten built-in capabilities (`Stdio`,
`Fs`, `Net`, `Env`, `Clock`, `Random`, `Db`, `Proc`, `Serve`,
`Unsafe`). `Serve` (inbound TCP) and `Unsafe` are Python-backend
only; `capa --wasm` rejects a program whose signatures reach either.
Full reference in [`docs/stdlib.md`](docs/stdlib.md).

Eight **seed libraries** live in standalone repos and are
Expand Down Expand Up @@ -289,9 +291,10 @@ backend (with a Python/Wasm output parity harness), and
Hypothesis-based property tests. The transpiler
suite actually executes the generated Python and checks stdout; the
property suite fuzzes the full pipeline with arbitrary text and
syntax-aware Capa programs. The Wasm backend runs every capability
(Fs, Env, Clock, Stdio, Net, Random, Db, Proc) and the full language
surface with output byte-identical to the Python reference, and
syntax-aware Capa programs. The Wasm backend runs every capability it
supports (Fs, Env, Clock, Stdio, Net, Random, Db, Proc, all but the
Python-only Serve and Unsafe, which it rejects loudly) and the full
language surface with output byte-identical to the Python reference, and
cross-function capability attenuation is enforced soundly at the Wasm
runtime via host-side handle tables.

Expand Down
5 changes: 3 additions & 2 deletions capa/analyzer/_declarations.py
Original file line number Diff line number Diff line change
Expand Up @@ -503,8 +503,9 @@ def _ty_contains_fun_deep(
exact quarantine violation F2 relies on being impossible), so it
must be rejected wherever it is reachable, not only as a literal
head. The walk mirrors the Wasm backend's
``_unsafe_bearing_type_names`` fixpoint (struct fields +
variant payloads + generic args) and is cycle-guarded on the
``_python_only_caps._cap_bearing_type_names`` fixpoint
(struct fields + variant payloads + generic args) and is
cycle-guarded on the
type name for recursive types (``type Tree { kids: List<Tree>
}``)."""
from . import SymbolKind
Expand Down
34 changes: 34 additions & 0 deletions capa/analyzer/_ifc.py
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,20 @@
("Fs", "write"): {0, 1},
("Db", "exec"): {0, 1},
("Db", "query"): {0, 1},
# Serve.send writes bytes to whoever is on the other end of an
# inbound connection -- exfiltration exactly like Net.post. Only
# argument 1 (the payload) is a sink; argument 0 is the connection
# id the runtime handed out, not program data, so gating it would
# be noise.
#
# It is spelled ``send`` and not ``write`` because the summary pass
# in ``_ifc_summary`` attributes a sink to a capability BY METHOD
# NAME (it has no receiver type at that point), which is sound only
# while each sink method name belongs to exactly one capability.
# ``Fs.write`` already owns "write", so a ``Serve.write`` made every
# ``fs.write`` report Serve as a reached capability too -- caught by
# tests/test_unaudited_secret_sink_fact.py when this landed.
("Serve", "send"): {1},
}

# Built-in capability methods that PRODUCE secret data -- the sources.
Expand All @@ -78,6 +92,26 @@
# and over-labelling it would warn on every legitimate file echo. A
# program that does hold a secret in a file can annotate the binding
# ``@secret`` explicitly. Future levels could make this configurable.
#
# ``Serve.read`` is deliberately NOT a source either, and this is the
# one entry whose ABSENCE is a decision worth spelling out. Serve
# (2026-07) is the language's first INBOUND data source, so it is the
# first time the question "is data arriving from outside secret?" has
# an answer to give. It is ``@public``.
#
# The reason is that this lattice models CONFIDENTIALITY -- who is
# allowed to LEARN a value -- and not integrity or taint. An inbound
# request is untrusted, but "untrusted" is an integrity property, and
# labelling it ``@secret`` would encode it in the wrong lattice: the
# immediate consequence is that echoing a request back to the client
# that sent it (the single most ordinary thing a server does) becomes
# a reported violation. The useful signal would drown in that noise.
#
# ``Serve.read`` being ``@public`` therefore asserts only "these bytes
# are not a secret whose disclosure this analysis must prevent". It
# asserts NOTHING about whether they can be trusted. Integrity /
# taint tracking would be a second lattice, not a relabelling of this
# one.
_SECRET_SOURCES: frozenset = frozenset({
("Env", "get"),
})
Expand Down
7 changes: 6 additions & 1 deletion capa/analyzer/_ifc_summary.py
Original file line number Diff line number Diff line change
Expand Up @@ -1028,7 +1028,12 @@ def _taint_of_method_call(
# this argument reach this built-in sink, so record its
# capability against EACH of them. A sink method name is
# unique to one capability in ``_PUBLIC_SINKS``, so
# ``_cap`` is determinate.
# ``_cap`` is determinate. That uniqueness is not a
# happy accident to be relied on quietly: it is now
# pinned by
# ``test_sink_method_names_are_unique_per_capability``
# in tests/test_serve_capability.py, which fired when
# Serve was first given a ``write``.
self._attribute_sink_caps(arg_srcs[pos], (_cap,))

# A mutating container method (push / add / set) routes the
Expand Down
35 changes: 35 additions & 0 deletions capa/builtins.py
Original file line number Diff line number Diff line change
Expand Up @@ -302,6 +302,41 @@ def fun(*params_then_ret: Ty) -> TyFun:
("allows", fun(TyString, TyBool), []),
("exec", fun(TyString, TyString, _str_res), []),
],
"Serve": [
# Inbound TCP listener (2026-07). Connection-level on purpose:
# the trusted runtime binds, accepts, and moves bytes; HTTP (or
# any other protocol) is parsed by ordinary Capa code, so a
# protocol bug is not a bug in the trusted computing base.
#
# Attenuation domain is the (bind address, port) pair, spelled
# ``"addr:port"`` / ``"addr:lo-hi"`` / ``"addr:*"`` with ``*``
# also accepted as the address. ``allows`` mirrors ``listen``'s
# argument shape rather than the one-String shape of the other
# caps, precisely so "allows(a, p)" answers "would listen(a, p)
# be permitted".
#
# Bytes are ``List<Int>`` with each element in ``0..=255``.
# ``recv`` returning an EMPTY list means EOF (the peer closed).
# Spelled recv/send, the standard socket verbs; ``write`` in
# particular is unavailable because IFC sink attribution
# requires sink method names to be unique per capability and
# ``Fs.write`` already holds that name.
# Serve is sequential: one open connection at a time, no
# threads and no async. ``accept`` and ``read`` are bounded by
# a timeout and return ``Err`` rather than hanging.
#
# Python backend only: the Wasm emitter rejects any signature
# reaching Serve (no vendored ``wasi:sockets``).
("restrict_to", fun(TyString, TyName("Serve")), []),
("allows", fun(TyString, TyInt, TyBool), []),
("listen", fun(TyString, TyInt, _unit_res), []),
("local_port", fun(res(TyInt, _io_err)), []),
("accept", fun(res(TyInt, _io_err)), []),
("recv", fun(TyInt, TyInt, res(lst(TyInt), _io_err)), []),
("send", fun(TyInt, lst(TyInt), _unit_res), []),
("close", fun(TyInt, _unit_res), []),
("stop", fun(_unit_res), []),
],
"JsonValue": [
("is_null", fun(TyBool), []),
("as_bool", fun(opt(TyBool)), []),
Expand Down
42 changes: 40 additions & 2 deletions capa/ir/_capa_types.py
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,32 @@
# that module skips wholesale when Hypothesis is absent and a
# registry guard must never be skippable.)
BUILTIN_CAPS: frozenset[str] = frozenset({
"Stdio", "Fs", "Net", "Env", "Clock", "Random", "Proc", "Db", "Unsafe",
"Stdio", "Fs", "Net", "Env", "Clock", "Random", "Proc", "Db",
"Serve", "Unsafe",
})


# The built-in caps the Wasm backends cannot implement at all. A
# program whose signatures reach one of these is rejected up front
# with a diagnostic naming the offending sites, so it never reaches
# lowering or the host bridges.
#
# TWO independent paths must reject, because each is reachable on
# its own: the Wasm emitter's discovery pass (``capa --wasm``) and
# WIT generation (``capa --wit``, which never runs the emitter). The
# shared reachability scan they both call lives in
# [`_python_only_caps.py`](_python_only_caps.py).
#
# These are PERMANENT stances, not backlog items:
#
# - ``Unsafe`` grants raw pointer / FFI / mmap-class primitives that
# have no sandboxed Wasm equivalent (slice 7 / D5, 2026-05).
# - ``Serve`` needs ``wasi:sockets`` to bind a listening socket. That
# world is not vendored in ``capa/wasi_wit`` and is not reachable
# from the wasmtime-py 44 bindings the hosts are built on, so there
# is no inbound socket for the guest to be handed (2026-07).
PYTHON_ONLY_CAPS: frozenset[str] = frozenset({
"Unsafe", "Serve",
})


Expand Down Expand Up @@ -60,6 +85,19 @@
# derived from ``BUILTIN_CAPS - HANDLE_BEARING_CAPS`` so that adding
# a capability forces an explicit choice instead of silently
# defaulting to "erased".
#
# ``Unsafe`` and ``Serve`` are here because they are members of
# ``PYTHON_ONLY_CAPS``: the Wasm backends reject them before lowering,
# so neither ever reaches a Wasm slot and "handle-bearing" would be a
# claim about codegen that never runs. Erased is also the SAFER
# classification for a rejected cap. If the rejection ever developed a
# hole, an erased cap pushes no value and the module fails to link
# against a host import nobody defined (loud); a handle-bearing cap
# would occupy an i32 slot with no entry in the host's root-handle
# map and silently fall back to the ``Fs`` root, which is exactly the
# quiet cross-cap substitution
# ``test_host_root_handle_map_covers_every_handle_bearing_cap``
# exists to prevent.
ERASED_CAPS: frozenset[str] = frozenset({
"Stdio", "Random", "Unsafe",
"Stdio", "Random", "Unsafe", "Serve",
})
129 changes: 30 additions & 99 deletions capa/ir/_emit_wasm/_discovery.py
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,6 @@

from __future__ import annotations

import re

from .._nodes import (
Module, Instr, Value, Function,
Expand All @@ -41,6 +40,7 @@
)
from .._lower_pattern import PatStruct, PatOr
from .._capa_types import BUILTIN_CAPS
from .._python_only_caps import find_rejection
from .._emit_wit import _WIT_SIGNATURES
from .._walk import iter_functions, walk_instrs, walk_module
from ._layout import (
Expand All @@ -49,6 +49,7 @@
)



def _pattern_has_str_literal(pat) -> bool:
"""True iff ``pat`` carries a String literal anywhere in its
sub-pattern tree: a variant payload (``Ok("yes")`` / nested
Expand Down Expand Up @@ -469,107 +470,37 @@ def _discover(self, module: Module) -> None:
which read as "this is a backlog item" rather than the
permanent stance it actually is. The single early raise
is more honest and points the user at the correct
workaround (Python backend or refactor the call site)."""
self._reject_unsafe_signatures(module)
workaround (Python backend or refactor the call site).

2026-07: the same scan now covers every member of
``PYTHON_ONLY_CAPS``, so ``Serve`` gets the identical early,
site-listing rejection."""
self._reject_python_only_cap_signatures(module)
for fn in iter_functions(module):
self._discover_instrs(fn.body)

@staticmethod
def _type_name_tokens(ty: str) -> set[str]:
"""Every type-name identifier appearing in a CIR type
string, including generic args and tuple elements. A simple
word scan is sound for the Unsafe reachability check: the
only false positives would be a user type whose name happens
to be a substring of another, which the ``\\b`` boundaries
rule out."""
if not ty:
return set()
return set(re.findall(r"[A-Za-z_]\w*", ty))

def _unsafe_bearing_type_names(self, module: Module) -> set[str]:
"""Fixpoint set of struct / sum type names that
transitively reach ``Unsafe`` through a field or variant
payload, so a parameter of such a type is rejected even
when ``Unsafe`` never appears literally in the signature
(audit 2026-06-17 C5(b))."""
field_tys: dict[str, list[str]] = {}
for decl in module.types:
fields = getattr(decl, "fields", None)
if fields is not None:
field_tys[decl.name] = [f.ty for f in fields]
continue
variants = getattr(decl, "variants", None)
if variants is not None:
field_tys[decl.name] = [
pty for v in variants for pty in v.payload_tys
]
bearing: set[str] = set()
changed = True
while changed:
changed = False
for name, tys in field_tys.items():
if name in bearing:
continue
for ty in tys:
toks = self._type_name_tokens(ty)
if "Unsafe" in toks or toks & bearing:
bearing.add(name)
changed = True
break
return bearing

def _reject_unsafe_signatures(self, module: Module) -> None:
"""Surface ``Unsafe``-reaching parameters at discovery time
with a diagnostic that names the function, the parameter,
and the only two valid responses (run on the Python
backend, or remove the Unsafe argument). Scans both
top-level functions and impl methods.

Audit 2026-06-17 C5(b): the check walks each param type
RECURSIVELY through named struct fields, sum-variant
payloads, and generic arguments, so a param of a type that
merely *contains* Unsafe (``type Wrapper { u: Unsafe }``)
is rejected loud rather than slipping through to emit an
invalid ``call $py_import``. Mirrors the manifest's
reachability traversal: Unsafe is detected wherever it is
reachable through the type, not only as a literal head."""
unsafe_bearing = self._unsafe_bearing_type_names(module)

def reaches_unsafe(ty: str) -> bool:
for name in self._type_name_tokens(ty):
if name == "Unsafe" or name in unsafe_bearing:
return True
return False

offenders: list[str] = []
for fn in module.functions:
for p in fn.params:
if reaches_unsafe(p.ty):
offenders.append(f"{fn.name}({p.name}: {p.ty})")
for impl in module.impls:
impl_label = (
f"impl {impl.trait_name} for {impl.type_name}"
if impl.trait_name else f"impl {impl.type_name}"
)
for method in impl.methods:
for p in method.params:
if reaches_unsafe(p.ty):
offenders.append(
f"{impl_label}::{method.name}"
f"({p.name}: {p.ty})"
)
if not offenders:
return
sites = "\n - ".join(offenders)
raise WasmEmissionError(
"the Unsafe capability is intentionally not supported "
"on the Wasm backend (it grants raw pointer / FFI / "
"memory-map primitives that have no sandboxed Wasm "
"equivalent). Use the Python backend for these "
"functions, or refactor to remove the Unsafe "
"parameter.\n - "
f"{sites}"
)
def _reject_python_only_cap_signatures(self, module: Module) -> None:
"""Reject a program whose signatures reach a member of
``PYTHON_ONLY_CAPS`` (``Unsafe``, ``Serve``), naming the
capability, why it can never work here, what to do instead,
and the offending sites.

The scan itself lives in
[`_python_only_caps.py`](../_python_only_caps.py) because WIT
generation needs exactly the same predicate and is reachable
on its own (``capa --wit`` never runs this discovery pass).
Two copies of a security-relevant reachability check would
drift silently, so there is one.

Raising early matters: pre-2026-05 the rejection happened deep
in cap-method dispatch ("capability method Unsafe.alloc has no
WIT/Wasm encoding yet; widen the signature tables"), which read
as a backlog item rather than the permanent stance it is.
"""
found = find_rejection(module)
if found is not None:
_cap, message = found
raise WasmEmissionError(message)

def _discover_instrs(self, instrs: list[Instr]) -> None:
for instr in walk_instrs(instrs):
Expand Down
Loading