This file lists what Resid's compiler, runtime and tools guarantee, how each guarantee is checked, and what is explicitly not guaranteed. Every "Guaranteed" row names the tests that fail if the guarantee breaks; run them with:
./boot.sh # self-compile fixed point
tests/conformance/run.sh # language cases, including err_* rejections
tests/runtime/run.sh # runtime properties (C harnesses over rt.ll)
tests/pkg/run.sh # package signing, trust and ceilings
tests/provenance/run.sh # signed provenance trailers and residc verify
tests/tls/run.sh # TLS server authentication over committed fixtures
tests/http/run.sh # lib/httpserv.resid request parsing and limits
tests/labels/run.sh # integrity labels and their explanations
- Untrusted library code compiled into a program: it must not gain capabilities (file system, processes, environment, arguments, network, terminal, clock, device, display, declassify) that the program did not grant it, or reach the runtime's memory internals at all.
- Untrusted package sources (a registry, a mirror, a copied archive): a dependency must be exactly what a trusted key signed, and must be the package that was asked for.
- Untrusted input data handled by a compiled program: it must not cause out-of-bounds memory access.
- A binary from elsewhere that claims to be a Resid build: its signature must be checked against a key the verifier already trusts, and what the verifier re-derived must be told apart from what the signer merely wrote down.
- Out of scope: an attacker who can write the local build tree (
target/, the key files, the compiler binary), timing and other side channels, and denial of service (a malformed input may abort the process).
| Guarantee | Enforcement | Tests |
|---|---|---|
No ambient authority: every capability family a function uses, directly or through anything it calls, wraps in a closure, or runs as a sort behavior, is granted by its own @requires or its enclosing sandbox. Authority enters a program only where main (or a test block) declares it. |
E0219, gk_authority in compiler/gcheck.resid |
err_authority_* (provider, builtin, call, closure, lambda, method sugar, behavior, f-string Show, test block), authority_granted |
Effectful runtime builtins are capabilities too: TCP is network, the ptrace debugger is process, TTY queries and raw mode are terminal. The runtime's git rev-parse helpers (resid_git_rev, resid_git_branch) are reachable from no program: git is not a family, the git. provider is unbound and the builtins are not callable. |
gk_builtin_family, gk_unknown_family |
err_authority_ambient_builtin, term_requires_missing, readline_requires_terminal, err_git_family, err_git_provider_unreachable, err_git_builtin_unreachable |
terminal(readonly) covers the TTY and window-size queries only; raw mode and restoring it are writes, at compile time and in the force-time guard (terminal!). |
gk_builtin_write, provider_family_of_line |
term_readonly_write, term_readonly_query |
network(readonly) covers connecting out, listening on 127.0.0.1, accepting, sending, receiving and closing. Binding a listener to any other address (resid_tcp_listen_at, http_listen_at) exposes a port to other machines and is the one network write, at compile time and in the force-time guard (network!). A server's worker regions can therefore be spawned with network(readonly) while only the code that binds holds network. The TCP verbs accept only AF_INET/AF_INET6 sockets, so a network grant cannot drive a display connection or any other Unix-domain socket it did not make itself; accept refuses a descriptor past the 65536-entry deadline table, so every connection it hands out has its deadline. Unix-domain sockets (resid_unix_*) are the local form under the same family: resid_unix_listen is a write (it exposes a socket to other processes), the rest are reads. The runtime fixes the policy: the socket is 0600 in a directory owned by the user with no group or other bits (made 0700 when missing, else refused), an existing file is replaced only if it is the user's own dead socket, accept drops and connect refuses a peer of another uid (SO_PEERCRED), every descriptor is close-on-exec, and the unix verbs work only on descriptors they made (a per-fd mark), so they cannot reach a display socket either. |
gk_builtin_write, gk_direct, provider_family_of_line |
err_network_readonly_listen, network_readonly_loopback |
Reading the clock is clock, an effect like any other: under Laws 8 and 9 the answer to "what time is it" is knowledge the program does not have, so it arrives only through an authorized provider and never ambiently. clock(readonly) covers now_ns, now_sec and monotonic_ns; sleep_ns consumes time rather than observing it and so needs the full grant, at compile time and in the force-time guard (clock!). lib/clock.resid is the standard library's only clock surface, and the rest of the date and time library needs no grant at all — converting, formatting and zone-resolving a timestamp you already hold is arithmetic. |
is_prov_family, is_write_verb, provider_family_of_line |
err_authority_clock, err_clock_readonly_write, authority_clock_readonly, dt_clock, tests/runtime/cap_guard.c |
The display is a capability like any other: connecting to a window server, sending and receiving on it (descriptors included), waiting on it and mapping shared memory for a frame are the resid_disp_* builtins, needing display. The family has no modes (display(readonly) is refused, E0213): connecting to a window server, opening a window, drawing into it and reading from it all act on what the program itself put on screen. It reaches nothing outside this machine's own session — a DISPLAY naming another host is refused — and every display verb accepts only Unix-domain sockets (checked with getsockopt SO_DOMAIN). A shared mapping is a handle: an index into a runtime table with a generation, never an address, so a forged, stale or freed handle is refused and never dereferenced. A descriptor sent with resid_disp_send must be the descriptor of a live shared mapping, else it is refused; closing a received descriptor clears its received mark; the descriptor queue and the mapping table are locked across spawn regions. One explicit exception, part of connecting: resid_disp_x11_auth reads the X authority file ($XAUTHORITY, else ~/.Xauthority) under display alone, with no filesystem grant; it reads only a regular file of at most 1 MB and returns only the 16-byte MIT-MAGIC-COOKIE-1 for this display. |
gk_builtin_family, gk_unknown_family, gk_display_moded, provider_family_of_line |
err_display_ungranted, err_display_readonly, display_transport, tests/runtime (display.resid, display_shm.c) |
A frame is written into its shared mapping, never outside it: resid_disp_shm_put (a list element per byte) and resid_disp_shm_put32 (an element per 32-bit pixel, from any element on) refuse a handle that is not a live mapping, a negative offset, bytes that would run past the mapping's end and, for put32, elements outside the list. Both bound checks are written so they cannot overflow. |
rt_disp_shm_put, rt_disp_shm_put32, shm_ok in runtime/rt/unix.resid |
tests/runtime (display.resid: past end, past the list, negative, freed handle) |
Publishing a secret is a capability: declassify(s, "reason") needs the mode-less family declassify, carried to every caller (E0219) and bounded like any family; declassify(readonly) is refused (E0213). The reason must be a non-empty string literal (E0251), and each call is an effect in the graph artifact (declassify.<reason>, capability declassify). The grant is also checked at force time, like a provider call: sec_erase marks each declassify left after reduction, and every function, lambda and spawn body holding one calls resid_cap_check("declassify") in its entry block (after a sandbox's resid_cap_enter, before a self-recursive loop's head; authority is fixed for one call), so a closure that declassifies, run inside a spawn list or sandbox ceiling without declassify, aborts (a spawn region fails) instead of publishing. A declassify folded to a literal leaves no code and no check. |
gk_builtin_family, gk_unknown_family, sec_declassify_moded, sec_call, ga_effect, sec_erase (sec_known_under), lw_declassify_check, rt_cap_check |
err_declassify_ungranted, err_declassify_moded, err_declassify_reason, secret_ok, secret_declassify_granted, secret_declassify_spawn_dropped, secret_declassify_sandbox_dropped, secret_known_declassified |
A Secret(T) never decides control flow, an address or a public result: conditions, match, logic, comparisons, / and %, indexes, range bounds and shift amounts are refused (E0255); checked + - * are refused because their overflow abort branches (E0254); bitwise operators, public shifts and wrapping_* keep the result secret. A secret cannot wrap a type whose shape is control or identity (E0253), nor a Bytes or Bytes(N) in any written or inferred type (E0253): a heap Bytes ends at its first zero byte, so its .len() and its conversions scan the bytes, a branch on each; secret byte strings are List(Secret(UInt(8))). |
sec_bin, gk_cond, gk_ifx, gk_match, gk_index, sec_lift, sec_wrap_err, sec_bytes_err (written types in gm_unknown_types, inferred ones in sec_wide_scan) |
err_secret_if, err_secret_ifx, err_secret_while, err_secret_match, err_secret_and, err_secret_compare, err_secret_div, err_secret_checked_add, err_secret_shift_amount, err_secret_index, err_secret_wrap_option, secret_index_public, err_secret_bytes, err_secret_bytes_fixed, err_secret_bytes_generic |
A secret never leaves the checked program unannounced: it cannot be a provider argument (E0255; write_secret takes a declassified value, so persisting key material needs the grant and is on the graph), a spawn region's result (E0255), or a Map key or Set element in any written type (E0253). |
gk_provider, gk_expr0 (spawn), sec_key_err in gm_unknown_types |
err_secret_provider_write, err_secret_spawn_result, err_secret_map_key, err_secret_set_element, err_secret_nested_map_key, secret_write_declassified |
A program that handles secrets runs its allocator in secret mode, switched on before main (the compiler emits the call when the reduced program contains a secret): every heap, region, thread-stack and thread-local mapping is MADV_DONTDUMP, and so is the initial process stack (its [stack] mapping in /proc/self/maps; without /proc it is left unmarked); freed small and big blocks are zeroed before they can be reused, and freed region pages are zeroed before they are cached for reuse or zero-filled by MADV_DONTNEED. Core dumps are off for the whole process, since a core also holds what no mapping flag covers (registers, among them the vector registers holding AES round keys, and static data): the mode sets PR_SET_DUMPABLE 0 and RLIMIT_CORE {0, 0}, so a fatal signal (SIGSEGV on a stack overflow, SIGBUS) leaves no core whatever core_pattern says, and an abort prints its message and exits with status 134 instead of raising SIGABRT. Not dumpable also means no process of the same user can ptrace-attach to the program or open its /proc/<pid>/mem (gdb -p, strace -p): intended. Even a debugger that started the program and traces it from exec loses access: the kernel refuses a tracer's reads and writes of a non-dumpable process's memory, so resid-debug (and gdb) can stop a secret-mode program only before main switches the mode on; resid-debug says so and stops instead of reporting zeros. The core limit is inherited, so processes the program starts dump no core either. The mode is never switched off or the process made dumpable again; device and native hosts are still started by the program itself: a host does not read the program's executable, and in secret mode no host starts without the Yama ptrace policy (Device access, below). Mappings are also locked on fault (mlock2 MLOCK_ONFAULT), as far as RLIMIT_MEMLOCK allows: past it they stay swappable, and each refused lock is counted (resid_secret_unlocked). Locking is best effort; the zeroing and the core rules above are not. |
rt_secret_mode_set, stack_nodump, sys_mmap, sec_lock, c_free, big_free, pages_give, pages_take, c_libc_abort (runtime); main_entry_ir, td_main_ir, sec_graph_has (compiler) |
tests/runtime/secret_lock.c (a lock refused under RLIMIT_MEMLOCK 0 is counted), tests/runtime/secret_zero.c (with a control: without the mode the bytes survive), tests/runtime/secret_nodump.c (not dumpable, the core limit, the stack's dd flag, abort as exit 134, SIGSEGV without a core; controls without the mode), tests/runtime/nodump/ (compiled programs: a secret program's checked overflow exits 134 with its message, its stack overflow dumps no core, a public one still raises SIGABRT), tests/graph/run.sh (resid-debug refuses a secret-mode program by name) |
The builtins of secret values cannot be redefined (E0259): a program's function named secret, declassify, classify, secret_split, secret_join or ct_select would replace the builtin in every module, so a dependency could otherwise turn secret or declassify into anything. |
sec_reserved in gm_unknown_types |
err_secret_reserved_name |
| A secret integer wider than 32 bits is never stored in a list, builder, vector, map or set (E0258), checked on written types and on every type the checker gives an expression (programs with secrets log them), so generic copies and inferred types are covered. List integers of 2^54 or more are boxed, a choice made on the value; secret bytes are UInt(8) and wide secrets live in records and parameters. | sec_wide_err, sec_wide_scan (in gk_finish), the type log enabled by sec_graph_has |
err_secret_wide_list, err_secret_wide_elements, err_secret_wide_generic |
ChaCha20, Poly1305 and the ChaCha20-Poly1305 AEAD have one implementation (lib/chachag.resid), generic over Word(W, B) (32-bit words, bytes) and Wide512(P, B) (Poly1305's accumulator, Int(512) or Secret(Int(512)), kept in parameters, never in a list); lib/chacha.resid's API is the public copy. Nonce, counter, AAD, lengths and the received ciphertext are public; the reduction mod 2^130 - 5 subtracts p under a sign mask behind ct_hide; the open verdict is one bit published through CtSame(B) (ct_equal at public bytes, ct_eq at secret bytes, so the secret copy needs @requires(declassify)). Checked against RFC 8439 §2.5.2 and §2.8.2, the public copy against Wycheproof, and both copies under valgrind with the key and plaintext marked secret. |
lib/chachag.resid, lib/chacha.resid, lib/word.resid (Wide512), lib/crypto.resid (CtSame), sec_liftable |
secret_chacha20poly1305, chacha20poly1305_in_resid, tests/ct/run.sh (chacha, chacha-secret, chacha-open-secret, poly1305-secret), tests/crypto (Wycheproof ChaCha20-Poly1305) |
AES-128/192/256, AES-GCM (any IV length) and AES key wrap have one implementation (lib/aesgcmg.resid), generic over Word(W, B) and Block128(X, W, B): 128-bit blocks (UInt(128) or Secret(UInt(128))) and the AES-NI round keys live in records and parameters, the schedule is a list of 32-bit words; lib/aesgcm.resid's API is the public copy. On AES-NI / AESE and PCLMULQDQ / PMULL the rounds and GHASH use aesni_enc_round, aesni_enc_last_round and gf128_mul_hw, which take secrets (constant-time instructions); otherwise the S-box is computed four bytes per word (an inverse in GF(2^8) as x^254, then the affine map) and GHASH multiplies with masks. IV, AAD, lengths, the received ciphertext and the wrapped key are public; a GCM plaintext or ciphertext over 2^36 - 32 bytes (SP 800-38D, where the 32-bit block counter would wrap and reuse keystream) is refused, which today no test reaches (the cap is checked in ag_seal_g and ag_open_g, past the 4 GB memory budget); GCM open and key unwrap publish one bit through CtSame(B) (the secret copies need @requires(declassify)). Checked against the GCM spec's test cases 4, 6, 10 and 16 and RFC 3394 at both types and on both paths, the public copy against Wycheproof, and the secret copy under valgrind on both paths with the key and plaintext marked secret. |
lib/aesgcmg.resid, lib/aesgcm.resid, lib/word.resid (Block128), sec_liftable |
secret_aesgcm, aes128gcm_in_resid, tests/ct/run.sh (aes-gcm-secret-*, aes-gcm-open-secret-*, aes-kw-secret-*, aes-unwrap-secret, aes-sw, aes-dec, aes-gcm, aes-kw, ghash, ghash-sw), tests/crypto (Wycheproof AES-GCM, key wrap) |
X25519 (RFC 7748) has one implementation (lib/x25519g.resid), generic over Wide512(P, B): field elements mod 2^255 - 19 are Int(512) or Secret(Int(512)) values kept in parameters (never in a list), always reduced below p; reduction subtracts p under a sign mask behind ct_hide, and the Montgomery ladder's conditional swaps are xor masks built from the scalar bit. lib/x25519.resid's API is the public copy. The private scalar is secret; the peer's public key, the field constants and the inversion exponent are public. Two facts are published, each through a behavior whose secret instance declassifies (so the secret copy needs @requires(declassify)): whether the shared secret is all zeros (CtSame(B)) and the public key derived from a private key (X25519Pub(B)). Checked against RFC 7748 §5.2 and §6.1 at both types, the public copy against Wycheproof, and both copies under valgrind with the scalar marked secret. |
lib/x25519g.resid, lib/x25519.resid, lib/word.resid (Wide512), lib/crypto.resid (CtSame) |
secret_x25519, err_secret_x25519_public, x25519_in_resid, tests/ct/run.sh (x25519, x25519-secret), tests/crypto (Wycheproof X25519) |
P-256 and P-384 key derivation, ECDH and ECDSA signing have one implementation, generic over P256Word(F, B) / P384Word(F, B) (field elements UInt(576) / UInt(832) or Secret(UInt(576)) / Secret(UInt(832)), kept in records and parameters, never in a list), generated into lib/p256.resid and lib/p384.resid by tools/gen_nistp.py: Montgomery arithmetic with masked conditional subtraction, the complete RCB16 formulas, a fixed-length ladder with masked selection, Fermat inversion of the nonce with the fixed public exponent n - 2, and the RFC 6979 nonce as an HMAC-DRBG over the generic HMACs (lib/sha256g.resid, lib/sha512g.resid) keyed by the secret key. lib/ecdsa.resid's ecdsag_*, ec_public_keyg and ecdhg take the key as List(B); its List(Int) API is the public copy, and verification (public inputs only) runs on it. A signature, a public key and the verdicts "key usable" and "point finite" are published through the behavior's open verb (ct_public, plus declassify at secret types, so those secret copies need @requires(declassify)); an ECDH shared secret stays secret. A secret cast that keeps every value stays secret; any other is refused (E0255). Checked against RFC 6979 A.2.5/A.2.6 and RFC 5903 §8.1 at both types, the public copy against Wycheproof ECDSA/ECDH and the RFC 6979 vectors, and both copies under valgrind with the key marked secret. |
tools/gen_nistp.py, lib/p256.resid, lib/p384.resid, lib/ecdsa.resid, sec_cast |
secret_ecdsa, secret_widening_cast, err_secret_narrowing_cast, tests/ct/run.sh (p256-sign, p384-sign, p256-ecdh, p384-ecdh, p384-public, p256-secret-sign, p384-secret-ecdh, p384-secret-public), tests/crypto (Wycheproof ECDSA/ECDH, RFC 6979) |
Ed25519 key generation and signing have one implementation (lib/ed25519g.resid), generic over Wide512(P, B) (field elements below p and scalars as Int(512) or Secret(Int(512)), kept in records and parameters, never in a list) and Word64(W, B) (SHA-512 of the seed); lib/ed25519.resid's API, its field and point arithmetic (shared with lib/x25519.resid) and verification are the public copy. Seed, expanded key, nonce r and the scalar arithmetic with a are secret at secret types; field reductions subtract under a sign mask behind ct_hide, and the scalar multiplication is a double-and-always-add ladder that picks the sum or the double with a mask from the scalar bit (no table, index or branch). The public key and the signature leave through Publish(B) (lib/word.resid: a copy at public bytes, declassify at secret bytes), so every caller of the secret copy needs @requires(declassify); the compiler's provenance signing (write_provenance, residc keygen) holds its seed as List(Secret(UInt(8))) and carries the grant up to main. Checked against RFC 8032 §7.1 (both copies), the public copy against Wycheproof EdDSA, and both copies under valgrind with the seed marked secret. |
lib/ed25519g.resid, lib/ed25519.resid, lib/word.resid (Publish, Wide512.p_mul256), lib/cose.resid (cose_sign1), compiler/driver.resid (write_provenance, cmd_keygen), scope_arith_builtin (ct_hide/ct_select are register-only, so masked field code gets no region scope) |
secret_ed25519, err_ed25519_secret_ungranted, ed25519_sign_in_resid, ed25519_verify_strict, tests/ct/run.sh (ed25519-sign, ed25519-secret-sign, ed25519-secret-pub, x25519), tests/crypto (Wycheproof EdDSA), tests/provenance |
HPKE (RFC 9180) has one implementation (lib/hpkeg.resid), generic over the byte type and the word behaviors of its primitives (Word, Word64, Block128, Wide512): the labeled HKDF over HKDF-SHA256/384/512 (lib/sha256g.resid, lib/sha512g.resid), the three KEMs -- DHKEM(X25519, HKDF-SHA256) over lib/x25519g.resid, and DHKEM(P-256, HKDF-SHA256) and DHKEM(P-384, HKDF-SHA384) over lib/ecdsa.resid's ecdhg / ec_public_keyg (the generic curves) -- the key schedule in all four modes, the nonces, seal and open over AES-128/256-GCM and ChaCha20-Poly1305, and the exporter; lib/hpke.resid's API is the public copy, and no suite has a public-only path. At secret types the private keys, the shared secret, the PSK, the key schedule's secret, key, base_nonce and exporter secret, each nonce and the plaintext are secret; public keys, enc, info, psk_id, the AAD, the received ciphertext and the sequence number are public. The AEADs take the nonce as secret bytes (aes_gcmg_seal_ivb, chacha20poly1305g_seal_nb, and their opens). Published by design, each through a behavior whose secret instance declassifies (so the secret copy needs @requires(declassify)): derived public keys (X25519Pub(B), or the curve's open verb), the all-zero DH check and the tag verdict (CtSame(B)), and for the NIST curves whether a derived candidate or a peer key is usable. Checked against RFC 9180 A.1, A.2 and A.3 (DHKEM(P-256)) at both types, DHKEM(P-384) in auth mode at both types against each other, the public copy against all of the RFC's vectors, and the secret copy under valgrind with the recipient key, or the ephemeral key and plaintext, marked secret. |
lib/hpkeg.resid, lib/hpke.resid, lib/ecdsa.resid (ecdhg, ec_public_keyg), lib/aesgcmg.resid (*_ivb), lib/chachag.resid (*_nb) |
secret_hpke, secret_hpke_nist, tests/ct/run.sh (hpke-open, hpke-open-secret, hpke-open-secret-chacha, hpke-seal-secret, hpke-seal-secret-chacha, hpke-p256-secret), tests/crypto (hpke_rfc9180.txt, hpke_p384_pyca.txt) |
The TLS 1.3 key schedule (RFC 8446 §7.1), Finished (§4.4.4) and AES-128-GCM record protection (§5.2) have one implementation (lib/tls.resid's tlsg_*), generic over the byte type, on the generic HKDF-SHA256 and AES-GCM with the nonce in bytes B (aes_gcmg_seal_ivb, aes_gcmg_decrypt_ivb); its List(Int) API is the public copy. The server and client run the secret copy: the x25519 ephemeral key and shared secret (lib/x25519g.resid; an all-zero shared secret is refused), the early, handshake and master secrets, the traffic secrets, the finished keys, and the record keys and IVs (TlsKeys) are List(Secret(UInt(8))), and each record's nonce (IV xor sequence number) is computed in secret bytes. The server's signing key (ServerKey) is secret from the moment its file is read (tls_key_parse, see the key-loading row) and CertificateVerify is signed with ed25519g_sign / ecdsag_sign_digest. Published by design: the key share, the signature, and through TlsPublish(B) (one declassify each, with its reason) record ciphertext, an authenticated record's plaintext handed to the application, and the Finished MAC; a record's tag and the peer's Finished publish one bit through CtSame(B). So every function and program that runs a handshake or a record carries @requires(declassify) (E0219; spawn lists included, E0214). Checked against the RFC 8448 §3 trace at both types (shared secret, every secret, key and IV, both Finished, the client's protected Finished and first application record), live handshakes against this repository's client and openssl s_client, the secret copy under valgrind with the shared secret, or the record key and IV, marked secret, and a whole in-process handshake and record exchange (ts_server_start_with, ts_server_finish, tls_client_finish over a socketless TsIn) under valgrind with both ephemeral keys and the signing key marked. Every publish point (TlsPublish, Publish, X25519Pub) marks what it publishes defined with ct_public, as the curves' open verbs and ct_eq already did, so code that branches on published bytes (a peer parsing a share, the inner content type) is not reported while a branch on anything still secret is; without it the same handshake reports thousands of such branches. |
lib/tls.resid (tlsg_*, TlsPublish, TlsKeys), lib/tlsserver.resid, lib/tlsclient.resid, lib/tlswire.resid, lib/tlskey.resid |
secret_tls_key_schedule, err_secret_tls_record_ungranted, tests/ct/run.sh (tls-key-schedule-secret, tls-record-seal-secret, tls-handshake-secret), tests/tls/run.sh |
SHA-512, SHA-384 and HMAC-SHA-512/384 are generic over Word64(W, B) (lib/sha512g.resid), with the state in a record and the schedule in a 16-word parameter window so no 64-bit secret word is stored in a list (where values of 2^54 or more are boxed, a branch on the value). Checked against the existing implementations and RFC 4231. |
lib/sha512g.resid, lib/word.resid |
secret_sha512, tests/ct/run.sh (sha512-secret, hmac512-secret) |
SHA-256, HMAC-SHA-256 and HKDF-SHA-256 have one implementation, generic over Word(T) (lib/word.resid): the copy at Secret(Int) is checked by the compiler like any code on secrets, and the copy at Int is lib/crypto.resid's software block function. Both are checked against RFC 4231 / RFC 5869 and the existing implementation; the secret copy runs under valgrind with no secret-dependent branch or address. |
lib/sha256g.resid, lib/word.resid |
secret_hmac_hkdf, tests/ct/run.sh (sha256-secret, hmac-secret, sha256-sw), tests/crypto |
A secret the compiler knows is refused (E0250): it would be in every copy of the binary. Known means built only from literals, builtins outside the runtime's own and randomness, and calls of functions that read nothing at run time (no provider, runtime builtin, closure or spawn, transitively) -- whether or not the reducer computed it, so --reduce-budget 0 and --no-reduce do not let one through. The same holds through functions: one that passes its parameters, through such steps, to secret(...) or to another such function (mk(0x5EC2...) where mk returns secret(x + 1)) makes a known secret when every argument is known. A call written directly inside declassify(...) is accepted, which states that the value is public; so is one in a test block, or in a function marked @fixed_secrets in a file under tests/ or named *_test.resid (fixed test keys); the mark elsewhere is refused. Not covered: a known value reaching secret(...) through a local binding of a parameter, a closure, or a method call; and classify, which claims no secrecy. |
sec_known_check, sec_pure_fix, sec_wrap_fix, sec_wrap_use (run on the reduced graph before lowering) |
err_secret_known, err_secret_known_folded, err_secret_known_unreduced, err_secret_known_wrapper, err_fixed_secrets_outside, fixed_secrets_ok_test, secret_known_declassified |
ct_select(c, a, b) on a Secret(Bool) selects with masks behind an empty-asm barrier, never a branch or select; ct_eq in lib/crypto.resid folds every byte into one secret word, reduces it to one bit and publishes only that bit, under the declassify grant. Both are checked under valgrind on the optimized binary. |
sec_select, lw_ct_select, ct_eq |
secret_ct_select, secret_ct_eq, err_ct_eq_ungranted, err_ct_select_public_cond, tests/ct/run.sh (ct-select, ct-eq) |
A secret is never observed through a behavior: the structural Show refuses any type holding one and names the field path (E0256); Show, Serialize, Hash, Eq and Ord are never given for a secret, whether declared, asked by a verb or needed by a generic copy (E0257); a type's own Show is checked like any function. After checking, Secret(T) is erased and lowers exactly as T. |
sec_path, gm_find_inst, gm_builtin_inst, gm_inst_err, sec_obs, sec_erase |
err_secret_show, err_secret_show_field, err_secret_show_verb_field, err_secret_show_instance, err_secret_wrapper_instance_leak, err_secret_serialize, err_secret_hash, err_secret_generic_show, secret_wrapper_instance_declassified |
A program never leaves the terminal in raw mode: the runtime restores the saved settings when main returns and on an uncaught abort. |
term_exit in runtime/rt/term.resid |
tests/runtime (readline on a pty) |
lib/readline.resid never sends a control character from a completion candidate or a prompt to the terminal: C0, DEL and C1 characters are shown as ?. |
lib/readline.resid |
tests/runtime (readline on a pty) |
Generics and behaviors add no authority. A behavior's function runs where the behavior is used, so its capabilities flow to the caller. A generic function's own body is checked against its own @requires; each copy made for concrete types is granted exactly what it and the instances it calls need, and the concrete caller must hold that (E0219 names the copy, e.g. label(Task)). A copy of a generic declared inside a sandbox is placed inside the same sandbox, so the ceiling still bounds it (E0211, E0218). |
gk_auth_all (copies), gm_wrap in compiler/mono.resid |
err_generic_authority, err_generic_sandbox, generic_authority_granted |
The runtime's memory internals (arena and bulk push/pop, persist copies) and the resid_raw_* runtime primitives (raw memory, atomics, system calls, static storage, function addresses), which bypass every check above, are not part of the language. Two locks: the driver honors --runtime-internals only when the entry file is compiler/driver.resid or under runtime/rt/ (no .. in its path); and every use (a call, or an @export/@import annotation) must come from a file under the entry's own tree's compiler/ or runtime/rt/ (the prefix before the entry's compiler/driver.resid or first runtime/rt/), reached without .. and never in lib/, found through the import source map (E0220). A lint test keeps lib/ and tools/ free of internal names. |
gk_internals_at, gk_internal_file, gk_internal_root, driver rentry |
err_runtime_internal, err_runtime_internal_outside, tests/runtime (primitives, lib/ import, a file outside the entry's tree, lint) |
Read-only grants cover reads only, including a write reached through a callee. A closure value is not a callee here: its needs are charged where the lambda is made, and a function that only calls a closure it was given is bounded by its own @requires statically, not at run time. To bound what a passed-in closure may do, call it inside a sandbox (or a spawn list), whose runtime frame the force-time guard checks. |
E0219 modes | err_authority_readonly_write |
A sandbox or spawn capability list is held to the same spelling as @requires: a mode on a mode-less family (display, declassify, provision, assume, native_<m>) or an unknown family is refused (E0213). |
gk_caps_err |
err_sandbox_moded, err_spawn_moded |
Sandboxes only narrow: nested sandboxes meet, and sandbox () grants nothing. |
ceil_enter, meet_caps in compiler/typecheck.resid |
err_sandbox_empty, err_sandbox_nested_meet |
import "m" @requires(caps) compiles m and its imports inside sandbox (caps); re-importing an unattenuated module attenuated is an error. |
imp_resolve_lines_a |
err_import_attenuated, import_attenuated_ok |
A manifest dependency compiles inside the capabilities its consumer's manifest lists for it. |
depmap name::root::caps + imp_resolve_lines_a |
err_manifest_ceiling, manifest_ceiling_ok, tests/pkg (ceiling) |
The standard library is compiled outside every dependency or attenuated-import sandbox (under an absolute stdlib root): a stdlib file a sandboxed module reaches through its own files is resolved first, at the importer's level. The module's calls into it are bounded transitively (E0211, E0215) and by the force-time guard, as for a stdlib file the main program happened to import first; uncalled stdlib code no longer counts against a ceiling. (Before this, where stdlib text landed depended on import order, and a device-only dependency was refused for ct_eq in crypto.resid, which it never called.) |
imp_std_reach, imp_hoist_std in imp_resolve_lines_a |
tests/pkg (pkg_stdlib_outside_sandbox, pkg_device_ceiling) |
A ceiling must be grantable under the manifest's [capabilities] grant with its mode: a read-only grant does not cover a full entry. |
cap_grantable in tools/resid-manifest.resid |
tests/pkg (read-only grant covered a full entry) |
| Authority only narrows down the dependency tree: a dependency's ceiling for its own dependency must be grantable under the ceiling it was given. | collect_sub_deps_at |
tests/pkg (transitive ceiling) |
| A dependency declared by two packages gets the meet of every ceiling given to it, whichever declaration is reached first, and every pinned key any declaration names is verified. (Before this, the first declaration reached won, so a dependency could widen a sibling's ceiling or drop its pin.) | merge_deps, meet_caps, verify_all_pinned_keys over every declaration |
tests/pkg (narrower ceiling ignored, second pin ignored) |
A spawn's child, and everything it calls, gets only the spawn's listed capabilities -- including a closure made outside the spawn and called in its body by the name it is bound to (the binding is immutable, so the call runs that lambda). A closure reached any other way (passed to a function, held in a value) is bounded at force time (next row). |
E0214 in gk_auth_spawns (gk_closure_facts); the worker runs in its own runtime frame |
err_spawn_body_provider, err_spawn_closure_provider, err_spawn_closure_write, err_spawn_* |
A running spawn region shares nothing mutable with its parent: captured maps are frozen and captured records marked shared at capture, a captured handle is moved (the parent may not use it again), and every region is joined before the scope that started it ends. |
lw_share_caps, gk_moved_use, lw_fut_waits |
spawn_concurrent, err_spawn_handle_moved |
Force-time guard: every provider call is checked before it runs against the thread's sandbox frames; writes need a grant that is not read-only. That covers the bodies of named functions, spawns and lambdas alike: a closure runs under the frames where it is called, not where it was made, so one made in main and run inside a sandbox ceiling or a spawn list that drops its family aborts (a spawn region fails). The static checks attribute a lambda's needs to the function that makes it and cannot follow a closure value across a sandbox or spawn boundary, so for closures this guard is the enforcement, not only defense in depth. Native calls check in their stubs. |
resid_cap_check, capinject_at (in lw_fn_body, lw_spawn_mode, lw_lambda), the native.resid stubs |
tests/runtime/cap_guard.c, sandbox_force_time_guard_present, lambda_caps_spawn_dropped, lambda_caps_sandbox_dropped, lambda_caps_spawn_dropped_ui and lambda_caps_sandbox_dropped_ui (terminal, including raw mode under terminal(readonly), and display), lambda_caps_sandbox_abort, lambda_caps_native_spawn |
Effects that are not capabilities (ambient by design): writing to
stdout/stderr, reading stdin (resid_read_line, resid_read_byte), OS randomness, and the runtime's own
allocation and aborts. There is no extern and no in-process FFI: a
program reaches the OS only through providers and the builtins above.
Code in another language runs only as a native module (below), in a
process that cannot reach the OS at all.
| Guarantee | Enforced by | Tests |
|---|---|---|
Every builtin a program calls has an integrity entry: its result is either acquired from outside (External) or computed from its arguments; a builtin with no entry is refused (E0271), never defaulted. Provider calls, the runtime's socket, terminal, clock, input, randomness, device, display and ptrace builtins, native module calls, spawn results and CPU feature queries outside the standard library are External. |
lb_builtin, lb_mcall, lb_apply in compiler/labels.resid |
tests/labels/run.sh (source-table compares the checker's builtin list with the table; basic, loops, cpu) |
A value chosen by outside data is External even when built from constants: if/match results, returns under a condition (and the early return of ?), and iterations of a loop over outside data or one a break under outside data stops; across calls through each function's flow summary (which parameters reach or select its result), with recursion to a fixed point; a closure carries what it captures and acquires. |
lb_choose, lb_match, lb_s (ret), lb_loop, lb_fn, lb_fix, lb_lambda |
tests/labels/run.sh (select, calls, closures, loops) |
| `resid-why --label NAME | FILE:LINEshows a value's label and, for an External one, the path from where outside data entered, read from thelabel` field of the graph artifact. |
lb_text, ga_label_out (compiler/gart.resid), gn_label_show (lib/kgart.resid) |
| A layout type's generated parser is total: every read and slice is preceded by a length check against the given bytes (a signed length is checked non-negative, and a length is compared as UInt(64) before it becomes an Int), so any input gives a value or a DeviceError, never an abort or an out-of-bounds read; le/be parses consume their input exactly. | ly_parse_fields, ly_gen_type in compiler/layout.resid | layout_parse (truncation at every field, failed checks, constructor errors), the tpm_wire oracle in tests/labels/run.sh (prefixes and byte mutations against tw_take_2b/tw_num) |
| c_abi offsets and sizes are the C compiler's: natural alignment, tail padding, flexible array members, nested records. | ly_align, ly_type_size, ly_off_at | tests/labels/run.sh (c_abi x86_64-linux-gnu, c_abi aarch64-linux-gnu, against clang's offsetof/sizeof) |
| A record literal sets every field of its type (E0001): an unset field was read as whatever its allocation held. | gs_unset in gk_struct_seen (compiler/gcheck.resid) | err_record_field_unset (conformance); the compiler's own source and every library and example check clean (the one omission found, in the reducer's gy_fres, is fixed) |
| Layout declarations are refused when lengths look forward, a variable length is not last under c_abi, a field type is unsupported, a nested type differs or contains itself (E0272), a Secret field has a check (E0273), or a field holds a runtime-built type (E0274). | ly_check, ly_check_all, ly_depth | err_layout_* |
| Keys must be unpredictable (E0270, reported as a warning during the rollout): every argument reaching a @key parameter is checked for min(length, 32) bytes from draws, provisioned keys or reviewed derivations, counted once per source node, with every source a copy of which reaches declassify counted zero; own keys take only draws; public keying copies are refused outside tests. A known-empty key is not reported (keying primitives refuse it at run time). | compiler/ekey.resid (ek_reviewed_call, ek_need, ek_count, ek_own_v, ek_arms) | tests/labels/run.sh (ekey_counts: padded, repeated, hashed-repeated, disclosed, constant, a constant or smaller arm; ekey_tls_schedule: an agreed key through the TLS schedule and record keys) |
| A device request's challenge slot is filled by the engine (lib/dev/device.resid, reached only through compiler-rewritten verbs): a fresh runtime value, a verifier's exact value, or an issued record's value, spent in the runtime before the request is sent (one request, even if the call fails) and bound after it to the descriptor's name and the reply's evidence. A wrong length, a reused, expired or imported record is BadInput with nothing sent. | dv_fill, dv_slot, dv_issued, dv_bound | device_challenge_slot |
| A constant AEAD nonce is refused (E0279, a warning during the rollout) unless its key rests on a draw made in the same function, outside any loop or closure, that no other sealing call there uses. Not covered yet: a nonce taken from outside data. | ek_nonce_site, ek_single_use, ek_nonce_warn | tests/labels/run.sh (ekey_nonce), challenge_export (the export token's zero nonce under its per-token key passes) |
| Relying on a provisioned key is a capability: provisioned_key(k, "reason") needs provision (mode-less, carried to every caller, checked again when a closure runs), records provision.<reason> in the graph artifact, and appears in the standard library only in its key loader (E0278). | sec_provision, gk_builtin_family, lw_declassify_check, op_scan | tests/labels/run.sh, the TLS suites (every server now grants provision) |
| Challenge records are built only by lib/challenge.resid (@opaque, E0276), their marks live in the runtime (one request, one acceptance, export only of an unused record, across threads), and only lib/challenge.resid and the device engines call the record builtins (E0277). Tokens are sealed with a per-token key (HKDF over 32 fresh bytes), opened only under the export key, spent in a SpentStore at import and refused a second import in one process. | lib/challenge.resid, runtime/rt/chal.resid, op_scan | challenge_records, challenge_export, err_opaque_literal, err_challenge_builtin, err_opaque_exporter, tests/tls (channel binding: both ends of a connection bind one exporter value) |
Not yet guaranteed (later phases of the plan): no rule refuses a program
because of a label; labels are computed only for --profile check and
debug builds; they are not yet re-checked on the residual graph or part
of the reducer's sharing key; records are labelled as a whole (a field
carries its record's label); layout types have no Secret or Challenge(N) fields yet, and a parse that exhausts the memory budget aborts; E0270 is a warning and still reports known false positives on the TLS server's event loop; the nonce rule, typed device channels and Challenge(N) fields are not in yet.
Verified evidence comes only from lib/verify/; a decision says, in its
signature, whose word it rests on. Tests: tests/attest/run.sh (a private
RESID_HOME whose lib/verify/ also holds the test anchors of
tests/attest/fixtures/testing.resid).
| Guarantee | Enforced by | Tests |
|---|---|---|
Verified(T), Appraised(T), Anchor and EvidenceTime are built only by the files of lib/verify/ (@opaque("*"), E0276, generic literals included); @primitive and @verify_internal mark functions only there (challenge_state/challenge_decide_mark also in lib/challenge.resid), and a @verify_internal function is called only from there (E0280). |
op_scan, op_sibling_ok (compiler/gcheck.resid), at_decl, at_call (compiler/attest.resid) |
verified_literal, evidence_time_literal, primitive_outside, internal_call |
An anchor is a nullary @anchor function whose annotation names its kind, principal (hardware kinds), formats (@signed types of the standard library or its own package), source, fingerprint, reviewer, algorithms and expiry; its anchor_der(bytes) is rewritten to carry those facts, the bytes are checked against the fingerprint at the first use, and anchor_make/anchor_der are refused anywhere else (E0281). |
at_expand, at_anchor_meta, at_anchor_decl, anchor_make (lib/verify/core.resid) |
anchor_bad_kind, anchor_no_principal, anchor_format_unsigned, anchor_make_outside |
A primitive's anchor argument is a call of an @anchor function (directly or through a local binding), of a kind the primitive takes, listing the algorithms it verifies with and its format (E0282); an appraisal's policy is a direct call of a nullary @policy function (E0283). |
at_check_anchor_arg, at_check_policy_arg |
anchor_arg_unknown, anchor_kind_wrong, policy_runtime |
Trust sets: a Trust is built only by an @trust function, whose body the compiler rewrites so the set holds exactly the @anchor functions it names in anchors and the sets it names in include (E0281 for the wrong shape, trust_make/trust_anchors anywhere else; E0282 for a name of the wrong kind or a set that includes itself), or by trust_with_keys/trust_with_ak, which add a verified CoRIM's or an activated AK's keys; Trust is opaque (E0276). A primitive that verifies under a trust set may rest on any anchor of the set, so a decision's accept must cover them all and require holds only for a set of one; a pure @trust set holding no anchor of a kind the primitive takes is E0282. |
at_trust_at, at_trust_decl, at_trust_ids, at_check_trust_kinds, the must facts in at_facts_call and at_requires (compiler/attest.resid); trust_make (lib/verify/claims.resid) |
trust_*, require_trust_set, ok_trust_narrow, ok_vendor_roots, key_broker (residc verify lists the set) |
Bindings: how evidence carries its challenge is a Binding made only by bind_fresh, bind_key, bind_channel and bind_device (opaque, E0276); the compiler reads which one a verification used, directly or through a local binding, for the qualifiers it gives and, for a device session, the session's anchors; a binding it cannot see gives no identity and unknown anchors, so a decision on it is refused (E0285). At run time a channel binding answers only for the record it was made with, a key binding refuses a malformed key, and a device binding needs a fresh session. |
at_binding (compiler/attest.resid), cl_want (lib/verify/claims.resid), bind_device (lib/verify/spdm_session.resid) |
binding_param_unknown, binding_literal, fresh_binding_key_bound, ok_trust_local_binding, device_bound_not_accepted, channel_broker, spdm_session_flow |
One verifier for every platform: verify_evidence reads the platform from the envelope's media or collection type alone and matches it once to its PlatformVerifier instance; the instance's roots or keys are tried in the trust set's order, a candidate that does not fit the evidence (another root's chain, a key that did not sign, the other SNP signing-key kind) leaves the next to try, and evidence that fails under a candidate that fits is refused with that failure; the challenge is then bound once, as for every platform. An instance claim that only an endorsement gives is dropped when two endorsements of the key name different instances. |
verify_evidence (lib/verify/verifier.resid), cl_verify, cl_try, cl_ambiguous (lib/verify/claims.resid), each platform's *_pv_check |
snp_negative (no ASK, no collateral, another platform's roots, an envelope of nothing this verifier reads), key_broker (a VLEK root on a VCEK report), corim_keys_flow, fuzz_verify (envelope) |
| Evidence envelopes from outside are decoded strictly and bounded: one well-formed CBOR item of definite lengths nested at most 12 deep (checked before the general decoder sees it), at most 4 MiB, a CMW record exactly [text, bytes] or [text, bytes, uint], a collection with text labels each once and at most 256 members, the envelope exactly its two members and at most 64 collateral items; every refusal is an Err. Collateral is used only when it fits the chain being checked (SNP: at most four certificate pairs are tried). | cbor_well_formed (lib/cbor.resid), cmw_decode (lib/cmw.resid), envelope_decode (lib/evidence.resid), snp_issued, snp_pairs, tdx_select |
snp_negative (a raw report), fuzz_verify (cmw, envelope for SNP, TDX, TPM and SPDM, nsm-answer) |
One appraisal for every platform: appraise_evidence refuses evidence that says the TEE can be debugged, applies the platform's mandatory rules (SEV-SNP: migration agent, VMPL 0 unless required; TDX: SEPT_VE_DISABLE; CCA: secured lifecycle; Nitro: PCRs 0-2; SPDM: measurements present), refuses any vendor TCB status other than UpToDate the policy does not allow and any allowance no platform defines, then requires the policy's measurements (at least one, or a CoRIM's corroboration) and claims, failing closed on a claim the evidence does not carry. |
cl_appraise_claims, cl_measurements, cl_require (lib/verify/claims.resid), each platform's *_pv_mandatory, *_pv_endorsed |
snp_negative, tdx_flow, cca_flow, nsm_flow, tpm_quote, spdm_flow, corim_flow |
A @decides function has a gate: every success return is reached only through the Ok of a primitive call made in its body (after ?, in a match arm or if (Ok(x) = ...)), and that gate rests only on accepted anchors, on every required one, was appraised under the named policy (appraised is required unless identity = local; appraised = none is written), is fresh (Delivered never is, unless fresh = false), carries an identity (KeyBound/ChannelBound/Local, unless identity = none), and with time = not_kernel was checked against a non-kernel time (E0284, E0285). Evidence received as a parameter has no known anchors. |
at_decides, at_stmt, at_ret, at_success, at_requires |
decides_*, ok_identity_none |
Releases: seal_to_evidence is called only inside a @decides function, and a key_bound decision's every success return is that call on its gate (E0287); at run time it refuses evidence not KeyBound to exactly the given KEM and key, seals in HPKE Auth mode under the releaser's key, and marks the gate's record decided, so a second release on one gate fails. A gate formed in a loop is refused (E0288). |
at_call, at_success; seal_to_evidence (lib/verify/seal.resid), vf_decide, rt_chal_mark op 4 |
release_outside, key_bound_plain_return, gate_in_loop, snp_negative (twice), key_broker |
What reaches or selects a decision's result is not External, at every caller and inside the body, except the bytes a primitive verifies (its inputs) and values only random draws or provisioned keys stand behind (E0286); a primitive's result is not External. |
lb_decides_args, lb_inputs_mask, lb_fn (compiler/labels.resid) |
input_external_key, input_selected, input_obtained, ok_input_random_key |
| Challenge binding: a verifier accepts evidence only when its relayed field carries the record's value (or the key- or channel-bound value made from it) followed by zeros, the record is alive and not yet accepted, and a record this program spent in a request is bound to exactly this evidence by a descriptor of its platform (an ioctl's, or the TSM report's since the configfs engine fills its challenge slot); acceptance is atomic for the process. | vf_bind_challenge, vf_reply_bound (lib/verify/core.resid), dv_ev_part (lib/dev/device.resid) |
key_broker (replay, other key, other challenge), snp_negative |
SNP: the report is 1184 bytes of a known version and signature algorithm; the ARK is the anchor and self-signed, a VLEK names a CSP_ID, the ASK and VCEK chain to it with RSASSA-PSS SHA-384, the ARK's CRL is current and does not list the ASK, the VCEK is P-384 and signs bytes 0..0x2A0; SIGNING_KEY matches the anchor's kind, the VCEK's product the anchor's, REPORTED_TCB the VCEK's SPLs, CHIP_ID the VCEK's hardware ID (a masked one is refused under a VCEK root), the CPU family the product's (version 3 on). Appraisal refuses a debug policy, a migration agent the policy does not allow, another VMPL, a committed or reported TCB below the floor, and an unlisted measurement, ID key or host data. |
snp_check, snp_claims, snp_pv_mandatory (lib/verify/snp.resid) |
snp_real (go-sev-guest's Milan report under AMD's real chain and CRL; tampered; wrong product), snp_negative |
NSM (AWS Nitro): the COSE_Sign1 is ES384 under the leaf certificate, whose chain runs from cabundle[0], which must be the anchor's certificate, through every later entry (each a CA, each signing the next) at the evidence time; the payload is a map of exactly the documented fields, each once, definite lengths, bounded sizes, no trailing bytes; the nonce must be exactly the challenge. Appraisal refuses missing PCRs 0-2, an all-zero PCR0 (debug mode), and any PCR the policy names with another value. |
nsm_check, nsm_payload, nsm_pv_mandatory (lib/verify/nsm.resid), aws_anchors.resid |
nsm_flow (a real document under the real AWS root; tampered; expired; debug enclave; a test chain's fresh, replayed, unknown-field, repeated-field and other-nonce documents; a key-bound release) |
TPM 2.0 quotes under a pinned AK (kind TpmAk): TPMS_ATTEST is TPM_GENERATED and a quote, signed over SHA-256 by the AK with an algorithm the anchor lists; one SHA-256 bank, its digest the SHA-256 of the given PCR values; extraData exactly the challenge. |
tpm_check, tq_sig (lib/verify/tpm.resid) |
tpm_quote |
TPM attestation keys by credential activation (kind TpmEk, the manufacturer's EK root): tpm_ak_challenge makes a credential (TPM2_MakeCredential: RSAES-OAEP or ECDH with KDFe, KDFa, AES-128-CFB, HMAC) for the EK certificate's key and the AK's name, its value derived from the challenge record's never-sent nonce, the AK's name computed from its public area; tpm_verify_ak accepts the TPM's answer only when it is that value (once), the EK certificate names tcg-kp-EKCertificate and chains to the anchor (each link current and signed by a CA above it) with a current CRL from its issuer for every certificate below the anchor (revoked is refused, none is stale), and the AK is a restricted signing key fixed to its TPM (fixedTPM, fixedParent, sensitiveDataOrigin, restricted, sign, not decrypt; nameAlg SHA-256; ECDSA P-256 or RSASSA-2048 with SHA-256). Quotes and counters verified from the result rest on the EK root. On the device: the chain of commands runs on one open file, links patch only within responses, a failed command ends it, and the AK has noDA while the endorsement hierarchy's authorization never counts toward lockout. |
tk_ak, tk_chain, tk_revocation, tpm_ak_check, tpm_verify_ak, trust_with_ak, tq_key (lib/verify/tpm.resid), lib/tpm_credential.resid, tpm_anchors.resid (generated), dh_tchain (runtime/rt/device.resid) |
tpm_activate (activated; replayed; another answer; the challenge's own value; another AK; revoked, missing and stale CRLs; no intermediate; no EKU; decrypting, unrestricted and movable AKs; an RSA EK's credential; quotes by the AK and by another key; a release), tpm_roots (every manufacturer root certifies a real intermediate), tpm_ak_anchor_kind, tpm_quote_activated_accept, tests/device tpm_simulator (credentials activated by the IBM simulator for RSA and ECC EKs, refused for another AK and a tampered blob), device_transact_chain, device_chain_* |
A channel_bound decision releases only through seal_to_channel, which refuses evidence not bound to exactly that connection (named by the SHA-256 of its TLS exporter), and the value is written only by tlsserver_send_bound/tlsclient_send_bound, each refusing another connection. A relying party verifying against its own connection's exporter refuses a report bound to a relayed one. |
seal_to_channel, tlsserver_send_bound, tlsclient_send_bound (lib/verify/channel.resid), vf_channel_id |
channel_broker (a release over TLS; a confused broker's other connection) |
A field of a @signed type marked @relayed or @host, or with no origin, is External when read, whatever its record's label, so a decision cannot select on it (E0286). The generic Claims keeps what the host or the requester chose apart (host_values, report_data, the CoRIM view and the raw evidence, all External) from what the platform vouches for. A second @layout_origins declaration can only make a field External, never launder one. |
lb_origins, lb_field_origins, lb_e (field) in compiler/labels.resid, origins generated by ly_origins (compiler/layout.resid) and declared for Claims (claims__origins, lib/verify/claims.resid) |
input_host_field, ok_measured_field |
Control over disclosure (E0291, E0292; warnings during the rollout, in check and debug builds and in any build of a program with a decision): a declassify whose value, or whether it runs (a condition, an earlier return, ?, break or continue), is decided by outside data is reported; each function's control summary carries the parameters that decide its disclosures to its callers, and a call that passes outside data there, or runs a disclosing function under outside control, is reported at the call. The standard library's disclosures and functions marked @robust_exempt(reason = ...) (listed by residc verify) are exempt. |
lb_disclose, lt_exit, lb_apply (compiler/labels.resid) |
robust_branch, robust_early_exit, robust_wrapper, robust_ok, robust_exempt |
| TDX (quote versions 4 and 5, ECDSA P-256 attestation key): the PCK chain (leaf, CA, root) ends at the anchor's certificate and verifies at the evidence time; the PCK key signs the QE report, whose REPORTDATA binds the attestation key and QE authentication data and whose MRSIGNER and product are Intel's TD quoting enclave; the attestation key signs the header and body; the signature data fills the quote exactly. Verification reads Intel's collateral from the envelope and refuses a PCK the PCK CA's current CRL revokes and a PCK CA the root's current CRL revokes; reads Intel's collateral (TCB info and QE identity, each strict JSON signed over its exact bytes by a TCB signing certificate under the same root, current, at or above the evaluation-number floor): the TCB info's FMSPC, PCE ID and TDX module signer must be the quote's, the first TCB level the PCK certificate's SGX SVNs, its PCESVN and the TD's TEE_TCB_SVN reach gives the status, the QE identity must match the QE report's MRSIGNER, product, MISCSELECT and attributes under their masks and its level gives the QE's status, and each status must be UpToDate or one the policy accepts; then MRTD, RTMRs and MRSEAM against the policy. | tdx_parts, tdx_check, tdx_pck_facts, tdx_select, tdx_signed_json, tdx_tcb_status, tdx_qe_status, tdx_pv_mandatory (lib/verify/tdx.resid), json_parse (lib/verify/json.resid), intel_anchors.resid |
tdx_flow (go-tdx-guest's real v4 and v5 quotes under Intel's real root; tampered; trailing bytes; a test chain's fresh, replayed, debug, SEPT_VE and other-challenge quotes; a TCB level that needs hardening, refused and then accepted by policy; Intel's real collateral against the v4 quote: no TCB level matches, as go-tdx-guest finds; collateral past nextUpdate; a revoked test PCK; a key-bound release) |
| CCA: the realm token is signed by the RAK it carries (a point on its curve), the platform token by the anchor's CPAK with an algorithm the anchor lists, and the platform token's challenge is the hash of that RAK; both claim maps hold only documented keys, once, with bounded values; the realm challenge is exactly the challenge. Appraisal refuses a platform lifecycle other than "secured" and checks the RIM, REMs and implementation IDs the policy names. | cca_collection, cca_check, cca_pv_check, cca_pv_mandatory (lib/verify/cca.resid) |
cca_flow (the TF-M test token under its CPAK; another CPAK; tampered; a test platform's fresh, replayed, unsecured, unbound and other-challenge tokens; a key-bound release) |
Rollback (§8): tpm_verify_counter accepts a TPM NV certification only when the AK signed it over SHA-256, it is TPM_GENERATED and of type NV, it covers a whole 8-byte counter, and its qualifying data is the challenge; bind_counter makes a Local blob fresh only when the counter is the one the blob was sealed against and its value is the blob's version, and the result rests on both anchors. |
tpm_verify_counter, tc_parse (lib/verify/tpm.resid), bind_counter (lib/verify/sealing.resid) |
local_flow (current, rolled back, another counter), ok_local_fresh_decision, local_counter_not_accepted |
A first seal is its own outcome: first_seal gives an empty, Local and fresh blob only when a fresh counter reading is at the program's stated initial value, never because a blob is missing. |
first_seal (lib/verify/sealing.resid) |
local_flow (initial, already advanced) |
| An EAR (draft-fv-rats-ear) is the COSE_Sign1 ES256 CWT of the appraisal's status and trustworthiness vector under the verifier's own or provisioned key. | ear_cwt, ear_claims (lib/verify/ear.resid) |
ear_flow (the claims decode to the draft's layout; the signature verifies) |
| The transcript (§9): every device crossing is noted with the runtime before the request is sent and after the reply (secret outputs by length only); the runtime keeps a running SHA-256 and the last 256 entries, atomically; it is on only in a program that reads it (main enables it first), and only lib/dev/'s engines note and only lib/transcript.resid reads (E0277). Its result is External. | dv_tr_req, dv_tr_out (lib/dev/device.resid), runtime/rt/transcript.resid, tr_hook_main (compiler/native.resid), op_chal_home |
transcript_flow, transcript_builtin |
SPDM 1.0-1.3 (NVIDIA GPUs, kind NvidiaDevice, and any vendor's device root, kind DeviceIdentity): the record's negotiation (GET_VERSION to ALGORITHMS, parsed exactly; required from 1.2, whose signature covers it; for 1.0/1.1 without one, the P-256/P-384 profile of the leaf key) must have chosen an algorithm the anchor lists; GET_MEASUREMENTS asks for a signature and carries the challenge as its nonce; every response parses exactly (blocks, count, opaque data, requester context, signature length of the negotiated algorithm); the device chain runs from the leaf to the anchor's certificate, each link current and signed by a CA above it, and every certificate below the anchor has a current good OCSP answer from its issuer or a delegated responder (NVIDIA's firmware alias leaf exempt); the leaf signs VCA ‖ unsigned exchanges ‖ request ‖ response with the 1.2 signing-context prefix where the version has it. CHALLENGE_AUTH is checked the same way over its M1 transcript. Appraisal checks the blocks a policy names. |
sp_chain, sp_ocsp, sp_algs, spdm_check, spdm_challenge_check, sp_pv_mandatory (lib/verify/spdm.resid), spdm_sig_ok (lib/spdm_msg.resid), ocsp_sr_next_update (lib/certverify.resid), nvidia_anchors.resid |
spdm_flow (NVIDIA's H100 report with NVIDIA's real OCSP answers; revoked, missing and stale OCSP; tampered; a negotiation tampered with; DMTF spdm-emu captures for 1.0-1.3 with ECDSA P-256/P-384/P-521, RSASSA-3072, RSAPSS-2048 and Ed25519; fresh 1.3 transcripts; a key-bound release), fuzz_verify |
Endorsed reference values: a CoRIM counts only as a tagged COSE_Sign1 by an Endorser anchor's key with an algorithm the anchor lists, content type application/rim+cbor, its corim-meta signature validity and corim-map rim-validity holding at the evidence time, the payload a bounded corim-map (tag 501) with CoMIDs (tag 506) whose maps repeat no key and whose keys, tags and values are each of a type the draft defines (anything else refused, not skipped). The appraisal applies reference triples only whole (environment and every measurement matching one evidence environment), a register map (TPM and Nitro PCRs, SPDM measurement blocks) only when the reference names every register the evidence holds, endorsements only to environments the claims name, conditional endorsements only when every condition holds, and a series' first matching record only; the endorsed appraisal accepts what a reference value corroborated beside the policy's values (CCA: every platform software component; SPDM: every block, in the device class its root or its endorsement names; TPM and Nitro: the PCR registers), and their result rests on the endorser's anchor too, so a decision must accept it (E0285). |
corim_check, comid, cr_mval, corim_appraise, corim_mval_matches (lib/verify/corim.resid), corim_verify, cl_appraise_endorsed (lib/verify/claims.resid), each platform's *_corim_claims and *_pv_endorsed, the with facts in at_facts_call |
corim_flow (veraison's signed CoRIM; after its validity; another endorser; tampered; a test CoRIM with every triple kind; corroboration by digest, minimum SVN, masked raw value, integer range and flags; endorsed flags and a conditional endorsement; a series; a triple applying whole or not at all; endorsed SNP, CCA and SPDM appraisals in and out of their environment; a release resting on two anchors), fuzz_verify, tests/crypto fuzz corim, endorsed_not_accepted, ok_endorsed_accepted |
SPDM sessions (1.1-1.3): verify_session accepts a KEY_EXCHANGE only with a negotiation parsed exactly that chose algorithms the library implements and the anchor lists; the certificate chain in GET_CERTIFICATE's format whose root hash is a device root of the trust set, linking up to it with OCSP as above; the DIGESTS response in the transcript of a multi-key connection; both exchange values points on the negotiated group; the requester's random the challenge; and the leaf's signature over the transcript to the signature with the 1.2 signing-context prefix where the version has it. session_covers ties measurements to the session through its all-measurements summary hash. |
spdm_session_check, verify_session, session_covers (lib/verify/spdm_session.resid) |
spdm_session_flow (1.1 and 1.3; fresh, replayed, tampered, another negotiation, another root, another challenge; measurements in and outside the session) |
The requester (lib/spdm_requester.resid, SPDM 1.0-1.3 over MCTP, PCI DOE and TCP): every response is decoded totally against the negotiation before it is used, a device's signature (CHALLENGE_AUTH, MEASUREMENTS, KEY_EXCHANGE_RSP) and ResponderVerifyData are checked before the next step, the session's secrets (ECDHE, PSK, handshake, data and updated keys) are generic over the byte type so a secret key keeps everything derived from it secret (bytes leave only through SpdmPublish(B)), ResponderVerifyData is compared in constant time, and DSP0277 messages carry the binding's sequence number and refuse a wrong one. |
lib/spdm_requester.resid, lib/spdm_session.resid, lib/spdm_msg.resid, lib/spdm_transport.resid |
tests/spdm/run.sh (22 configurations against DMTF's spdm-emu: 1.0-1.3, every implemented algorithm, mutual authentication, PSK, chunking, multi-key, secured-message versions), spdm_session_flow (an independent model's known answer), tests/crypto fuzz spdm, tests/ct |
Evidence bound to a device session: with bind_device(s), any platform's evidence verifies only when it carries challenge_session_value(challenge_value(c), th) for a session verified fresh, and the result rests on the platform's and the device's anchors, so a decision accepts both (E0285). |
bind_device (lib/verify/spdm_session.resid), cl_want (lib/verify/claims.resid), challenge_session_value (lib/challenge_bind.resid), at_binding (compiler/attest.resid) |
spdm_session_flow (bound and appraised; the plain challenge; a replayable session; a decision naming both anchors), device_bound_not_accepted |
Endorsed keys: a CoRIM's attest-key and identity triples give keys only for an environment that names an instance, and from a triple with conditions only when they name no measured element and, naming who must have authorized the key, include the endorser; keys without a public key (thumbprints, bytes) are not attestation-key candidates. under trust_with_keys, a CCA platform token verifies under a key endorsed for the token's own instance ID, a TPM quote under a key endorsed for some instance, an SPDM device whose certificate's key an identity triple names (by key, certificate or thumbprint), and the instance is claimed only when every endorsement of that key names the same one; the CoRIM's not-after and the endorser anchor's expiry bound the evidence time, and the result rests on the endorser, so a decision accepts it (E0285). |
cr_key_triple, cr_key (lib/verify/corim.resid), endorsed_keys, endorsed_identities (lib/verify/endorsed_keys.resid), trust_endorsed_cands, cl_ambiguous (lib/verify/claims.resid), cca_pv_check, tpm_cands, sp_endorsed_cands |
corim_keys_flow (the endorsed CPAK; a key for another instance; after the CoRIM's not-after; the endorsed AK and its instance; a policy requiring an instance; a reference-only CoRIM; a key-bound release on the endorser), corim_flow (identity by certificate and by thumbprint; a policy requiring the instance and another), endorsed_key_not_accepted |
@decides(bind = "b"): the decision's one ChallengeRecord must have been issued for b, checked first thing at run time; a program whose challenge_issue calls name more than one purpose names one on every decision (E0293). |
at_bind_at, at_bind_rule (compiler/attest.resid), decision_bind_check |
bind_flow, bind_required, bind_two_records |
assume(x, a) gives Verified(x) resting on the application's @assumption function a only when x is the value it pins (SHA-256), needs the assume family (E0219), and a decision accepts it only by naming the assumption; the standard library states none (E0289). |
assume (lib/verify/assume.resid), sec_assumed, at_asm_at |
assume_flow, assume_ungranted, assumption_no_pin, assume_arg_unknown |
In a program that reaches lib/verify/, no instance the program or a dependency declares replaces one of the standard library's (E0294), so the verifiers' randomness and word instances are the library's. |
at_instances (compiler/attest.resid, on the parsed graph) |
instance_replace |
| AMD CRLs below a per-product CRL number floor are refused whatever the clock says. | snp_crl_floor, snp_crl_number |
snp_negative (old CRL) |
Local: snp_platform_key derives the SNP sealing key itself, mixing in the guest policy and measurement always, only from a fresh report of a record this program spent on its own device and bound to that reply, after refusing debug and migration-agent policies, and consumes the gate; local_open gives Local only for data local_seal sealed under that key with that measurement in the authenticated data. |
snp_platform_key, local_seal, local_open (lib/verify/sealing.resid) |
local_flow, ok_local_decision, local_without_local |
A program that reaches lib/verify/ compiles only against the closure (every lib/verify/ file and what it imports) and runtime this compiler was released with, and without -rt/-rtr; --verify-lib-dev lifts it and the provenance record says so (E0290). The record's attest array lists every anchor (origin, fingerprint, reviewer), policy and decision (with identity = none, appraised = none and fresh = false marked); residc verify prints them. |
at_pins_check, at_unpinned, compiler/verify_pins.resid (generated by tools/attest/verify_pins.py, checked by boot.sh), at_report, prov_payload, vf_print_attest |
tests/attest/run.sh (pins) |
Not yet guaranteed (later phases of the plan): E0291/E0292 are warnings,
not run in release builds of programs without a decision, and closures
carry no control summary of their own (a closure's disclosures count for
the function that makes it); "trusted for control" is any primitive's
result (no [labels] control_anchors yet); CoRIM conditions that name a
measured element (such keys are not used); SPDM 1.4, ECDHE on P-521,
Ed448, SM2/SM3/SM4, FFDHE, SHA-3 and post-quantum algorithms (refused at
negotiation); a kernel interface to a TDISP device's SPDM transcript (the
requester needs a transport of the program's own); TPM EKs from the
high-range templates (P-384, RSA 3072) and the quote's qualifiedSigner;
the transcript's abort markers for failed spawn regions; the
above-kernel profile (A6).
A native module is code from another language (LLVM IR text) bound with
@link("m"). The guarantees below hold for any artifact, hostile ones
included. The test fixtures are in tests/conformance/native/.
| Guarantee | Enforcement | Tests |
|---|---|---|
Calling a native function needs the family native_<m>, checked transitively like any capability, and bounded by spawn lists, sandboxes and manifest ceilings. native_<m>(readonly) and a bare native grant nothing. |
gk_link_decl, gk_all_facts seed, gk_requires_err; force time: the stub's resid_cap_check("native_<m>!") |
err_native_ungranted, err_native_bare_native, err_native_readonly, err_native_spawn_ungranted, err_native_sandbox, tests/pkg (native ceiling), cap_guard.c |
Native code runs only in a separate process: the program re-executed from /proc/self/exe (by a child the program makes for the call, hs_spawn) with an empty environment and only the call's socket open, so none of the program's memory, arguments, environment or descriptors are there. |
rt_native_call, hs_spawn, hs_child in runtime/rt/native.resid |
native_escape (stdout), native_stateless |
| That process has no authority: before native code runs it disables the TSC, unmaps the vDSO clock pages and installs a seccomp filter allowing only a write on its socket, exit and exit_group (the request is read before; nothing after needs memory from the kernel). Any other system call, x32 or 32-bit entry kills it. | native_lockdown, native_filter |
native_escape (open, getpid, stdout, socket, fork, execve, clock, rdtsc, mmap, PROT_EXEC mmap, x32, getrandom, vsyscall), tests/runtime (native host confinement: Seccomp: 2, NoNewPrivs: 1 read from the live host) |
Shadow stack in the host: CET on x86-64 (arch_prctl ARCH_SHSTK_ENABLE then ARCH_SHSTK_LOCK), the guarded control stack on AArch64 (PR_SET_SHADOW_STACK_STATUS then PR_LOCK_SHADOW_STACK_STATUS), turned on in the host's last frame, which never returns, before the filter. Without CPU or kernel support the call fails and the host runs without it. |
native_serve |
tests/runtime (native host confinement: x86_Thread_features_locked: shstk where /proc/cpuinfo has user_shstk; the GCS half is not exercised here, no GCS hardware) |
AArch64: the module's own functions are built with return-address signing, BTI landing pads and GCS compatibility, whatever the artifact's attributes say (they are stripped from its attribute groups), in a section of their own between page-aligned marks @native.<m>.__resid_lo/__resid_hi, which bound the host's mprotect(PROT_READ|PROT_EXEC|PROT_BTI). A name beginning __resid in an artifact is refused. BTI enforcement is not exercised here (no BTI hardware): the test checks the attributes, the section and that every module symbol lies between the marks. |
nt_harden, nt_tab_ents (native.resid), native_bti (runtime) |
tests/runtime (aarch64 native hardening) |
Inline asm in a module's functions is allowed and recorded, not refused: it runs only in the host, after the filter, and refusing it would not stop native code from reaching the program's own system-call instructions. The provenance record's native_asm maps each module with inline asm to its sites by mnemonic; verify prints it. |
nt_asm_text, nt_asm_summary, prov_nasm, vf_print_nasm |
tests/provenance (native asm in the record: esc, tiny; none for spin) |
No state survives a call, and a call's CPU time is bounded (60 s), its wall-clock time too (120 s: the host is then killed and the call fails). The host acts only for the program that started it (the device host's hs_auth checks, below): one started by hand exits 124 before reading a request, and it reads the whole request, each read's sender checked, before its filter goes on; the program reads only what that host sent (hs_from_host), and in secret mode starts none without the Yama ptrace policy (below). |
process per call; RLIMIT_CPU in hs_child; hs_finish, hs_auth, native_read_req, hs_from_host |
native_stateless, tests/runtime/run.sh (native host by hand) |
The reply is untrusted input: its length must be exact, a Bool 0 or 1, a narrow integer in range, a Str(N) valid UTF-8 within its capacity. A crash or a malformed reply fails the call (an Err inside spawn). |
resid_native_int_ok, resid_native_str_ok, rt_native_call |
native_forged_reply, native_in_spawn_err, native_host_killed |
| A native call is never evaluated at compile time. | fbody = -1 in gx_collect; no leaf summary |
native_never_folded |
An artifact cannot run code in the program itself: it may reference only its own symbols (native.<m>.<name> for a name it defines, never another module's), LLVM intrinsics and memcpy/memmove/memset; module asm, aliases, ifuncs, comdats, sections, constructors, prologue and prefix data, external and thread-local globals and quoted names are refused, inside a function body as well as at top level, and a body ends only at a line that is } alone (text after the brace is refused); every symbol it defines is renamed native.<m>.*. |
nt_ingest, nt_scan, nt_refs in compiler/native.resid (E0237) |
err_native_artifact_* (brace, cross, prologue included) |
| A binding's C types are checked against the artifact's definition. | nt_abi_err (E0235, E0236) |
err_native_export_absent, err_native_abi_mismatch, err_native_artifact_internal, err_native_no_artifact |
A region's thread stack holds a native call's fixed-capacity values (a 16 MB Bytes argument and its answer live inline in the frame, §44), so a call that crashes or answers badly can run inside spawn, where its failure is the region's Err, not an abort of the program. Each spawn worker reserves 256 MB (RESID_SPAWN_STACK_MB, at least 8); the reservation is address space, committed only as the region touches it. |
spawn_stack_mb in runtime/rt/ctl.resid |
spawn_big_frame; ../resid-gui/tests/evil.sh (a malicious font module under the real wrapper, every attack an Err) |
| The standard library, the tools and the runtime bind no native module. | gk_link_place (E0232), lint |
tests/runtime (E0232) |
A package's artifact must match the SHA-256 its manifest pins, and the archive hash (and a pinned-key signature) covers .ll files. |
native_flags_of, is_source_name, pk_walk |
tests/pkg (native artifact pinned, in the archive) |
The signed provenance record names each linked artifact's SHA-256 (attestation), and the graph records each native call as an effect native_<m>.<fn>. |
prov_payload native, ga_effect |
tests/provenance (native) |
Not guaranteed:
- Correctness of native code. The process boundary contains it; it does not make it right. A reply is checked for its type, never its meaning.
- Kernel enforcement. The sandbox is only as strong as the kernel's seccomp. A kernel without seccomp, or one with a hole in an allowed system call, is outside this model, like other kernel bugs.
- Denial of service. Native code can spend its 60 s of CPU or exhaust memory (the host is first in line for the OOM killer). Both are out of scope here, as elsewhere.
- Timing and other side channels, as elsewhere.
rdrandis not blocked: OS randomness is not a capability. - The build tree.
-rtstill links an arbitrary extra C file without checks. It is a builder's flag, and an attacker who can write the build tree is out of scope.
../resid-gui binds two native modules, stb_truetype and stb_image, to
untrusted font and image files. The rows above contain what they can do;
these say what is done so that they do not crash on hostile input.
| Guarantee | Enforcement | Tests |
|---|---|---|
| Every read stb_truetype makes of a font file is bounds-checked against the file (a crafted offset reads 0), a composite glyph expands at most 8 levels and 1024 glyphs, and a failed allocation draws nothing instead of writing through a null pointer. | stbtt__rd, stbtt_GetGlyphShape and the rasterizers in ../resid-gui/vendor/stb_truetype.h (each marked resid-gui patch) |
../resid-gui/native/fuzz/run.sh font (libFuzzer, ASan, UBSan; the crashes and minute-long inputs it found replay clean) |
Signed overflow in either decoder wraps (-fwrapv), and every double the font module turns into an integer saturates (NaN is 0): hostile input makes a wrong pixel, never undefined behavior. |
../resid-gui/native/build.sh, toi in ../resid-gui/native/font/font.c |
../resid-gui/native/fuzz/run.sh font|image |
| A decoder's answer is checked field by field before a pixel is used: magic, status, sizes within limits, every glyph box inside the atlas, the image within what arrived. | font_parse, image_parse in ../resid-gui/src/gfx/ |
their inline tests (400 mutated answers each); ../resid-gui/tests/evil.sh (seven lying answers refused) |
A program reaches a kernel device only through the device provider and a
descriptor from the standard library's lib/dev/ (PLAN-device-access.md).
The compiler checks and records every descriptor; each call then runs in a
fresh, isolated device host (runtime/rt/device.resid, plan §5) that
checks the request again, opens the one path and is confined by seccomp
(and, for a configfs report, Landlock) to that one operation.
| Guarantee | Enforcement | Tests |
|---|---|---|
A device verb needs the family device, checked transitively like any capability and bounded by spawn lists, sandboxes and manifest ceilings; a descriptor whose write is true needs the full grant, at compile time and in the force-time guard (resid_device_call_w is checked as device!). A descriptor whose write the checker cannot read before reduction counts as a write. The runtime's read entry resid_device_call refuses (Denied) a request whose write byte is not 0, whatever the engine sent, and the host opens a device read-write only for a writing ioctl or a Transact. write is a reviewed label in lib/dev/, not proved from the layout, except that an ioctl that only sends (_IOC_WRITE, no Out or InOut field) labelled write = false is refused, and so is a Transact labelled write = false -- it writes its command bytes to the device (E0263, and again by the runtime, which refuses a Transact request whose write byte is not 1). |
gk_prov_family, dv_writes (gcheck), provider_family_of_line, rt_cap_check, rt_device_call, dv_check, dv_requests_err, pq_check, pq_reqs_ok, dh_ioctl |
err_device_ungranted, err_device_readonly_write, err_device_sandbox, err_device_spawn, device_sandbox_dropped, device_ok, tests/runtime/device_entry.c, tests/runtime/device_host.c (device_read_entry_refuses_write, device_transact_read_refused), tests/device (e0263_write_only_read, e0263_transact_read, device_ioctl) |
device names the provider in every scope: a local, parameter, lambda parameter, loop variable, match-arm or destructuring binding, pattern (if (Some(device) = x), Some(device) = x;), function, type, variant or import alias (import "m" as device;) of that name is refused, so device.<verb>(...) always means the provider to the checker. After reduction a verb is only a device that resolves to the builtin provider, and its descriptor must be a literal of the role type lib/dev/device.resid declares for the verb (not a record of another type with the same fields), so no other path reaches the engine. |
dv_rebinds, dv_scan (E0001), imp_resolve_lines_a (aliases), dv_is_provider_verb, dv_lit_type (E0260) |
err_device_rebind, err_device_rebind_pattern, err_device_rebind_letpat, err_device_import_alias |
The set of kernel interfaces a program can reach is the files of the standard library's lib/dev/: a descriptor literal or the @descriptor annotation anywhere else (a dependency's own lib/dev/ included: the path is compared with the standard library root, which must be absolute -- with a relative root, as when RESID_HOME is unset, no file counts as lib/dev/), a call of the engine, and a call of the runtime entries resid_device_call and resid_device_secret are refused. No program or library may define a function named resid_... (E0265): the runtime's entry points share the program's link, and the compiler makes a program a device host (calls resid_device_host first in main) only when its IR calls @resid_device_call( or @resid_device_call_w( exactly -- a look-alike such as resid_device_callz is neither definable nor matched. |
dv_scan, dv_misplaced, dv_std_dir (E0260), gk_reserved_name (E0265), dv_calls_host |
err_device_descriptor_outside, err_device_annotation, err_device_engine_direct, err_device_raw_verb, err_device_secret_raw, err_reserved_runtime_name, tests/device (e0260_relative_stdroot, device_hook_exact) |
A descriptor is known at compile time (Laws 1 and 5): one chosen or computed at run time is refused after reduction. Integer literals written 0x, 0b or 0o are known like decimal ones (the reducer reads them by value). |
gx_dev_mcall (renders it), sem_lit_dec, dv_known (E0262) |
err_device_descriptor_residual, tests/device (e0262_lib_residual, device_hex_descriptor), tests/reduce (hex_literals) |
| A device verb is an effect: never evaluated at compile time, whatever its arguments. | gx_dev_mcall returns a residual |
device_never_folded |
A descriptor's layout is consistent with its request number (_IOC_SIZE and direction bits), its fields lie inside the struct and apart, pointer fields are 8-byte aligned, buffers have a maximum (at most 16 MiB), length fields are Scalars wide enough for their buffer's maximum and no other buffer's, a Nested field's parent is an earlier In or InOut Buffer with its pointer 8-byte aligned and its length field inside the parent's maximum, apart from the pointer and wide enough (no deeper nesting, siblings apart), there is at most one Errno and none in a Sequence step, the path is under /dev/ or /sys/ without .., and the build's target has exactly one request number. A Sequence's links go forward from a Scalar output to a Scalar input of one width, and only its last step has outputs. |
dv_check, dv_nested_err (E0263, E0264); again in the runtime, pq_check, pq_nested_ok |
tests/device (one case per rule, e0263_nested_*, e0263_errno_twice, e0264_errno), tests/runtime/device_host.c (device_nested_out_parent_refused), tests/runtime/device_host.c (device_length_field_narrow_refused, device_length_field_shared_refused, device_layout_refused) |
A manifest's devices = [...] bounds the descriptors a dependency's code reaches, including through any behavior instance it could dispatch to (an instance's functions count against every bounded dependency, wherever the instance is declared); a dependency's own dependencies get at most its bound (one that declares none inherits it), and a second declaration narrows it. |
dv_bounds, dv_roots (E0261), devices_over, meet_devices, collect_sub_deps_at (resid-manifest) |
tests/pkg (pkg_device_ceiling) |
No pointer, file descriptor, request number or path reaches the program: inputs and outputs are values (List(UInt(8)), Int), and a buffer marked secret comes back as List(Secret(UInt(8))). The host allocates every buffer and patches the struct's pointer fields itself -- a Nested buffer's address into its parent buffer, which it zeroes again in the parent's output; outputs are the buffers' contents and the declared Scalars and Inlines, never a pointer. A Nested buffer gets the length the program wrote for it only up to its maximum (more is refused), and its region is exactly that long. The engine checks every input against the descriptor before the request is built, and the reply against the descriptor's maxima: a number output must fit its Scalar's width, and any 8-byte value decodes without an abort. A device module checks the device's own status words before returning data: SNP_GET_DERIVED_KEY's response status (declassified alone, four bytes) and exitinfo2 are checked, and a failed request gives Err(Kernel), never key bytes. |
lib/dev/device.resid (dv_check_ins, dv_reply, dv_rd64), dh_fill, dh_nested, dh_outs, dh_blank_ptrs, sg_key_body |
device_verb_direct, device_ok, device_reply_num, device_key_status, tests/device (device_no_address_leak), tests/runtime/device_host.c (device_nested_placed, device_nested_pointer_never_leaks, device_nested_length_refused) |
Each call runs in a fresh process: the program re-executed as resid-device-host (empty environment, one socket as fd 3, every other descriptor closed, refusing to run set-id, no core dump, no time-stamp counter on x86-64, no vDSO, CPU-limited), which checks the request again itself (the E0263/E0264 rules, the inputs against the fields, the request number for the running target), opens the one path with openat2 -- no symbolic link anywhere on a /dev/ path or a configfs root, no magic link on a sysfs attribute's (sysfs reaches attributes through ordinary links), O_NOFOLLOW on the last component either way; a kernel without openat2 gets O_NOFOLLOW alone -- and refuses a file of the wrong kind (a character device for Ioctl, Sequence and Transact; a regular sysfs or configfs file for ReadAttr), and then installs a seccomp filter that kills it on any call but the descriptor's operation on that descriptor (ioctl with that fd and each step's request number; read/write on that fd), writes to its socket, mmap of private anonymous non-executable memory only (flags exactly MAP_PRIVATE|MAP_ANONYMOUS, fd -1), and exit -- no munmap, so no guard page can be removed. Nothing the host opens outlives the call, and no descriptor is left in the program. |
hs_spawn, hs_quiet, hs_filter_install (native.resid), dh_main, dh_same_ids, pq_check, dh_open2, dh_is_chr, dh_is_attr, dh_lock, dh_base_rules, bf_rule |
tests/runtime/device_host.c (device_seccomp_kills, device_seccomp_mmap_shared, device_seccomp_munmap, configfs_root_symlink_refused, device_stateless, device_layout_refused, device_request_refused), tests/device (device_ioctl, device_sequence, device_transact, device_read_attr, device_stateless, device_absent_is_err) |
The program starts each host itself, a fresh one per call. A child made with clone(CLONE_VM|CLONE_VFORK|CLONE_UNTRACED) shares the program's memory -- and so, in secret mode, its non-dumpable state -- until execve, the calling thread waiting until then; it runs on a stack of its own and touches only a block made for it beforehand, by system calls (no allocation, no thread-local storage, no write to shared state): only the call's socket crosses execve, as fd 3, with an empty environment, no blocked signal, RLIMIT_CPU, RLIMIT_CORE 0 and PR_SET_PDEATHSIG (then getppid, against the race). The host's first act, as soon as its argv and environment have a host's shape, is PR_SET_DUMPABLE 0 (after reading AT_SECURE while /proc/self/auxv is still its own); once fd 3 is a socket it puts /dev/null on fds 0-2 (nothing it opens later lands there, and a stray write to stdout or stderr goes nowhere), closes everything else, and refuses (exit 124) when it is traced already (TracerPid in /proc/self/status). The program reaps that exact pid (it is the parent), kills it through its pidfd at the deadline, and is never made dumpable again. Yama gate: from execve until its first act a host is dumpable, so a program in secret mode starts no host unless /proc/sys/kernel/yama/ptrace_scope reads 1, 2 or 3 -- where only an ancestor may attach, and the program's ancestors already control how it is started; without Yama, or at 0, every device and native call is refused (a device call: BadReply, "not started ... Yama ptrace policy"; a native call fails with that reason). A program without secrets is not gated. |
hs_spawn, hs_child, hs_child_block, hs_yama_ok, hs_finish, hs_nodump, hs_settle, hs_untraced (native.resid); at_secure (start.resid); rt_device_host, dh_main, rt_native_host |
tests/runtime/device_host.c (device_secret_mode_yama_gate: in secret mode a policy file absent or at 0 refuses, at 1 serves; device_secret_mode_host; device_host_traced_refuses: a host traced from its execve refuses before anything; device_stateless), tests/device (device_secret_mode_host, device_secret_out) |
A host acts only for the program that started it, its parent P, with no privilege of its own. Before it reads a request it refuses (exit 124) when the kernel started it in secure mode (AT_SECURE: set-id, file capabilities, an LSM transition), when it holds an effective or permitted capability P lacks (a program running as root keeps its own; ambient capabilities are a subset of the permitted; capget of another process needs no ptrace access, so it works on a non-dumpable P), when fd 3's peer (SO_PEERCRED: the maker of the socket pair) is not P with its uid and gid, and when P does not send back 16 random bytes the host sends it; every byte it then reads must carry P's pid, uid and gid (SO_PASSCRED, checked per read), and P must still be its parent after the challenge. The challenge closes what the peer check leaves open: a process that writes a request into the socket, then execs this program or passes the socket on, passes the peer check, but only a call P is making answers the challenge, on a socket P made. A token chosen by P would not do: a freshly executed host has nothing to check it against. There is no check of P's executable: in secret mode P is not dumpable, so /proc/P/exe cannot be read, and it is not needed -- a host started by anyone else serves only that someone, who could run the program itself (the AT_SECURE and capability checks keep a privileged binary from lending its privilege), and the forgery that matters, a reply P believes, is closed on P's side: P takes bytes from a host's socket only from the exact child it made for the call (SCM_CREDENTIALS pid with P's uid and gid, every read; anything else is dropped and the call fails), and only P can make its own children. The same checks guard a native module's host. What this rests on is the kernel's word, taken as an outcome: the pids and credentials it stamps (SO_PEERCRED, SCM_CREDENTIALS -- only CAP_SYS_ADMIN may send another pid), getppid, capget, TracerPid. Nothing else outside the host is trusted. |
hs_auth, hs_caps_within, hs_peer_is, hs_challenge, hs_recv_cred, hs_answer, hs_recv_until, hs_from_host, at_secure (start.resid) |
tests/runtime/device_host.c (device_host_by_hand_other_exe, device_host_by_hand_no_answer, device_host_serves_its_parent -- by hand, a host serves its own parent that made its socket and answers --, device_host_peer_not_parent -- the socket made by another process than its parent --, device_host_answer_not_parent -- another process answers the challenge --, device_reply_from_other_process -- a reply sent by a child of the host is dropped --, device_host_at_secure, device_host_capability; each fails when its check is removed), tests/runtime/run.sh (native host by hand) |
The device host's self-tests (faults injected on purpose, a kernel that follows Nested pointers, a fake configfs) never run in a program: they live in the real host so that they run under its seccomp filter, Landlock and guard pages, but only the C harness's entries (resid_device_host_test, resid_device_test_parent) set a self-test mode, a fake root or a test deadline; no compiler declares them, and the link drops them from every program binary, whose host is always started with mode 0 and no root. They were not moved to a test-only runtime module, which could reach the host only through a hook -- a writable function pointer in every host. |
rt_device_host, rt_device_host_test, rt_device_test_parent (device.resid) |
tests/device (device_selftest_entry_absent: nm finds neither entry in a device program, and finds resid_device_host) |
The TPM is reached only through lib/dev/tpm.resid's typed wrappers (GetCapability, GetRandom, PCR_Read, ReadPublic, NV_ReadPublic, NV_Read, Quote with an existing key): its Transact descriptors tpm.tpmrm0 and tpm.tpmrm0_secret are private to that module, so no program can send a command of its own (TPM2_Clear, NV_Write, PCR_Extend), and being a Transact it needs the full device grant -- device(readonly) covers no TPM command. A manifest bound devices = ["tpm"] limits a dependency to those wrappers. |
module visibility (tpm_op, tpm_op_secret are not pub), E0263 (a Transact is a write), gk_prov_family |
err_device_tpm_raw, err_device_tpm_readonly, device_tpm_ok |
A TPM wrapper does not drive the TPM's dictionary-attack lockout where the public area shows it could: commands carry only the empty password (no password parameter exists), and before NV_Read the index's NV_ReadPublic is read and an index authorized by its own authValue (TPMA_NV_AUTHREAD) without TPMA_NV_NO_DA is refused (TpmArg, nothing sent; the owner and platform hierarchies are DA-exempt, any other authorizing handle is refused); before Quote the key's ReadPublic is read and a key without noDA is refused when userWithAuth is clear (a password cannot authorize it) or it has an authPolicy. |
tpm_nv_read_da_ok, tpm_quote_key_ok, tpm_nv_read_via, tpm_nv_read_all_via, tpm_nv_read_secret_via, tpm_quote_via, tw_pw_auth |
device_tpm_wire (each rule), tests/device tpm_simulator (a DA-protected index with a password and two keys refused with TPM_PT_LOCKOUT_COUNTER still 0; the raw command the wrappers withheld raises it to 1) |
An NV index that holds a secret is read as one: tpm_nv_read_secret receives the response through a Transact whose output is secret (tpm.tpmrm0_secret, so the bytes come back through resid_device_secret, never in the host's reply) and returns List(Secret(UInt(8))); only the response's structure (header, sizes, the password session's response) is declassified, and it is checked by the same decoder as a public read over a copy with the data zeroed. tpm_nv_read's output is public List(UInt(8)). |
tpm_nv_read_secret, tpm_send_secret, tpm2_nv_read_resp_secret |
device_tpm_wire (the secret decoder agrees with the public one on every prefix and mutant), tests/ct (dev-tpm-nv-resp-secret, dev-tpm-nv-read-secret), tpm_simulator |
Device replies parsed past the engine are untrusted input: every TPM response decoder (lib/dev/tpm_wire.resid), the SNP certificate table parser and the TSM report and PCI TSM text decoders check each length and count against the bytes they have before reading, answer Err for anything short, long, trailing or inconsistent, and never index out of range, so no reply aborts or hangs the program (a count past the bytes left is refused before any loop). TPM commands are built only from checked arguments (TpmArg otherwise, nothing sent). |
tpm_resp_params, tw_num, tw_take_2b, tw_take_sel, tw_take_2bs, tsm_snp_certs, tsm_report_decode, pci_tsm_name |
device_tpm_wire (go-tpm and tpm2-tss vectors; every prefix, as read and with its size patched, refused; every byte set to 0xff and 0x00), device_tsm_report (every prefix and corruption of a certificate table), device_pci_tsm |
A TSM report is from a provider the descriptor lists (sev_guest, tdx_guest, arm_cca_guest, checked by the host and again by the wrapper), bound to exactly 64 bytes of report data, and a report asked for with a VMPL or an SVSM comes back only from sev_guest, the one provider that honours them (a CCA guest shows the attributes and ignores them: Err(Unsupported)). |
dh_prov_known, tsm_report_get, tsm_report_decode, tsm_report_honoured |
device_tsm_report, tests/runtime/device_host.c (configfs_unknown_provider_err) |
An SVSM report's service_guid and service_manifest_version reach the kernel only well-formed (36 GUID characters; a u32) and only with a service provider -- checked by the wrapper, the engine's caller, and again by the parent and the host before any host runs -- and each write(2) to them is a store the generation check expects, as the kernel counts them (try_advance_write_generation in every *_store). |
tsm_report_get, ts_guid_text_ok, pq_report_err, pq_guid_ok, dh_cf_open, dh_cf_write, dh_cf_rules |
device_tsm_report, tests/runtime/device_host.c (configfs_report_service_guid, configfs_service_written, configfs_service_guid_missing_attr, configfs_service_options_refused) |
| The signed provenance record lists every descriptor the residual program holds (name, path, verb, request number, stability class) -- an over-approximation: one imported but never called is listed too -- and the graph records each verb as an effect naming its descriptor. | dv_records, prov_payload devices, ga_effect |
tests/provenance (device_in_provenance, device_stability_in_provenance) |
Not guaranteed:
- Time, after the kill. A host the kernel cannot kill (blocked
uninterruptibly in a driver) is left running when its call returns
Err(Timeout); it is reaped by a later call, or stays a zombie until the program exits if more than 63 pile up in one thread. - A host's first instants, under Yama. From
execveuntil itsPR_SET_DUMPABLE0 a host is dumpable, as any freshly executed program is. Withptrace_scope1 only an ancestor of the host may attach then: the program's own ancestors (its shell, a supervisor, a debugger that started it), who already control how the program is started. A tracer still attached when the host looks is refused (TracerPid); one that attached, changed the host and detached in between is not seen. Operator hardening that closes the window: install the program executable but not readable (mode 0111); the kernel then starts the program and every host non-dumpable. A program without secrets is not gated: it is dumpable itself. - The kernel's word. Every check is an outcome the kernel reports
(pids, credentials, parents, capabilities,
TracerPid, Yama's policy): a kernel bug there, a process withCAP_SYS_ADMIN(which may send any pid inSCM_CREDENTIALS) orCAP_SYS_PTRACE, and an LSM that hides/proc/self/statusor refusescapget(the host then refuses to run) are outside this model. - A program that debugs and makes host calls at once. The debugger's
wait (
resid_dbg_wait) takes any child's event, so a host that exits while it waits is reaped there and its call sees its status lost (BadReply, unless the reply is complete); a kill at a deadline goes through the host's pidfd, so it never reaches a reused pid. Killing the debuggee reaps only its known threads, by pid (reap_all). - The real configfs report interface is exercised only for absence and
on a fake configfs (
tests/runtime/device_host.c) that models the kernel's generation count; no TEE in the test setup. Landlock confines the report entry; the host still holds the right to remove another empty directory under the report root. - A host started by a program that is compromised acts for it: the host authenticates the program, not the program's integrity.
- Under emulation. qemu-user has no seccomp: a device call that reaches the filter fails closed there.
- Agreement with the kernel's headers, beyond the generated set. Only
lib/dev/uapi_*.residare generated and matrix-checked; descriptors over interfaces that are notinclude/uapistructs (Transact, ReadAttr, ConfigfsReport) and the test fixtures are written by hand; the configfs, sysfs and TPM descriptors were checked by reading one kernel tree (tests/device/kernel-pin.txt), not by a generator. The matrix runs before a release and on a schedule, not on every build, and it checks the pinned kernels only: a kernel between two pins that broke its own ABI rule would pass. The generator itself (Python, clang) is trusted to read the probe faithfully; its output is reviewed and committed. - The TPM, live. The TPM wrappers' logic (
tpm_*_via) runs against the IBM TPM simulator over TCP intests/device(tpm_simulator, only whenRESID_TPM_SIMULATORis set), with quote signatures verified; the device host's Transact on/dev/tpmrm0is tested only for reaching the device (no TPM this user may open in the test setup).tpm_quoteandtpm_nv_readuse an empty password only. - The TPM's lockout, past what a public area shows. An entity's authValue cannot be read, so a key that is not noDA, has userWithAuth and no authPolicy (go-tpm-tools' AK templates are such keys) is quoted with the empty password: if it was given a non-empty authValue, that Quote fails and counts toward the TPM's lockout. The public area is read by one command and the key or index used by the next, so an entity replaced at the same handle in between (by another process on the resource manager) is used unchecked; a quote's signature, verified against the AK the verifier trusts, still decides.
- What a device says, unsigned. PCR values, NV contents, TPM
capabilities, a TSM report's
auxblob,manifestblob,providerandgeneration, and the PCI TSM state are not evidence until a signature covers them (the device reference, "What is signed":website/src/content/docs/reference/devices.md). - Checks under
--profile checkor--no-reduce. E0261-E0264 run on the reduced program, so a type-check-only run does not make them and--no-reduceleaves every descriptor unknown (E0262).
| Guarantee | Tests |
|---|---|
| List, string and fixed-capacity indexing is bounds-checked; an index the compiler proves in range skips the check (range facts). | range_facts_discharge, conformance index cases |
| String functions never read past the terminating NUL on truncated or invalid UTF-8. | tests/runtime/utf8_bounds.c |
Materializing a range whose length overflows aborts instead of overflowing an allocation; lo..=Int.max aborts instead of wrapping to empty. |
runtime resid_range_list |
| Immediate Int/Float words are never confused with pointers: they lie at or above 2^48, and the runtime checks at startup that the stack, the heap, mmap'd memory and its own data lie below it (aborting otherwise). | tests/runtime/immediates.c, immediate_scalars |
| Arithmetic is checked (spec §6.5) unless the compiler proves it cannot overflow. | saturating_corners, range_facts_discharge |
An integer literal never wraps: it must fit the type its context gives it (binding, rt, list element, argument, return, operand, integer cast), in every base, or compilation fails (spec §6.1a). |
err_lit_range_rt_hex, err_lit_range_rt_wide, err_lit_range_rt_dec, err_lit_range_list_bin, err_lit_range_arg_oct, err_lit_range_return_hex, err_lit_range_cast, err_lit_range_operand, lit_range_edges |
Arithmetic on literals is checked like any arithmetic: a literal is lowered at the narrowest of Int, Int(128), Int(256) that holds it, so 9223372036854775807 + 1 traps at Int, and a constant folded at a wider type that does not fit the type it flows into becomes the checked conversion's abort (widen_val), never a trunc. |
lit_arith_overflow_{add,mul,sub,hex,i128} and their _noreduce copies, lit_arith_bounds, lit_arith_bounds_noreduce |
A byte string never silently loses bytes at a zero: a heap Bytes ends at its first zero byte, so a b"..." literal holding one is refused unless it is a Bytes(N); converting a Bytes(N) to Bytes, Str or Str(M) aborts when a non-zero byte follows a zero (resid_fixed_bytes); Bytes(N) → Bytes(M) copies min(N, M) bytes, zeros included. |
err_bytes_literal_zero, err_bytes_literal_nul, bytes_fixed_zeros, bytes_fixed_interior_zero_abort |
Arithmetic the runtime implements (checked_*, xs.sum()) checks overflow and aborts, like compiled arithmetic. |
checked_builtins_overflow, list_sum_overflow |
saturating_mul(-1, Int.min) saturates instead of wrapping. |
saturating_corners |
xs.grow(n, v) and every list allocation refuse a size that would overflow. |
list_grow_huge |
str_repeat aborts instead of returning "" when the size overflows or memory runs out. |
str_repeat_huge |
A code point outside the Unicode scalar values encodes as U+FFFD, so a Str stays valid UTF-8. |
(runtime code) |
A record held by a value still being built in the same expression (a constructor payload, Some(r), a struct field, an earlier call operand) is never rebuilt in place by a later operand. |
own_held_in_ctor |
A record held inside a value of a type the ownership analysis does not write in place (a sum payload, an Option, a map, a field or element of a call result) stays aliased through copies of that value, so it is never rebuilt in place under it. A sum whose payloads can reach no record, list or map (recursively; generic sums, closures and a sum name two modules declare count as reaching one) has no such object to protect and is shared freely. |
own_held_in_holder, own_scalar_sum_holder, tests/own/fuzz.sh (holder ops in gen.py) |
The runtime is Resid (runtime/rt/), built on the compiler-only raw
memory primitives, with no C library underneath. It is compiled as the
runtime module, where its own arithmetic wraps instead of trapping, so
every bound check in the runtime is written so it cannot overflow
(comparing against limit - a, never a + b > limit). The compiler
performs in-place updates of values it proves unshared (ownership
analysis, loop regions). Both are checked by review, the conformance and
runtime suites and the self-compile, not by a proof.
A package archive (RESIDPKG1) holds every .resid, .toml and .ll (native module) file of
the package, sorted, so its SHA-256 covers the sources, the manifest's
name, version, dependencies and capabilities, and resid.lock.
| Guarantee | Tests (tests/pkg/run.sh) |
|---|---|
A registry dependency is accepted only when the registry's signed index lists its exact hash, or its detached Ed25519 signature verifies under the dependency's pinned key or a [signing] keyring key. Unsigned packages need [signing] allow_unsigned = true. |
unsigned, devprofile, noanchor, viaindex, wrongindex, pinned, pinwrong, viakeyring |
[signing] require_signatures = true refuses the index on its own: a detached signature under a pinned or keyring key is then required, because a hash somebody wrote down is not a signature over it. |
reqsig_noanchor, reqsig_keyring, reqsig_wrongkey, reqsig_nopubkey |
| A modified archive is rejected. | tamperidx, tamperpin |
| The archive must hold the package that was requested (name and version), not another package signed by the same key. | subst |
A path dependency with a pinned key must match what resid-pkg sign-dir signed. |
pathapp |
| Extraction never writes outside the target directory. | extract path traversal |
A registry package names its own dependencies by version only: a path inside a verified archive would reach source outside what was verified, so it is refused (with a version too, the version is used). |
sealed path dependency |
| A dependency declared by several packages gets the meet of the ceilings they give, whichever declaration is reached first; one without a ceiling adds no bound and drops none. | unbounded declaration first |
Secret keys are written readable by their owner only (filesystem.write_secret). |
keygen secret mode |
A registry named by [registry] url is untrusted input exactly like a
local directory, and the transport widens nothing: the archive's SHA-256
is checked against resid.lock and any -sha256 sidecar, trust still
comes from a pinned key, a keyring key or a signed index, and the archive
must be the package that was asked for. A fetch that succeeds is never
itself a reason to trust anything.
| Guarantee | Tests (tests/pkg/run.sh) |
|---|---|
| A dependency fetched over HTTP is verified exactly as one fetched from disk. | remote_signed, remote_wrongkey, remote_unsigned, remote_slash |
| A version the registry does not publish is an error, not an empty build. | rem404 |
| A package archive that is not valid UTF-8 survives the round trip byte for byte. | remote archive is byte-identical after extraction |
A manifest naming both [registry] path and url is refused, rather than one silently winning. |
remboth |
An https:// registry without [registry] ca is refused; with one, the server's certificate must chain to it and name the host, or the fetch is refused. Nothing is downgraded to plaintext. |
remhttps, tlsdirect, tlsbadca |
resid-pkg serve is the publish side of the same layout, and is
deliberately small: loopback only, GET and HEAD, no listing, and no
request path may name a file outside the registry directory. Uploads are
opt-in (--upload <keyring> --index-key <key>) and take only an archive
signed by a keyring key; a client still trusts the index signature and
the archive hash, never the server. Its HTTP is
lib/httpserv.resid's, so the HTTP server guarantees below apply to it,
and four worker regions share the listener. With --cert and --key it
serves over TLS 1.3 through lib/tlswire.resid, so the TLS server
guarantees apply too.
| Guarantee | Tests (tests/pkg/run.sh) |
|---|---|
| The server serves a registry, answers 404 for what it does not carry, rejects methods other than GET/HEAD, and refuses a path that could escape the registry directory. | serve GET, serve 404, serve rejects POST, serve refused a traversal path |
| It binds loopback and nothing else. | serve is not bound to loopback only |
The signed index carries @serial (one more on every write) and @expires (30 days on; index refresh re-signs it). A consumer refuses an index without them, an expired one, and one with a lower serial than it has already seen from that registry under that key, so a mirror cannot replay an older index to re-list a withdrawn version. index verify refuses an expired index. |
publish wrote @serial/@expires, index refresh bumps the serial, rolled-back index, expired index, verify of an expired index, serial-less index |
| An extracted registry archive is not trusted as it lies in the cache: each use rewrites its files from the verified archive and refuses a file the archive does not hold. | an edited cache file restored, a planted cache file refused |
Over TLS it is the same registry: resid-fetch pulls the index and an archive byte-identical, and a key and certificate that are half given or do not belong together are refused at startup. |
resid-fetch over https, serve --cert without --key, serve with a key the certificate does not carry |
| An artifact of any size up to what the client accepts is sent whole, not refused at the runtime's 1 MiB single-send cap. | serve a 3 MB artifact byte-identical |
| A client stalled mid-request costs the registry a socket until the request deadline, not a worker. | serve answers while other clients stall |
| An upload is written only when its signature verifies under the publisher keyring; a published version is never replaced; the index is re-signed by the registry key a client pins. | upload by a keyring key, upload by a key outside the keyring, a published version replaced, index after upload, upapp |
| Uploads are opt-in, and their two flags go together. | PUT to a read-only server, serve --upload without --index-key |
| Over TLS an upload checks the server against a trust store, and refuses without one. | upload over TLS, upload over TLS without a trust store |
Not guaranteed: path dependencies without a pinned key are trusted as
local source (spec §28.3); the package signature is not a COSE structure
and does not name the publisher key; require_signatures does not extend
to path dependencies, which the spec exempts as local source; the
highest index serial seen is kept per package (target/resid/), so a fresh
checkout accepts any unexpired signed index, and a mirror can still freeze
on one until it expires (30 days); and resid build does not fetch https:// itself, so a TLS registry is pulled with
resid-fetch into a directory that [registry] path names.
The server parses requests from untrusted peers. It is plain Resid over
List(Int) byte buffers, so the memory-safety rows above cover it; the
rows here are about what it accepts.
| Guarantee | Tests (tests/http/run.sh) |
|---|---|
A request's head and body are bounded (HttpLimits: 64 KiB of head, 8 MiB of body, 1000 requests per connection by default). A longer head is answered 431 once the buffer passes the bound, at most one 16 KiB read later; a declared Content-Length over the bound is answered 413 before any of the body is read, and a chunked body as soon as its chunks would pass it. An all-digit Content-Length of more than 15 digits is 413. A chunked body is capped at 4096 chunks (413) and parsed in linear time. |
|
A request head holding NUL or another C0 control byte (other than HT, CR and LF) or DEL is refused (400). URL and form decoding accept only strict UTF-8, and %00 decodes to U+FFFD. |
roundtrip (400) |
Request smuggling shapes are refused rather than resolved one way: Transfer-Encoding with Content-Length, a coding other than a final chunked, a Content-Length that is not digits or whose repeated values differ, Transfer-Encoding on HTTP/1.0, obsolete line folding, whitespace before a header's colon, and a bare CR or LF or other control byte in a chunk-size line or a trailer. |
roundtrip (400, 501), client.py te+cl, te-gzip, bad-cl, fold, space-colon |
An HTTP/1.1 request without Host is refused (400), and an unsupported version is 505. |
roundtrip, client.py no-host, version |
| A refused request closes the connection, so nothing after the point the parser stopped is read as another request. | roundtrip, client.py |
| A connection is closed by half-closing and draining before the close, so a refused client still receives its error reply instead of a reset. | roundtrip (431 reply received), client.py huge-head |
Each request has a whole-request deadline (HttpLimits.request_ms, 30 s by default), from when the server starts waiting for it until its body is read, and the TLS handshake has the same bound; each reply likewise has reply_ms (60 s) to be taken, so a client that never reads it frees the worker when that passes; a client that trickles bytes or idles between keep-alive requests is disconnected when it passes. Enforced by the runtime (resid_tcp_deadline), so the server needs no clock grant. |
roundtrip (slow client cut off, stalled reader dropped) |
| The accept loop closes each connection exactly once, so a worker never closes a descriptor number another worker has just been handed. | roundtrip (refusals, repeated runs) |
examples/http_server.resid serves files only under its --root: a path with an empty, . or .. segment is 404, and so is a directory. |
client.py dotdot, dir |
| A client that connects and stalls -- silent, mid-head, or mid-handshake -- costs the server a descriptor, not a worker: http_accept_loop and tls_accept_loop are event loops over every connection they hold, so other clients are answered at once however many stall. | client.py (answered past 60 stalled clients), tls (served past 30 stalled handshakes) |
| Each loop holds at most HttpLimits.open_max connections (1024); past it, the one that has waited longest for its request is dropped for the newcomer, so stalled connections cannot keep new ones out. | roundtrip (crowd evicted) |
| A request is parsed once it is whole; how far it has been checked is remembered, so one sent a byte at a time costs linear work. A TLS handshake step is attempted only when a new record is complete, and a handshake past 64 KiB or 16 records is refused. | roundtrip (slow client cut off) |
Not guaranteed: a handler's own time is unbounded and runs on its loop, so a slow handler delays that loop's other connections (spawn more loops for more cores); and a flood of new connections can still crowd out waiting ones through eviction (denial of service is out of scope above).
| Guarantee | Tests (tests/tls/run.sh) |
|---|---|
| A server presents the chain it was configured with, leaf first, and refuses to start when the certificate does not carry the key it signs with -- checked at startup, not at every handshake. | key matches its certificate, a key and another key's certificate |
Only TLS 1.3 is spoken. A client that offers TLS 1.2 is refused with protocol_version rather than answered under a version the server does not implement. |
ossl hello is tls13, TLS 1.2 should be refused |
The only cipher suite is TLS_AES_128_GCM_SHA256, because that is the only one this language can protect a record with. A client offering neither it nor a share this server can use gets insufficient_security or illegal_parameter, not a downgrade. |
(offered-suite and share checks in lib/tlsserver.resid) |
| The key share is x25519, drawn fresh per handshake, so a session key is never reused across connections (forward secrecy). | (per-handshake random_bytes) |
A handshake is refused with an alert, never a silent close: protocol_version, illegal_parameter, handshake_failure, insufficient_security, decrypt_error or internal_error. |
(alert mapping in ts_alert_for) |
| A record that fails its tag ends the connection; it never becomes request bytes. | (record layer: tls_open returns nothing) |
| Records carry at most 2^14 bytes of plaintext each, so a reply larger than a record is split rather than truncated. | (large static files over TLS) |
The client's Finished is verified before the connection serves anything; a wrong one is decrypt_error. |
resid client against the resid server |
ALPN picks the first protocol this server speaks that the client also offered, so a client offering only h2 gets no ALPN extension rather than one it cannot use. |
ossl alpn pick |
| The transcript hash is taken over the bytes that went on the wire, anchored on the ClientHello as received: a field this server does not read is still in the hash. | (openssl interoperability) |
Capabilities: reading the key and the chain is filesystem(readonly) and
happens in the caller (lib/tlskey.resid); serving is network(readonly)
and binds nothing. A server that exposes a port other machines can reach
needs the full network grant, as before. Serving, and checking that the
certificate carries the key, also need declassify: the private key and
every TLS secret are typed secret (spec §48), and the handshake and record
layer publish what goes on the wire (a key share, a signature, ciphertext)
and hand up what an authenticated record decrypts to. The same holds for
the client (tls_client_connect, tls_https_get, resid-fetch,
resid build's https:// fetch).
The private key is read, never written, never printed, and not kept past the call. What this language cannot do is check the key file's mode: there is no stat verb, so a mode check is not expressible here. Keeping a key file owner-only is the operator's job, and a deployment that cannot do that should not be running this.
| Guarantee | Tests (tests/tls/run.sh) |
|---|---|
| The server is authenticated before anything is sent: the leaf has to name the host, be inside its validity window, chain to a root in the trust store, and carry a CertificateVerify that verifies under its own key. | client against our own server |
| No trust store means nothing is trusted. There is no flag to skip verification and no fallback to plaintext: an https url with no store is a refusal. | (fail-closed in tls_server_trusted; resid-fetch refuses with no store) |
A name that does not verify is refused by name -- not trusted for 'otherhost' -- rather than by a timeout or a silent close. |
untrusted name refused |
An address SAN is matched as bytes, exactly. 127.0.0.1 in a certificate is not a wildcard for the loopback. |
iPAddress SAN, wrong iPAddress SAN refused |
| A response is only accepted with a Content-Length, and over a 64 MB cap. A body is never read to close, because a registry that keeps streaming is a registry that can stream forever. | (cap and Content-Length required in tls_https_get) |
| ALPN is negotiated, not assumed. The client's offers go on the wire in its ClientHello, the server's choice comes back in EncryptedExtensions, and a client offered a protocol the server did not name fails rather than picking for itself. | server choice wins over the client's order, declined ALPN is not an invented one |
A server cannot hold a client: the whole exchange, handshake to last byte, has a deadline (five minutes; tls_client_cfg_within, tls_https_get_within, resid-fetch --timeout), and a connect gives up after 30 s. The same deadline bounds lib/http.resid and the http:// registry fetch in resid build. |
a trickling server is cut off by the fetch deadline (tests/pkg/run.sh) |
What arrives is not trusted for it: resid-fetch prints the SHA-256 and resid build still verifies the index against [registry] pubkey and every archive against its hash. The indirection adds transport authentication, not trust. |
(unchanged in tests/pkg/run.sh) |
The direction of the TLS 1.3 traffic secrets is the one mistake that a test cannot be built around: a client that uses its own application secret for both directions completes the handshake and then opens no application record at all. The client reads with the server's application traffic secret and writes with its own.
Not guaranteed:
- Only
ecdsa_secp256r1_sha256,ecdsa_secp384r1_sha384anded25519are produced. RSA signing, session resumption (PSK or tickets), client certificates, encrypted ClientHello, record compression and 0-RTT are not implemented. A client offering none of the server key's algorithm is refused rather than served with a signature the certificate does not cover. - No session ticket is ever sent, so every connection pays a full handshake. That is the safe direction to be wrong in.
- This repository's own client verifies the CertificateVerify schemes
ECDSA P-256/SHA-256, ECDSA P-384/SHA-384, Ed25519 and RSA-PSS with
SHA-256/384/512 (rsaEncryption and RSASSA-PSS keys), each only with a
certificate key of the matching kind (
tls_scheme_alg). - The key file's permissions are not checked (see above).
- Constant time is checked for the operations listed under "Cryptography library" below, on the shipped (optimized, LTO) code, including the TLS key schedule, one record sealed and opened under secret keys, and a whole handshake with a record each way between this repository's server and client in one process (no socket: each end reads the other's bytes from a buffer), with both ephemeral x25519 keys and the server's signing key marked secret. The socket I/O around those steps is not run under valgrind; it handles only published bytes. The secret types cover the rest: the checker refuses a branch, index or comparison on any TLS secret.
Release binaries carry a COSE_Sign1 (Ed25519) trailer over a record that
binds the source files, the binary and its sidecars by SHA-256. residc verify checks the signature and the hashes, then reports the record as
evidence (what it re-derived) and attestation (what only the
signer says), and names where the key it trusted came from. The graph
tools (resid-why, resid-graph, resid-debug) do not verify
provenance themselves; run residc verify before trusting their inputs.
| Guarantee | Tests (tests/provenance/run.sh) |
|---|---|
| A release build without a signing key fails; a debug build without one is unsigned and says so. | release without key, debug without key |
| The code hash covers every byte before the trailer: a modified binary, a modified signature and a modified sidecar are each refused, and a sidecar the signature covers may not be removed. | tampered code, tampered signature, tampered notes, tampered graph, missing signed sidecar |
The detached .resid-prov.cbor, when present, must be the trailer byte for byte. |
detached copy that differs from the trailer |
The record's grant is main's declared @requires, not an empty list; a program without authority records []. |
grant is main's @requires, empty grant for a main without @requires |
| When the graph artifact is signed, its sources must be the record's and every capability its nodes use must lie within the grant, with its mode: a node writing with a family the grant holds only read-only is refused. A record that lies about either, under a valid signature, is refused. | graph capability outside the signed grant, graph sources differ from the signed record |
The verdict says which keyring the key came from: anchored ($RESID_HOME/keys), supplied (--pub, RESID_VERIFY_PUB) or local (keys/*.pub in the current directory). A key found in both the install and the current directory is reported as anchored. --anchored refuses anything but the install's keyring. |
supplied key is reported, cwd keys/ is local, RESID_HOME/keys is anchored, --anchored refuses a supplied key, --anchored refuses a local key |
Evidence and attestation are printed apart. The code hash, the sidecars, the detached copy, the builder (when the verifying residc is the one recorded) and the graph cross-checks are evidence; toolchain, profile, output and grant are attestation; sources are attestation unless --sources DIR re-hashes them, and then a changed or missing file is a failure. |
code hash is evidence, builder compiler is evidence, another compiler: builder is attested, sources are attested without a tree, --sources re-derives, --sources catches a changed source |
The trailer is readable by an independent implementation (Python cbor2 + cryptography), which also verifies the signature and the code hash. |
independent reader accepts the genuine trailer |
| CBOR one-, two- and four-byte length forms read back; a head whose length runs past the buffer is refused. | two sources use the two-byte length form, cbor one-, two- and four-byte lengths read back |
A concealed payload needs RESID_PROV_KEY, and a wrong key fails authentication. |
concealed verify without key, concealed wrong key |
| Rebuilding the same source with the same key gives the same bytes. | reproducible |
Not guaranteed: toolchain and profile are attestation only, and
compiler is evidence only when the residc running verify is the
builder (otherwise it is a hash the reader may compare by hand); a
local key verifies the signature exactly as an anchored one does, and
is only named as local -- --anchored is the switch that refuses it;
the graph cross-check applies only to builds that carry a signed graph
artifact (debug and check profiles); --sources compares against the
paths the record names, so a build from another directory needs its
relative layout reproduced.
| Guarantee | Tests |
|---|---|
Every primitive agrees with Wycheproof (C2SP, committed under tests/crypto/vectors/, including every "invalid" case): ECDSA P-256/P-384 with SHA-256/384/512 and P-521 with SHA-512 (verification only) in DER and r‖s form; ECDH P-256/P-384 (raw points and SubjectPublicKeyInfo); RSA PKCS#1 v1.5 and RSA-PSS at 2048/3072/4096 bits with SHA-256/384/512; HMAC and HKDF with SHA-256/384/512; AES-128/192/256-GCM; AES key wrap; ChaCha20-Poly1305; X25519; Ed25519. |
tests/crypto/run.sh (≈13,300 vectors) |
| Deterministic ECDSA nonces are RFC 6979's, byte for byte (the RFC's own vectors and pyca/cryptography's). | ecdsa_rfc6979.txt |
HPKE (RFC 9180) matches the RFC's vectors for DHKEM(P-256) and DHKEM(X25519) in all four modes with every KDF and AEAD, and interoperates with pyca/cryptography for DHKEM(P-384). A forged tag never opens and does not advance the sequence number; hpke_at_seq moves a context only forward (back past an opened message gives a failed context, so a replay does not open again), and the last sequence number Int holds seals and opens nothing. Reusing an older context value is not prevented: contexts are values. |
hpke_rfc9180.txt, hpke_p384_pyca.txt, roundtrip |
| COSE_Sign1 (ES256, ES384, ES512, PS256/384/512, RS256/384/512, EdDSA) reads the algorithm only from the protected header, requires the key type and curve it names, and refuses a wrong tag, trailing bytes, a swapped payload and an algorithm only in the unprotected header. | cose_sign1.txt |
ECDSA verification rejects r or s outside [1, n-1], keys off the curve, sums at infinity, and DER signatures that are not strict DER (BER lengths, padded or negative integers, trailing bytes). |
Wycheproof ECDSA files |
| Ed25519 verification refuses a public key or an R of small order ([8]P the identity): under the identity key, `enc(B) | |
RSA verification refuses moduli below 2048 bits, even moduli, even or tiny exponents and exponents over 32 bits, compares PKCS#1 v1.5 by re-encoding (never by parsing the recovered block), and rejects a signature representative >= n. |
Wycheproof RSA files, rsa1024-ca |
Constant time, checked on the binary. tests/ct/run.sh runs ECDSA signing (P-256, P-384), ECDH, public-key derivation, X25519, Ed25519 signing, AES (AES-NI and software, encrypt and decrypt), AES-GCM, GHASH, AES key unwrap, ChaCha20-Poly1305, SHA-512, HMAC, HKDF, HPKE seal and open (X25519 and P-256), the TLS 1.3 key schedule and record protection, and ct_equal under valgrind memcheck with the secret marked undefined (ct_secret). No branch, conditional move or memory address depends on a secret in the optimized, LTO-linked code; a negative control (a secret-indexed table) must be reported. The software AES S-box is computed, not looked up; field reductions, point selection and conditional subtractions are masks, and masks pass through ct_hide so LLVM cannot turn them back into branches. The case list comes from the knowledge graph, and a coverage gate (tools/resid-ctcover.resid) fails the run when a library function that handles a secret -- a public signature with a Secret in it (directly or through a record or sum holding one), a public generic function that runs on secrets once instantiated at a Secret type, or any function that declassifies -- is reached by no case at a secret type, unless tests/ct/uncovered.txt lists it with a reason (today the socket loops, the TlsCfg constructor and the device I/O of lib/dev/: the engines, the reply parse that takes secrets from the runtime, and the two wrappers that call a device). The surface covers lib/dev/ as well as lib/. Of the 252 functions in it, 235 are reached by the 66 cases, among them the TLS server handshake's pure steps, constant-time base64, and loading PEM and DER key files (PKCS#8, SEC1, Ed25519) with every byte of the file marked secret, and the device modules' code on secrets fed the bytes a device would answer (tests/ct/devprobe.resid: the SNP derived key's response, the engine's outputs, a TPM NV_Read of a secret). |
tests/ct/run.sh |
A server's private key file is secret bytes from the moment it is read: tls_key_load reads it as bytes (filesystem.read_bytes, never text) and tls_key_parse makes every byte Secret(UInt(8)) before looking at any. Only framing is published, each with its declassify reason: each byte's class (line feed, other whitespace, dash, '='; computed with masks), the PEM armor lines (which start with a dash, which a base64 line cannot), the DER identifier and length octets, version and algorithm OIDs, read one at a time at public offsets, and whether a file is DER (its first byte, a SEQUENCE's 0x30). The base64 body is decoded in constant time by base64g_decode (lib/crypto.resid, generic over Word(W, B), base64_decode its public copy): each character's value and validity come from range masks, never a table or a branch, invalid characters set a bit in a secret flag, and that flag is the one bit published, through CtSame(B). The private scalar or seed is sliced out of the secret DER at public bounds and goes into ServerKey without being published; an EC scalar's range [1, n-1] is checked by the constant-time public key derivation, whose "key usable" verdict and public key are published by design. So loading a key needs @requires(declassify). Checked under valgrind with every byte of the key file marked secret (P-256, P-384 and Ed25519 PKCS#8 PEM, P-256 SEC1 PEM, PKCS#8 DER, and refused files), and the decoder against RFC 4648 §10 and malformed input at both types. |
lib/tlskey.resid (tls_key_parse, tk_classes, tk_pem_block, tk_at), lib/crypto.resid (base64g_decode, b64g_sextet) |
| Every parser of untrusted bytes is total: certificates, CRLs, OCSP responses, keys (PKCS#8, SEC1, SPKI, RSAPublicKey, COSE_Key), ECDSA signatures, CBOR/COSE, TLS handshake messages, PEM, HTTP/2 frame headers and HPACK header blocks, SPDM messages and transport frames, TPM responses, public areas and EK certificate lists, and CoRIM payloads (parsed and then appraised against themselves) never abort and never loop on malformed input; mutated inputs are run through all of them (an abort is caught per input, a hang times out). | fuzz section of tests/crypto/run.sh; tests/attest's fuzz_verify for the verifiers' own parsers (SNP, TDX, NSM, CCA, TPM, SPDM records, CoRIM, Intel's JSON) |
Randomness comes from getrandom(2) with flags 0, which blocks until the kernel's pool is ready; there is no /dev/urandom fallback. When getrandom fails, a one-byte draw (resid_crypto_random_byte) aborts and a bulk draw (resid_random_os) returns no bytes, never possibly unseeded ones. |
(runtime code, runtime/rt/net.resid) |
| Guarantee | Tests (tests/tls/run.sh) |
|---|---|
| A server is trusted only when its leaf names the connected host, is inside its validity window, and chains to a root in the trust store. | pemstore-full-chain, wrong-host, expired-leaf |
Path constraints (RFC 5280) are enforced on every link up to the root: a CA's pathLenConstraint bounds the CAs beneath it; its name constraints (dNSName and iPAddress subtrees, permitted and excluded) must admit every name in the leaf and the host it was matched for, and a constraint of any other name form refuses the chain rather than being ignored; a certificate with a critical extension the walk does not process is refused; a leaf with an extendedKeyUsage must name serverAuth (or anyExtendedKeyUsage). A dNSName * is a wildcard only as a whole leftmost label (*.). |
nc-, pathlen-, eku-*, critical-unknown-ext, partial-wildcard (fixtures/pathcons, gen_pathcons.py) |
| The store may be a PEM bundle or a directory of DER certificates; both hold the same anchor. | derstore-full-chain |
| Intermediates come from the chain the server sent, and a chain that needs one is rejected when it is not sent. | pemstore-no-chain |
| A leaf is only as trusted as the anchor that issued it. | wrong-anchor, other-root-own-leaf, derstore-rejects-other-leaf |
| No store trusts nothing. There is no "skip verification" flag: an empty or absent store refuses the handshake rather than falling back to "any certificate with the right host name". | no-store, empty-store |
| A pinned leaf is accepted without a chain, but is still checked for host name and validity. | pinned-leaf, pinned-leaf-wrong-host, pinned-expired-leaf |
| A store path that does not exist is an empty store, not a crash. | missing store path |
| PEM reading is strict: text that is not a certificate, and an unterminated block, yield no root rather than a partial one. | junk PEM, unterminated PEM block |
The chain the server sends is read whole, and a certificate_list that claims more than it holds, or that is cut short mid-entry, yields only the certificates that are actually there. |
single-certificate message, two-certificate message, three-certificate message, message with a request context, over-long certificate_list, truncated message |
Certificates are compared as moments on the timeline, not as packed
integers: x509_valid_now takes an Instant and converts the
certificate's UTCTime/GeneralizedTime through lib/calendar.resid, so a
certificate's notBefore cannot drift from what the rest of the language
calls the same day. A time this cannot read rejects rather than comparing
against a moment it did not read.
| Certificates are parsed strictly (x509_parse: DER only, inner and outer signature algorithms byte-equal, well-formed and duplicate-free extensions) and verified for ECDSA with SHA-256/384/512 on P-256 or P-384 keys, RSA PKCS#1 v1.5 with SHA-256/384/512, RSA-PSS with SHA-256/384/512 (any salt length; MGF1 must use the message hash; hashAlgorithm and maskGenAlgorithm must be present, since their defaults are SHA-1) and Ed25519. An id-RSASSA-PSS key only verifies PSS. AMD's published SEV ARK/ASK chains (Milan, Genoa) and the AWS Nitro root verify. | rsa_pkcs1, rsa_pss, pss parameter check, the x509 section of tests/crypto/run.sh |
| A certificate may only sign for another if it says CA:TRUE and allows keyCertSign. A leaf handed over as an intermediate cannot issue. | leaf must not be a CA, issuer CA checks |
| A store carrying CRLs enforces them: a certificate the issuer's current CRL lists is refused. | good.der, bad.der |
| A CRL is used only if it is signed by the issuing CA and inside its thisUpdate..nextUpdate window, so a stale CRL cannot certify anything. | a stale CRL must not be usable |
| revocation_required refuses a certificate that no current CRL covers, so "no revocation information" never reads as "not revoked". | good.der under revocation_required, revocation_required must refuse a stale CRL |
| CRLs and roots are loaded separately, so a bundle of CRLs is never mistaken for a set of trust anchors. | (loading) |
Not guaranteed:
- Revocation evidence comes from the store's CRLs and OCSP responses;
no stapled OCSP response in the handshake is read. A store with
neither for an issuer has no revocation information about that
issuer's certificates, and
revocation_requiredis the switch that makes that a refusal rather than an acceptance. - A pinned certificate (
trust_store_has) is accepted without any chain, so it is not covered by a CRL: pinning is an explicit decision to trust those exact bytes, revocability included. - A trust anchor is not itself checked for revocation.
require_signaturesdoes not extend to path dependencies, which spec §28.3 exempts as local source.- SHA-1 (in any signature), SHA-3, DSA, RSA below 2048 bits and ECDSA
over curves other than P-256, P-384 and P-521 are not verified: such a
certificate is refused, not accepted on another algorithm's terms.
P-521 is verification only (signing, ECDH and key generation refuse
it), and TLS does not offer it. ECDSA AlgorithmIdentifiers with
parameters (RFC 5758 says absent) are refused too: of the TPM
manufacturers' chains in Microsoft's TrustedTpm.cab, that rules out
Intel's OnDie CA CSME intermediate (NULL parameters) and Infineon's
2006 IFX chain (SHA-1);
tests/attest/run/tpm_roots.outrecords each root's verdict. - Constant time is checked with valgrind on x86-64 only, and covers
secret-dependent control flow and addresses, not variable-latency
instructions (the only divides in the checked binary are on public
indices in the AES key schedule and in the allocator, found by reading
its disassembly rather than by a test). The checks need valgrind installed;
without it
tests/ct/run.shruns only its coverage gate and reports the valgrind runs skipped. Coverage is reachability in the call graph: a case covers a function its code can call, not one it is proven to execute on every path (an AES-NI case also reaches the software rounds), and a generic function counts only when the probe instantiates it at aSecrettype. - A key file's framing is published by design (the key-loading row): the
positions of its line breaks, whitespace, dashes and '=' padding, its
armor lines, and its DER tags, lengths and OIDs -- which say what kind
of key it is, and how long, but nothing of the key. A PEM file is told
from DER by its first byte, so a PEM file whose explanatory text before
the armor starts with '0' is read as DER and refused. The file's bytes
as read (
filesystem.read_bytes) are an ordinary list until they are wrapped, freed like any other memory of a program in secret mode.
build/boot/seed.ll is committed LLVM IR of the compiler. ./boot.sh
links it, rebuilds the compiler from source twice and requires all three
IR outputs to be byte-identical, so the seed is exactly what the source
compiles to under itself. This does not rule out a seed that reproduces
itself while miscompiling (the "trusting trust" problem). No independent
second compiler of the current source is maintained; the independent
interpreter resid-ddc has
reproduced the seed and the runtime IR byte for byte by diverse
double-compiling, but it lives outside this repository and no suite here
reruns it.