Security

Cohesix is a pre-production research operating system. Its design reduces and makes authority visible; it does not make the complete system formally verified or suitable for unattended production use. seL4’s machine-checked proofs apply to the kernel under their stated assumptions, not automatically to Cohesix userspace, host tools, firmware, drivers, or deployment policy.

See the Glossary for Cohesix-specific authority, role, and evidence terms.

Native private adapter release requires a configured profile, signed source provenance and a current root-admitted peft.release ticket. Candidate and baseline evaluation must share every configuration binding; a registry pointer alone is not native serving proof. Expiry/revocation stops phase execution; compensation requires current authority for the exact frozen rollback target. Fresh recovery-only tickets cannot train or promote and cannot overwrite an unrelated generation. Host systemd/CUDA limits, attestation custody and refusal semantics are specified in Private LoRA release.

Reporting a vulnerability

Do not disclose a suspected vulnerability, exploit, secret, or sensitive log in a public issue or discussion.

1. Open this repository’s Security tab and use GitHub private vulnerability reporting when it is available.
2. Include the affected commit or release, target/profile, minimal reproduction, expected security boundary, and impact. Attach only redacted evidence.
3. If private reporting is unavailable, open a non-sensitive issue asking the maintainer for a private reporting channel. Do not include vulnerability details in that issue.

Cohesix is maintained as a research project and does not promise a fixed response or remediation SLA. The maintainer will acknowledge a usable private report, validate scope, coordinate disclosure when practical, and record a fix and verification evidence if the issue is accepted.

Current source receives security fixes first. Versioned release directories are immutable research snapshots; a backport exists only when the corresponding release notes explicitly identify it. Never assume that an older bundle has the security posture of the current tree.

Operator diagnostic authority

The emergency debug-input console’s hexdump requires the manifest’s explicit authority.debug_memory permission and is always disabled by either release feature. HAL admits only 1–256 bytes wholly within the root executable code span, from __text_start to __driver_task_text_start in the initial RX mapping. It excludes rodata credentials, mutable state, embedded runtime archives and device mappings. Checked range arithmetic precedes every dereference. Admission and refusal produce bounded serial audit lines; this early shell does not claim a persistent NineDoor audit journal. The ordinary production console has no arbitrary memory command.

bi, caps mcs, and smp mcs are bounded projections on an already admitted operator surface. Printed slots, badges, and generations are identifiers, not transferred authority. The live registry is copied with a non-blocking lock and released before output. Inspection performs no debug dump, capability or scheduling mutation, or seL4_SchedContext_Consumed call; generated state is never labelled live and early console never claims activation.

Security objectives and non-goals

Cohesix aims to:

• keep the privileged kernel and in-VM trusted computing base small;
• make resource and namespace authority explicit through seL4 capabilities, generated manifests, roles, tickets, and lifecycle state;
• validate hostile input before side effects;
• bound memory, work, retries, queues, and retained evidence;
• compartmentalize physical drivers and keep GPU ecosystems host-side;
• leave deterministic receipts for accepted and denied control-plane actions.

Cohesix does not currently provide:

• a formally verified whole system;
• a POSIX security boundary, multi-user desktop, or general-purpose server;
• in-VM TLS, HTTP, SSH, CUDA, NVML, model execution, or package-management services;
• encryption for the direct TCP console or hive-gateway;
• a Pi 4 IOMMU/SMMU boundary on BCM2711;
• a guarantee that a compromised operator host, boot firmware, selected driver firmware, or privileged build environment cannot compromise a deployment.

Trust and authority boundaries

The seL4 kernel controls memory objects, execution, notifications, interrupts, and IPC through capabilities. Cohesix root-task remains trusted for bootstrap, HAL admission, manifest enforcement, namespace authority, tickets, lifecycle, and audit. Queen and Worker-role sessions receive only their generated namespace view; Worker tickets are mandatory and Queen ticket requirements are profile-controlled. The operational QEMU and Pi profiles declare Heartbeat, GPU and LoRA as executable roles with compiler-owned endpoint and lifecycle authority. WorkerBus remains model/session-only. Declaration and reserved badges do not prove live capability installation or execution; READY and exact-target evidence are separate.

Physical devices run in manifest-declared, single-threaded Rust driver runtimes. HAL owns physical-address discovery, device-untyped admission, MMIO, IRQ, DMA, PCI, SDIO, and board-level resource assignment. Driver runtimes may touch only the resources delivered through their generated fixed ABI. The root task may admit resources, submit bounded service turns, and retain diagnostics, but must not own steady-state physical drivers.

Host tools are outside the target TCB. They may use operating-system services, CUDA/NVML, model runtimes, REST, and UI frameworks, but may only project the documented console and Secure9P semantics. A compromised host tool with a valid Queen secret can exercise that secret’s authority; least-privilege host process and secret handling remain deployment responsibilities.

See Architecture for component boundaries, Roles and scheduling for role authority, and Drivers for the physical-device proof contract.

Network and console exposure

The authenticated root-task TCP console is the only in-VM TCP listener. It uses length-framed console lines with transport AUTH, application ATTACH, bounded commands, OK/ERR responses, and END stream terminators. It is not a Secure9P listener.

