feat(caps): Serve, the tenth built-in capability (inbound connections, Python backend)#82
Merged
Merged
Conversation
Serve grants the authority to listen on a network address and accept
inbound connections. It is the language's first INBOUND authority:
every capability so far reaches out, Serve is reached.
Surface (connection-level, not HTTP-level -- the runtime binds,
accepts, and moves bytes; protocol parsing is ordinary Capa code in a
library, so a protocol bug is not a bug in the trusted computing base):
restrict_to(spec: String) -> Serve
allows(addr: String, port: Int) -> Bool
listen(addr: String, port: Int) -> Result<Unit, IoError>
local_port() -> Result<Int, IoError>
accept() -> Result<Int, IoError>
recv(conn: Int, max_bytes: Int) -> Result<List<Int>, IoError>
send(conn: Int, bytes: List<Int>) -> Result<Unit, IoError>
close(conn: Int) -> Result<Unit, IoError>
stop() -> Result<Unit, IoError>
Bytes are List<Int> masked to & 0xFF, matching String.bytes(). An
empty recv is EOF. Every fallible method returns Result<T, IoError>.
Sequential only: one open connection at a time, no threads and no
async. A second accept while a connection is open returns Err telling
the caller to close first. The project's async work stays gated
(docs/design/async-feasibility.md).
Nothing blocks forever: accept and recv are bounded at 30s, in the
spirit of Net.get's 10s and Proc.exec's 30s, and return Err on expiry.
Attenuation domain is the (bind address, port) pair, spelled
"addr:port", "addr:lo-hi" or "addr:*", with "*" also accepted as the
address. A bind must satisfy EVERY accumulated rule, the conjunctive
model Fs uses for path prefixes, so restrict_to can only ever narrow:
restrict_to("*:*") on an already-narrowed cap restores nothing. A spec
that does not parse denies everything, because ignoring it would
silently widen. Enforcement runs BEFORE the syscall, so a denied
address or port is never bound, not even transiently; the test proves
that by asserting the refused port is still free afterwards.
Python backend only. wasi:sockets is neither vendored nor reachable
from the wasmtime-py bindings the hosts use, so the Wasm emitter
rejects any signature reaching Serve at discovery time, listing every
offending site -- the Unsafe precedent, generalised: the reachability
scan and the reason table are now driven by a new PYTHON_ONLY_CAPS
registry rather than a hard-coded "Unsafe".
IFC: an inbound request is untrusted but NOT confidential, so it is
@public. Capa's lattice models confidentiality, not integrity or
taint; @secret would make echoing a request back to its own sender a
violation, which is the normal case for a server. Serve.send joins the
public-sink table (payload argument only).
The method is spelled send, not write, because _ifc_summary attributes
a sink to a capability BY METHOD NAME (no receiver type is available
there), which is sound only while sink names are unique per
capability. A first draft using write silently made every fs.write
report Serve as a reached capability; that regression was caught by
tests/test_unaudited_secret_sink_fact.py and the invariant is now
pinned by a dedicated guard instead of a comment.
Registry guards did their job. Adding Serve fired three of them, each
naming exactly what was missing: the WIT-generator guard (now derived
from PYTHON_ONLY_CAPS rather than spelling "Unsafe"), and the
discarded-call sweep coverage guard (Serve is the first Python-only
cap that HAS methods, so the sweep needed the exemption it already
expressed for py_import / py_invoke). The manifest, SBOM and policy
layers needed no work because they derive from CAPABILITY_NAMES;
tests verify that rather than assuming it.
Suite: 4314 passed / 18 skipped under pytest, 4297 OK / 18 skipped
under `unittest discover` (what CI runs). The new test module imports
no wasm tooling at module level and its six Wasm-rejection tests run
with wasmtime unavailable, verified against a blocked import.
Review follow-ups on the Serve capability. Two honesty fixes plus two
consistency fixes, no behaviour change to the happy path.
1. A comment described a mechanism that does not exist.
_emit_wit.py claimed Unsafe "can never reach WIT generation" because
the Wasm emitter rejects it, "so it never lands in used". That is not
what happens. `capa --wit` is a standalone path that never runs the
Wasm emitter at all. The truth is two different accidents:
- Serve DOES land in used (it has capability methods) and was
dropped later by the _KNOWN_CAPABILITIES guard in the interface
loop.
- Unsafe never lands in used, but because it is METHOD-LESS, so
there is no cap-method call for the collector to see. Its
authority goes through the py_import / py_invoke free functions.
Both were SILENT drops. `capa --wit` on such a program exited 0 and
printed a document that omitted the capability and whose world block
declared `export main: func()` while the real main took it as a
parameter -- a document whose entire purpose is to describe the
program's interface, describing a different program.
emit_wit now raises PythonOnlyCapabilityInWit up front. Raising rather
than documenting the gap: a program holding one of these capabilities
can never become a Wasm component, so there is no host that could
consume the WIT and nothing legitimate is lost. The CLI already turned
any compile_wit exception into `capa: --wit: <msg>` + exit 1, so the
diagnostic came for free. This also closes the identical pre-existing
hole for Unsafe.
The check scans SIGNATURES rather than used, which is what makes it
catch the method-less case that no used-based check ever could.
2. Serve.send could partially transmit and report a bare timeout.
sendall can push a prefix and only then raise; it does not report how
far it got. The class docstring said "send every byte", which is true
only on Ok. Documented that on Err the transmitted byte count is
UNSPECIFIED, that a naive retry can therefore duplicate a prefix, and
that the right response is to close the connection rather than resume.
The count is not reported because obtaining it would mean replacing
sendall with a manual send loop, which is a restructure of the send
path rather than a cheap win. The error causes now carry the same
warning, since the Result type cannot.
Also renamed the send error strings from "write ..." to "send ...",
left over from the earlier write -> send rename.
3. allows now agrees with listen on invalid ports.
The port-validity checks sat after the `if self._rules is None`
early return, so an unrestricted cap answered allows(addr, 65536) =
True while listen refused. Fail-safe, but a predicate documented as
"would listen(a, p) be permitted" that contradicts listen defeats its
own purpose. Hoisting alone would have produced "does not permit ...
current restrictions: unrestricted", so listen instead validates the
port explicitly first and reports "invalid port N" consistently
whether or not the cap is restricted.
4. The reachability scan now lives in one place.
WIT generation needs the same predicate the Wasm discovery pass uses,
and _emit_wasm imports from _emit_wit (so the dependency cannot go the
other way). Rather than duplicate a security-relevant reachability
check -- exactly the drift _capa_types' own docstring warns about --
it moved to capa/ir/_python_only_caps.py, with the reason strings, and
both callers raise in their own vocabulary. Fixed the stale references
to the old helper names in _capa_types and analyzer/_declarations, and
softened the "lists EVERY offending site" claim: a capability reached
only through self in an impl method is not listed as its own site
(the module is still rejected, because constructing the receiver needs
a capability-typed parameter, and that one IS listed).
Also noted, without changing it, that _trace.records() is one string
wide and therefore under-records Serve's (address, port) restriction
domain. Not widened: the triple shape is consumed by the property
suite's attenuation-replay machinery, which currently covers seven
capabilities correctly, and Serve's attenuation is tested directly and
more thoroughly than a replay could manage.
Suite: 4321 passed / 18 skipped under pytest, 4304 OK / 18 skipped
under `unittest discover`. The no-wasm collection is still clean (74
tests, 1 skip, the wasmtime-gated root-handle guard).
Adds the Serve surface alongside Net in the stdlib reference, a new IFC source row for Serve.recv and sink row for Serve.send (payload argument only, not the runtime-issued connection id), and the statement that the information-flow lattice models confidentiality rather than integrity or taint, so @public on an attacker-controlled inbound request asserts nothing about trustworthiness. Also records the sequential-only stance and why concurrency is deferred, the Python-backend-only limitation and its cause, and the attenuation grammar with its honest limits: IPv4 only, exact address matching, and the port-0 caveat where the check runs on the requested port so an ephemeral bind can land on a port the same rule would refuse by number. Several capability enumerations were stale and are corrected here: they predated Net, Db and Proc in places. docs/semantics.md is deliberately left alone: it declares the Agda model authoritative, and that model covers seven capabilities, so aligning its prose with the compiler would misrepresent what is machine-checked.
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| # to steal a bound port, which would undermine the whole | ||
| # point of a capability that names an address and port. | ||
| sock.settimeout(_SERVE_ACCEPT_TIMEOUT_SECS) | ||
| sock.bind((addr, port)) |
| program can no longer use the socket, which is true either way.""" | ||
| try: | ||
| sock.shutdown(socket.SHUT_RDWR) | ||
| except OSError: |
| pass | ||
| try: | ||
| sock.close() | ||
| except OSError: |
| out["stdout"] = _run_capa( | ||
| source, "echo_server.capa", Stdio(), Serve(), | ||
| ) | ||
| except BaseException as e: # pragma: no cover |
| def test_accept_timeout_returns_err_not_a_hang(self): | ||
| # Shrink the bound so the test is fast; the point is that the | ||
| # wait TERMINATES with an Err rather than blocking forever. | ||
| import capa.runtime._capabilities as caps |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Capa could make outbound requests but could not serve. This adds
Serve: the authority to listen on an address and port and do inbound connection I/O. It is the first capability added since the initial commit, and the first inbound data source the language has ever had.Groundwork landed separately in #81, which gave the capability set a single source of truth and the guards that make adding one safe. Those guards did their job here: three fired during this work, each naming what was missing.
Surface
Connection-level, not HTTP-level. HTTP parsing does not belong in the trusted runtime; it will live in a Capa library, which keeps the parser auditable and the host surface small.
restrict_to(spec),allows(addr, port)(no I/O),listen(addr, port),local_port(),accept(),recv(conn, max_bytes),send(conn, bytes),close(conn),stop(). Bytes areList<Int>masked& 0xFF, matchingString.bytes(). Every fallible method returnsResult<T, IoError>.Sequential is enforced rather than advised: a second
acceptwhile a connection is open returns an error.acceptandrecvare bounded at 30 seconds and return an error rather than hanging. Concurrency stays deferred, gated as described indocs/design/async-feasibility.md.Attenuation
The domain is the (address, port) pair, with specs
"addr:port","addr:lo-hi","addr:*"and"*"as an address. Narrowing is conjunctive, sorestrict_to("*:*")on an already-narrowed capability restores nothing. A malformed spec parses to a rule nothing can satisfy, becauserestrict_toreturns aServerather than aResultand silently ignoring a typo would widen authority. Enforcement happens before the syscall.Honest limits, documented: IPv4 only, address matching is exact string equality so
127.0.0.1andlocalhostdiffer, and because the check runs on the requested port, a":0"rule admits an ephemeral bind on a port the same rule would refuse by number.Information flow
Serve.recvis a@publicsource andServe.sendis a sink, attributed to the payload argument rather than the runtime-issued connection id. The docs now state plainly that the lattice models confidentiality, not integrity or taint:@publicon an attacker-controlled inbound request asserts only that it is not a secret whose disclosure the analysis must prevent, and asserts nothing about it being trustworthy.A method-name collision was found and fixed while building this. Sinks are attributed by method name with no receiver type, so an earlier
Serve.writemade everyfs.writereportServeas reached. Renamed torecv/send, and the invariant is now pinned by a guard rather than left as a comment.Backends
The Wasm backend rejects a program holding
Serve, loudly and listing every offending site, becausewasi:socketsis neither vendored nor reachable from wasmtime-py. This follows the existingUnsafeprecedent.Serveis classified erased rather than handle-bearing: handle-bearing describes Wasm lowering that never runs for a rejected capability, and erased fails loudly if the rejection ever developed a hole, whereas handle-bearing would occupy a slot with no root handle and fall back silently.--witalso rejects them now. It previously exited 0 and emitted a document declaringexport main: func()for a program whosemaintook aServeparameter, so it described a different program. The check scans signatures rather than collected methods, which also closes the identical pre-existing hole for the method-lessUnsafe.Verification
Adversarially reviewed. Attenuation monotonicity survived 36,248 checks across 147 malformed and adversarial specs with zero violations, and denials were confirmed as real enforcement by verifying the refused port stays bindable while the permitted one still binds. No program could be constructed that performs a
Serveoperation withServeabsent from its manifest, across helper, struct, trait, closure and dynamic-dispatch shapes. The originalwritecollision was reproduced to prove the fix is load-bearing, and the erased-capability fail-loud behaviour was verified by bypassing the rejection.python -m unittest discover tests(what CI runs) 4304 tests OK,pytest4321 passed, both with 18 skipped. With wasmtime blocked, every new module still collects and the Wasm-rejection tests still run.