Authentication is not encryption. Bind direct console forwarding to loopback or carry it through an authenticated encrypted tunnel. Hive Gateway also defaults to loopback, refuses a non-loopback bind without explicit opt-in, and does not terminate TLS. Use different secrets for target-console and gateway request authentication.

Only one process may own the target TCP session. Concurrent clients share one Hive Gateway owner rather than racing direct cohsh, SwarmUI, or bridge connections.

Host agent protocol access has a compiler-owned, false-default master switch and independent MCP and A2A switches in manifest schema 1.29. The effective value is the master AND the per-protocol switch. The selected QEMU profile enables MCP and A2A on the authenticated Hive Gateway bind; Pi keeps both disabled. The gateway rejects runtime override attempts before resolving credentials or starting transport work. Switching access off does not erase an execution or pending delivery obligation.

MCP Streamable HTTP uses the existing request credential and delegated ticket; local stdio resolves a delegated ticket from an explicit secret reference and writes only protocol messages to stdout. HTTP checks Origin where supplied, rejects unauthenticated requests before dispatch, and validates the pinned revision, content types and bounds. Per-subject discovery is derived from the current standing ledger, and every tool still enters the same REST/CLI job authority path. Preflight observes current provider and target facts but does not reserve or dispatch. A tool reply, model text, timeout or disconnect does not prove a native result or cancel a job. A2A uses the same request credential, delegated ticket, standing budget and exact job identity. Its Agent Card is subject-scoped; its bounded JSON-RPC and SSE handlers carry no second scheduler, push callback or provider credential. Task completion and digest references cannot substitute for native output or shared PEFT verification. A disabled A2A switch registers neither card nor task route or stream.

Console compartment boundary

The active console-network-runtime child uses console-network ABI v6 and owns smoltcp, Ethernet/IP/TCP state, length framing, constant-time transport-token comparison, and pre-authentication timeouts. Root owns no TCP parser. It receives only a copied, authenticated bounded command and remains the sole authority for Queen policy, role tickets, namespace operations, and command execution.

Four fixed shared pages carry the ordinary pointer-free sequence-last packet, control, egress, and event records between root and the child. Page mappings are directional, reserved fields must be zero, lengths are validated before copying, and an incomplete or unstable commit is rejected. The child cannot access root CSpace, namespace-wide authority, SchedControl, or undeclared memory. Its only device-side authority is the exact generated backend: QEMU direct-VirtIO resources or, on the Pi bcmgenet-v5 profile, a CPU-only direct-GENET extension that grants no MMIO, DMA, device-visible, or physical-address authority.

The Pi extension becomes eligible only after DHCP and exact quiescence of every root-mediated GENET command, RX, and TX cursor. Root publishes the pending generation before one generation-bound zero-payload DGHO; only its exact PROGRESS/READY terminal activates the link. Exact IDLE/QUIESCING retains the old path for bounded drain and retry. The 32 reused pages map as cacheable Normal/XN memory in the GENET and console children: page 0 carries aligned sequence-last control, pages 1 through 15 carry GENET-to-console RX, and pages 16 through 31 carry console-to-GENET TX. GENET remains the sole MMIO/DMA/IRQ and private-DMA-ring owner. Console-network remains the sole smoltcp/TCP/auth owner. Root retains lifecycle, control-event, and fault supervision but no steady packet-copy, poll, or GENET packet-command authority after READY.

Each direct direction has one producer and one consumer. Generation-bound monotonic cursors and sequence-last commits carry truth; reciprocal send-only notifications are coalescing wake hints, and each consumer rechecks durable state before waiting. A handoff failure, peer fault, invalid cursor or sequence, stale generation, descriptor drift, or containment error poisons the link and pair-contains both generations. Coupled containment suspends GENET, removes both signal caps and all 32 external console mapping caps before anchor revoke, and cannot return to root packet mediation as a fallback.

The selected Pi direct-GENET console image spans 69 PT_LOAD pages and is admitted by a generated service inventory of 107 frames and 164 retained root CSpace slots. The speed-profile increase from 66 pages is three executable image frames and their retained mapping caps; data-plane and scheduling budgets are unchanged. The 32 direct pages reuse external GENET-owned frames and add mapping caps, not new data-plane frame objects or a larger child untyped. Exact construction bounds constrain authority; they are not runtime or performance evidence.

Publication requires explicit credit after root has copied, validated, and durably handled the indicated records. Notifications are wakeups, not data. Duplicate, stale, uncredited, or generation-mismatched records fail closed. Graceful shutdown publishes one terminal record before containment; fault and revoke paths scrub mappings, signals, pending responses, and capabilities before the child generation can be reused.

Root control, the console child, and the Pi resumable GENET runtime use the selected generated timeout policy. Under NaturalPostpone, exhaustion of the current scheduling-context refill postpones execution until replenishment; standard faults remain installed and terminal. GENET protocol, cursor, DMA, IRQ, device-deadline, and paired containment failures remain fail closed; only ordinary legal budget exhaustion postpones. Reserved timeout identities remain accounted, but client timeouts, retry policy, public grammar, and fault authority are unchanged. Exact temporal values and response analysis belong to the selected generated profile and Roles and Scheduling.

Authentication and attachment

The host authority floor combines MAC-verified REST delegation, bounded caller quota retention, strict Queen idempotency, and durable host executor recovery. It is gateway_enforced, not evidence of VM-verified REST caller identity. Release A requires provisioned env:/file: ticket secrets, a public CAS verification key distinct from the published fixture, enabled bounded audit/replay, and disabled arbitrary-memory diagnostics. The release assembler rejects development authority profiles and scans selected payloads for renamed private fixture keys and secret canaries. M27a authority records production gates and the separate, still-deferred 28d ledger/quarantine claims.

Ticket references are resolved into the target binary at build time. A privately provisioned image therefore belongs inside the credential boundary even though its resolved JSON contains references only. Public evaluation images must use separate explicitly shared credentials; private hive keys cannot be reused for their builds. Host-side credential changes do not rotate a compiled target key.

External identity and read visibility

External identity mapping is host-only. coh identity --mapping ID accepts a JWT through stdin and public keys through --jwks FILE; a local mapping uses --local and the kernel effective uid. The generated providers.identity_mappings policy pins issuer, one audience, signing algorithm, exact public-JWKS digests, external subject, required groups, normalized audit subject, role, paths, provider actions, operation count and TTL. OIDC and Kubernetes issuers require HTTPS identities; JWT-SVIDs bind the SPIFFE trust domain and exact workload path. RS256, ES256 and Ed25519 keys cannot be interchanged, and token-supplied discovery URLs are not followed. Unknown subjects, missing groups, wrong audience, invalid signatures, expired or overlong tokens and broad root scopes are refused. Deployments enroll explicit mappings in compiler input; shipped mappings are disabled.

By default, the CLI prints a cohesix-identity-request/v1 proposal. Explicit issuer enrollment enables gateway-only ticket issuance through the CLI or POST /v1/identity/exchange. The gateway checks each write’s generated provider action before charging quotas or forwarding it; mapped tickets have a separate signing domain and cannot authenticate directly to the VM. JWT issuer time and expiry survive repeated exchanges. Local uid assertions are accepted only from the local kernel-backed CLI, never from HTTP. See the complete identity enrollment and ticket wire contract, including finite bounds, audit redaction, disabled defaults and restart limitations.

The gateway classifies all REST namespace reads using compiler-owned component-prefix rules. Unclassified paths inherit admin_only; the admin-only registry and public version/capability summaries contain no live provider state. File reads and status check request authentication and delegated Read/ReadWrite scopes before cache lookup or broker dispatch, sharing signature, expiry, mount, role, ceiling and quota checks with writes. Scoped Worker reads bind the subject; an explicit Queen root read scope grants administrative access. Write-only scopes confer no read authority. --read-compatibility is an explicit single-caller gateway-Queen posture for admin-class paths only; it cannot expose ticket-scoped paths without delegation. Read denials enter the existing bounded delegation audit path. Python objects and native labels remain non-authoritative projections.

Transport AUTH proves access to the console listener. Application ATTACH separately selects a role and validates any required ticket. A Worker-role attachment does not create a Worker task; executable Worker lifecycle is admitted independently by the generated supervisor.

Attachment is one authority transaction. The namespace child validates and prepares the role/ticket context, NineDoor commits that context, and root emits OK ATTACH only after the bridge transaction succeeds. Optional logging, tracing, or endpoint diagnostics are best-effort observations and cannot grant, veto, or roll back authority.

A leaky-bucket rate limiter allows two failed authentication attempts in a 60-second window; the next failure enters a 90-second cooldown. Root adds bounded exponential backoff beginning at 250 ms. Denials and successful role assertions emit bounded audit lines without printing secrets.

Response and availability rules

Responses preserve the public OK/ERR/END order. Large bodies are split into bounded records and service units. An authenticated response lane receives bounded flush priority without starving physical operator input, fatal output, timers, containment, or ordinary service.

Pi network cadence may retain only exact durable productive identity inside the generated scheduling policy and unchanged hard caps. Exact direct-GENET productive identity may resume under generated NaturalPostpone for at most 64 complete quanta and only for the current authenticated request. A stage-bearing continuation additionally binds the exact nonzero one-slot child-control sequence and may use the condition-before-block root fan-in only while that same control still owes its child watermark. Fused stage-and-drain or OutputDrained is terminal: direct GENET takes the ordinary Yield and cannot carry a baton, empty hot tail, broad wait, or authority into a future sequential request. Mediated WiFi may resume only under generated NaturalPostpone, with every full Operator, Driver, and attached Network service turn charged against the unchanged 64 logical material-work cap and productive Driver or attached Network progress independently capped at 64. Root-control remains on core 0 and console-network on core 2. Neither Pi backend pre-drains the child SC or calls SchedContext_YieldTo. WiFi additionally binds the selected physical lifetime, authenticated generation/connection, and accepted-command epoch. Identity or control-sequence drift, operator or passive work, recovery, containment, quarantine, reboot, handoff, local fault, incompatible generated policy, or cap expiry fails closed without a new refill, retry, packet owner, or device authority.

The exact-743e CYW43 correction does not grant wake-badge authority. Only after one nonzero sequence-last child command is durable and the retained root-causal frontier still reads Waiting on the exact Cyw43Client route may CYW43 use one MCS seL4_NBSendWait to prompt the existing send-only slot-8 SDIO doorbell while atomically blocking on its bound read-only slot-3 local notification. Returned, Recovery, Invalid, wrong-route, zero-sequence, or identity-drift evidence performs no combined wait and selects the existing fail-closed path. This atomic peer prompt is MCS-only. A classic non-MCS profile retains its prior local-notification wait-only behavior and sends no additional SDIO peer signal. A coalesced MCS wake can re-prompt only the same durable command; it cannot authorize a retry, duplicate device action, fallback owner, broadened capability, or new queue entry.

The exact fresh-foreground-publication correction adds no badge authority. CYW43 captures the exact admitted parent, child, generation, root-grant environment, stable Waiting completion, Cyw43Client route, and recovery fences before committing the sequence-last child command. This includes the ordinary cold HOST_CONFIG child as well as persistent exchanges. After that commit and its required cache clean, selected MCS performs no passive read, diagnostic publication, or semantic bookkeeping before atomically prompting slot 8 and parking on slot 3. A later recovery race can cause at most one redundant coalesced hint: SDIO still validates the durable command and generation before its sole physical issue. On return, CYW43 revalidates the immutable frontier, completion, and recovery state before later work. It does not replay the legacy producer WAIT_BEGIN phase over a newer owner action, terminal, or recovery frontier. Classic and every inexact, stale, wrong-route, or recovery-fenced publication retain one signal-only prompt. The returned badge carries no work authority. A reserved-root bit may pass only through the existing exact expired-deadline classifier, which independently requires the immutable arm, physical lifetime, child sequence, and expiry before prompting SDIO. This cannot broaden either cap, duplicate an operation, or create a retry, queue, fallback owner, or recovery path.

Selected-MCS terminal handoff also preserves durable authority across the producer wake. The isolated runtime commits completion, retires the consumed sequence, and publishes receive-ready before an atomic reply-and-receive or the reciprocal delegated-SDIO-child peer-prompt-and-wait syscall. Root-owned low-domain SDIO bootstrap and recovery commands retain ordinary root fan-in and remain endpoint-capable while CYW43 is suspended. A returned badge is scheduling information only; a returned endpoint MR0 must still match the stable sequence-last command. The delegated SDIO atomic peer prompt is the first scheduling syscall after retirement, and generic root fan-in cannot precede it. Failed completion publication never admits a successor. Thus the optimization closes a lost-wake interval without transferring the Reply object, scheduling context, physical issue authority, recovery authority, or capability rights.

An exact-command-badged endpoint IPC with an invalid MR0 or sequence enters the generated standard-fault lane; arbitrary or unbadged notification values cannot manufacture Reply ownership from a visible ring record. Completion publication failure likewise traps before local retirement, receive-ready, Reply, signal, or receive, leaving the independent supervisor as the sole authority to answer an associated caller and fence the generation.

The direct-GENET correction narrows continuation authority to the current causal episode. Generation and connection are insufficient without the exact nonzero child-control sequence for a stage-bearing wait. Once fused stage-and-drain or OutputDrained completes that response, the current activation ends at explicit Yield. A post-response Network baton, cross-core empty hot tail, or broad fan-in wait is never minted for a request the peer has not yet published. The next request enters the ordinary Serial-first rotor, so the correction cannot bypass operator priority, display debt, passive work, fault handling, or any recovery and containment fence.

Routine diagnostics are best-effort and may be dropped under their declared bound. Security-relevant authority, lifecycle, completion, and fault decisions remain in typed records or evidence surfaces rather than relying on an unstructured log line. A full diagnostic queue cannot create an alternate output owner, retry loop, or unbounded backlog.

Input, protocol, and memory controls

All user-controlled console lines, paths, 9P frames, JSON records, tickets, and configuration values must be validated before side effects. The public Secure9P red lines are 9P2000.L only, msize <= 8192, walk depth at most 8, no .., and no fid reuse after clunk. Short writes, tag concurrency, cursor advances, scope rates, and retained bytes are generated and bounded. See Secure9P for session invariants and Interfaces for record schemas.

Network RX/TX, serial, pending console lines, driver rings, logs, telemetry, evidence, and retry work use fixed or manifest-bounded storage. Overload must surface a deterministic refusal or counter; it must not create an unbounded queue or silent retry loop. The event pump serializes authoritative target state. SMP is used for separate single-threaded tasks, not shared-memory multithreading of authority state. The Pi direct-GENET pages carry only bounded SPSC data-plane state between two fixed owners; they do not make root authority shared or make notifications authoritative.

The namespace-service contract treats path, payload, partial frame, sequence, and generation fields as hostile. The as-built nine-door-runtime source validates them in a restricted no_std child and returns only a typed bounded prepared operation; the root-side contract independently checks the exact response identity and bytes before policy or mutation. Root’s endpoint cap is Write + GrantReply with neither Read nor Grant, while the child’s endpoint cap is Read-only. Request and response mappings are directionally restricted, exactly two pages each, and backed by disjoint live frame handles validated against generated virtual addresses. The QEMU constructor validates the embedded image digest, entry, and W^X load span, allocates only the compiler-budgeted anchor generation, and registers the still-suspended TCB before registry seal. During construction, root configures and binds one compiler-budgeted, root-retained bootstrap scheduling context; the child receives neither that scheduling-context cap nor SchedControl authority. After registry seal and root-fault activation, root resumes the child, validates an empty Log parser probe, observes the child’s atomic ReplyRecv transition into the next receive, and unbinds the exact bootstrap scheduling context before declaring the service passive. Activation, probe, or unbind failure revokes the namespace boundary and suspends the child where possible, so no later Call can block on a failed bootstrap. The receive-loop Reply object is shared only with the generated root-fault recovery slot. On fault, an outstanding donor receives exactly one typed Closed failure before the durable containment record is published; without an outstanding Call no Reply is attempted. Recovery authority is then retained and serialized until all four request/response mapping lifecycles are scrubbed and unmapped. The recovery Reply cap is then quietly deleted before the two fault caps and retained anchor are revoked. Root-control advances that fixed NineDoor containment cursor one material unit per exclusive Recovery turn and only after all higher-priority console-network recovery work is absent. Steady operation is passive donation only after the bootstrap scheduling context has been unbound; no SetAffinity placement path is used. The active console service cannot enter this passive path. Closing with a partial frame, queue saturation, cancellation, child-generation revocation, replay, and late completion fail closed. The child receives only its service endpoint/Reply object and two bounded shared-frame mappings; it receives no Queen policy, root CSpace, device, broad namespace, scheduling context cap, or SchedControl authority. The bootstrap scheduling-context implementation remains subject to live QEMU qualification. This internal ABI does not relax the rule that the authenticated console is the only in-VM TCP listener. Live QEMU fault injection remains evidence required beyond source and target checks; it is not Pi hardware acceptance.

Operational host/GPU projection begins unavailable source=none; target source contains no fabricated provider or GPU topology. GPU snapshots use gpu-bridge-snapshot/v2 and arrive only through an authenticated Queen session. Root validates the production source identity, epoch and strictly increasing sequence, observation time, bounded TTL, catalog and per-manifest digests, CAS/base/adapter compatibility, and activation generation/receipt before atomically replacing a generation. Fixture-mode, stale, replayed, forged, incompatible, or oversized snapshots fail closed. Accepted data is withdrawn at TTL and direct writes to the active-model pointer are denied. Console/REST placeholder credentials fail before connection, and fixture signing keys are forbidden from operational target and release closures. Operational manifests select cas.signing.verification_key_path; coh-rtc validates a public Ed25519 point and emits only those public bytes. The corresponding signing key remains in an external secret store. The checked-in fixture signing seed and its public counterpart are test-only and cannot be selected by the QEMU/Pi runtime or release manifest. For a generated production profile, place the deployment public key below the profile output directory. coh-rtc-authority-profile writes its path relative to that directory, so the same manifest and public key can be copied to Mac and Linux builders without embedding the build host’s absolute path.

Ticket quota limits (generated)

• ticket_limits.max_scopes: 8
• ticket_limits.max_scope_path_len: 128
• ticket_limits.max_scope_rate_per_s: 64 (0 = unlimited)
• ticket_limits.bandwidth_bytes: 8388608 (0 = unlimited)
• ticket_limits.cursor_resumes: 16 (0 = unlimited)
• ticket_limits.cursor_advances: 256 (0 = unlimited)

Generated by coh-rtc (sha256: 3b1501e34fd9367b624534459a6f036cd1990d2e663f21189fa7c85781584da9).

These values are the committed default-profile snapshot. The selected source manifest and resolved manifest govern a target build.

The default cumulative session byte allowance is 8 MiB (8388608 bytes). It covers several complete retained Queen-log exports (up to 2112 records of 256 bytes plus separators) and ordinary CLI, FUSE, SDK and UI traffic sharing a gateway. It is an accounting ceiling, not a preallocated response buffer or a per-second rate. Explicit smaller ticket quotas remain effective. Payload, stream, cursor, rate, namespace and role bounds are unchanged; exhausted sessions still fail with ELIMIT. New sessions bind the selected build’s limits; existing signed tickets retain any smaller explicit allowance.

Hardware, DMA, and firmware

QEMU is the reference development and regression target; it is not physical hardware proof. On Raspberry Pi 4, selected physical devices are admitted to isolated driver runtimes after HAL coverage checks. BCM2711 has no supported IOMMU/SMMU isolation path in the current Cohesix profile, so DMA safety relies on HAL-owned ranges, bounded rings, cache policy, quarantine rules, and single-owner driver admission. Documentation must not describe that as hardware DMA isolation.

The direct-GENET CPU link does not weaken that owner boundary or enlarge the DMA claim. GENET alone retains its private DMA buffers and device descriptors and copies validated frames to or from CPU-only shared pages. Console-network sees neither DMA mappings nor physical addresses. Coupled fail-closed containment is mandatory because the peers share data-plane state: a fault in either generation removes reciprocal signalling and console page copies before revoke, without reviving root packet mediation.

The GENETv5 implementation uses Linux device-tree and driver behavior plus U-Boot bring-up as reference material. The CYW43455/SDIO implementation uses OpenBSD bwfm, Zephyr/Infineon WHD layering, and Linux brcmfmac edge cases as reference material. These are provenance references, not code sources; source lift is prohibited. CYW43455 and SDIO runtimes are implemented research surfaces, but current-image association, DHCP, TCP, and repeatability remain evidence-gated in the build plan. Likewise, a generated direct-GENET descriptor, successful target build, or staged image proves neither handoff nor traffic. Fresh same-image Pi evidence must separately qualify GENET correctness, containment, latency, throughput, and benchmark behavior.

Pi firmware, U-Boot, Wi-Fi firmware/NVRAM, and the external seL4 build are deployment dependencies. Pin their provenance, verify staged hashes, and keep flash proof separate from proof that the board booted the same image. The hardware runbook owns the accepted evidence sequence.

Secrets and sensitive data

• Do not commit deployment credentials or copy them into examples, issue text, evidence, command history, or screenshots.
• Root-task and the primary coh, cohsh, Python, and live-gateway paths reject the literal placeholder changeme. Some ancillary compatibility binaries still expose legacy placeholder defaults; that value cannot authenticate a current target and must be overridden. Select real, distinct target-console and gateway request secrets.
• Pass secrets through protected deployment configuration or environment variables, prefer hidden shell input, and unset them after use.
• Host-ticket arguments must contain opaque secret references, not bearer tokens or raw credentials.
• Treat manifest ticket secrets, Wi-Fi PSKs, CAS signing material, evidence packs, and raw serial logs as sensitive even when the repository contains development fixtures.

Boot-time cohesix.env may persist only documented network policy fields. It is not a general secret store, and writing saved policy is a separate proof state from successfully using that policy on the current image.

Audit, evidence, and replay

The host-only causal verifier requires canonical typed bytes, bounded Ed25519-signed records, separately configured phase custodians, exact component and target hashes, ticket/subject/action/idempotency/writer binding, chronological parent references, one terminal result, native identity/generation continuity, and immutable CAS contents. A provider key with no grant phase permission cannot sign a grant. Pack checksums establish content integrity only. Imported operation reports, OTel spans, CloudEvents and in-toto statements never become authoritative Cohesix receipts. The verifier’s explicitly selected recorded time supports offline reconstruction without claiming current freshness. Live producer integration and admission remain distinct from verifier conformance.

Recovery uses a new ticket and idempotency key with its own signed intent/facts/approval/grant/execution/verification/terminal chain. The signed binding links the original ticket, graph hash and terminal hash. coh evidence verify-recovery verifies both independent graphs and their chronology, target and epoch relationships. Appending a provider-signed compensation assertion to an earlier ticket cannot authorize reversal.

Federation distinguishes target-write acknowledgement from terminal delivery. Pending and acknowledged intents, and retained results awaiting source delivery, are non-evictable. The relay persists the exact target terminal bytes before publishing them to the source, and checks action, writer epoch, idempotency and source/target/hop/correlation identity. Conflicting terminals remain unresolved. Restart observes acknowledged work without executing it again; old WAL delivered entries are migrated to awaiting terminal observation because their historical ACK did not prove completion. Peer request-auth and delegated ticket references come from the generated provider contract and are resolved host-side.

SIEM delivery custody

SIEM delivery consumes a graph accepted by the shared verifier and exports only the generated allowlist. providers.siem_delivery selects one HTTPS endpoint and a credential reference; event data cannot select a destination. Redirects and environment proxies are disabled. A private, locked state directory durably retains the projection, monotonic cursor, attempt state, retry time, and exact destination acknowledgement. The receiver must dedupe Idempotency-Key durably and return cohesix-siem-ack/v1 with the same graph digest, payload digest and status=accepted. Lost acknowledgements can cause the same key to be sent again; receiver deduplication is part of the deployment contract. No local copy or HTTP status alone counts as delivery. Pending and deadletter entries are retained at capacity, applying backpressure. Re-running the command with the same verified graph resumes the bounded retry state; changing destination policy requires a separately owned state directory. An explicit ca_certificate_path_ref resolves locally to one bounded PEM CA path and replaces default TLS roots. Invalid selection never falls back to ambient trust. State files reject symlinks, hard links, foreign ownership and group/world write permissions inside the private owner-only directory. An existing owner lock with a missing WAL is a recovery error, not an empty queue. The exact receiver ACK bytes are retained and hashed before the sender advances its durable acknowledgement state. Historic evidence delivery carries no new provider-execution or admission authority.

Security-relevant accepts and denials write bounded audit lines to /log/queen.log and, when enabled by the selected profile, /audit records. Host ticket actions use versioned, allowlisted schemas, idempotency keys, and explicit lifecycle receipts so operators can distinguish requested, claimed, running, terminal, and dead-letter states.

coh evidence pack records captured and missing paths instead of inventing data. It hashes audit ticket fields and recursively redacts JSON keys containing token, secret, password, signing-key, or API-key material. Redaction reduces accidental disclosure; it is not a substitute for reviewing a pack before sharing it. The exact pack contract and CI/SIEM recipes live in Operator recipes.

Replay is limited to retained Cohesix control-plane records. It cannot recreate external host state, reverse a host side effect, or prove that an omitted event did not occur. Policy approvals are single-use; replaying a consumed approval fails deterministically and emits an audit record.

Operator evidence trust boundary

The operator evidence contract is host-side and read-only. Canonical trace digests bind retained bytes and redaction policy; they are integrity checks, not authenticated device signatures. Expected identity labels supplied by a caller remain non-attested. Replay permits only retained reads and rejects writes without opening a network connection. Pack and case readers enforce bounded regular files, confined paths, explicit inventory availability, and shared recursive secret-field redaction.

The shared TPM2 verifier checks enrolled certificate chains, signatures, nonce/boot/artifact/PCR binding, time bounds and replay/reset data. Its policy comes from the verifier, never from target evidence. Offline PASS remains an explicit historical-signature result. The current Pi uses optional measurement-only mode; required or signed modes without an admitted provider are refused before generated development ticket registration. See the signed-device contract for the owner’s stock-Pi exemption, trust enrollment, supported algorithms and unavailable device-runtime work. No Python projection, case outcome or trace label proves external execution.

Sidecars and host actions

Kubernetes mutation authority

Kubernetes mutations use its HTTPS API with an explicitly configured CA and service-account credential reference. Cordon tests both immutable UID and resourceVersion atomically. Drain uses policy/v1 Eviction with UID/version preconditions, retains DaemonSet, mirror and terminal-pod exclusions, and respects disruption budgets. It does not force-delete workloads. Terminal success requires the same cordoned node identity and no remaining eligible pods. Transport ambiguity or a pending disruption budget leaves the admitted operation unresolved for reconciliation rather than publishing success.

Sidecar mounts and providers are manifest-gated. Namespace collisions receive deterministic hash-prefixed labels; role and path scopes are checked on each operation. Offline spool and replay are bounded by selected manifest limits and must not exceed Secure9P msize. Sidecars do not add in-VM listeners.

Host actions under /host/tickets/* are requests, not implicit target access to the host. The host ticket agent validates schema, action allowlist, arguments, idempotency, and state before a configured host adapter performs a side effect. Use dedicated host identities, least-privilege adapter configuration, and the request/result/federation contracts in Interfaces.

M28 selected jobs place their standing scope and cumulative ledger under one private host custody point shared by the gateway and native ticket agent. The compiler permits only GPU workload submission and an enrolled systemd restart; the deployment scope may narrow action, exact target, subject, expiry, budget, concurrency, retry and cooldown. Both selected effects cost one budget unit. The gateway derives current target or native facts before durable reservation; the agent rechecks the source binding and facts at native dispatch. A local file lock serializes spending, and a synchronized replacement retains the same admission identity across restart. Unknown native termination keeps its allocation. Revocation prevents new dispatch; it does not erase or terminate an existing effect. A cancellation request is not native termination.

These are host-enforced limits. A privileged host administrator, another gateway/agent using a different ledger, or a legacy raw host-ticket delegation that independently permits the same action can bypass this standing budget. Deployers must keep one selected custody point and attenuate legacy tickets to the intended action paths. Ledger and scope files are protected local state, not cryptographic proof of native execution. The target’s ticket, Worker, lease and writer-epoch checks remain independent of host standing decisions.

Recipe recovery and cached results

The host recipe journal is private local controller state, not execution authority. An exclusive owner lock, synchronized atomic replacement, immutable operation/topology binding and finite cumulative attempts protect submission identity. Cache keys and accounting are recomputed from retained input contracts; result acceptance always rechecks independently enrolled signed evidence and actual output hashes. Owner control of a journal cannot grant target or native authority. Keep the controller state and evidence enrollment under distinct appropriate custody; the journal is not a cryptographic attestation of a DAG.

A lost ACK retains uncertainty and its resource reservation. Recovery reconciles the existing native and ticket journals; it never silently dispatches an old grant. New execution/cancellation uses current exact root/host authority and state checks. Reuse across revisions requires current scoped ticket visibility, fresh compatible device/runtime publication and the bounded reuse age, while historical offline inspection refreshes no authority. Native termination is required before release; a cancellation request alone cannot establish it. Local diagnostic case attachments are sanitized and retain proof none.

Bounded GPU workload host transport

The optional GPU executor uses the generated providers.gpu_executor contract: a private Unix socket, HMAC-SHA256 authenticated request and response frames, 16 KiB frame bound, one active CUDA context, 64 retained jobs, and a 4 MiB WAL. Its explicit cohesix-gpu-executor-config/v1 deployment file binds the GPU ID, physical CUDA UUID, exact helper SHA-256, provider graph, writer epoch, socket, private state root, and secret reference. The reference profile is CUDA 13.2.2 on Orin Nano; MIG is unavailable on that profile. Native host administration remains outside this authority boundary.

Run gpu-bridge-host --workload-config /absolute/config.json as the owner of that private state. Select host-ticket-agent --gpu-executor-socket PATH --gpu-executor-credential-ref env:NAME --gpu-request-root PATH --execution-lanes 2 on the same host. The secret value is never an argument or evidence field. The agent reads only root-admitted v2 requests, checks the exact ready Worker and active root lease, and renews a one-second bridge grant while both remain current. A changed lease sequence, Worker generation, expired ticket, lost agent, or disconnected control plane revokes execution. Cancellation completes only after the CUDA child has been killed and reaped. Bridge restart records interruption and never replays the operation. Retained successful output hashes are checked again before returning a stored result; full retention produces backpressure.

coh gpu [connection options] workload --action gpu.workload.submit --spec FILE (and the corresponding cancel/observe actions) writes only /host/tickets/spec. Python client.gpu_workload_ticket(spec) follows the same path. A submission ACK is not a provider or Worker terminal receipt. Input CAS JSON uses the canonical Rust workload::Input serialization, is limited to 8192 bytes, and is stored as <sha256>.json. The agent cannot select an executable path through a ticket. The bridge independently rechecks device topology, free-memory headroom, every output element, and the expected output digest before reporting success.

When the GPU executor is selected, lane zero is reserved for lease, cancel, and observe operations. Submissions and other provider work use the remaining lanes. This keeps cancellation serviceable during CUDA execution. The durable lane topology includes this selection; changing it requires a fresh journal root after existing operations are reconciled.

Field-bus action and snapshot boundary

The field-bus contract keeps MODBUS/DNP3 protocol I/O host-side. Compiler-owned endpoint/point maps reject arbitrary addresses, functions and control payloads. Read-only is the default; controls require an independently signed admitted ticket binding the exact map, target, writer epoch, manifest and native component. Durable attempt state precedes wire I/O. Missing control ACKs remain ambiguous and cannot be replayed after restart. A new compensating control requires separate admission.

Base MODBUS/DNP3 framing does not authenticate the physical device. Protocol ACKs and local host signatures cannot imply plant behavior or device attestation. Native OS/network permissions and independently verified endpoint ownership remain deployment responsibilities. The service renderer permits only compiled serial devices and retains private devices for TCP-only configurations. Field-bus snapshots are admin-only by default, preserve the original ACK expiry, omit raw control payloads and withdraw on stale/failed/missing points. They never become an action grant, Worker receipt or physical device proof.

Content-addressed storage

CAS updates are file-backed and Queen-writable; they do not create another network service. Chunks are verified by SHA-256, invalid content is quarantined and audited, and signature requirements are selected by the manifest. A delta must identify and validate a non-delta base epoch before it can be accepted.

CAS integrity stance (generated)

• cas.signing.required: true
• Hash mismatches are rejected, quarantined, and audited without side effects.
• Signature failures emit deterministic ERR plus audit entries.
• /models exposure remains gated by ecosystem.models.enable.

Generated by coh-rtc (sha256: 674f8c3ed5412b48f6d8e4804d75735aa6b40237b15fa0be463f06e777132101).

Generated observability limits

Observability tolerances (generated)

• observability.proc_ingest.latency_samples: 32
• observability.proc_ingest.latency_tolerance_ms: 5
• observability.proc_ingest.counter_tolerance: 1
• observability.proc_ingest.watch_min_interval_ms: 50

Generated by coh-rtc (sha256: aae20e12321a8a009e32d6e163c28d7ab51ca76a211a6ef0f1dd753f88b1c6ce).

The generated cohsh pooling, retry, heartbeat, and trace limits are owned by docs/snippets/cohsh_ticket_policy.md and embedded in Userland and CLI; they are not a second security policy.

Telemetry Ring Latency (generated)

• Suite: nine-door/telemetry_ring
• Samples: 7
• P50: 0.014 ms
• P95: 0.025 ms
• Unit: ms Generated from apps/nine-door/out/metrics/telemetry_ring_latency.json.

This generated microbenchmark record is regression evidence for its named suite, not an end-to-end deployment latency claim. Benchmark methodology and publishable report requirements live in Benchmarks. Developers refresh the snippet and this embedded projection together:

scripts/ci/update_latency_metrics.sh \
  apps/nine-door/out/metrics/telemetry_ring_latency.json \
  docs/snippets/latency_metrics.md docs/SECURITY.md

Profile-qualified security claims

The committed default manifest is not universal deployment policy. Security claims must identify the selected source manifest, resolved manifest hash, seL4 output profile, target, commit, and evidence run. Features disabled by that profile are absent, not protected by an undocumented fallback.

Current target status and proof boundaries are maintained in Hardware bring-up and the Build plan. The NIST 800-53 crosswalk is an evidence index, not a certification; see NIST mapping.