From aa97f2998daf4c0421104d46a3aacd6ade934062 Mon Sep 17 00:00:00 2001 From: Roone Date: Sun, 27 Sep 2026 20:21:57 -0600 Subject: [PATCH 01/15] Open initial-spec: cead as a system, in TLA+ Co-Authored-By: Claude Opus 5.5 (1M context) From e705f5d89baa413e5b0b9982e82a698826f23e45 Mon Sep 17 00:00:00 2001 From: Roone Date: Sun, 27 Sep 2026 20:46:10 -0600 Subject: [PATCH 02/15] Sort the vocabulary so a noun can be found Co-Authored-By: Claude Opus 5.5 (1M context) --- CODE.md | 54 +++++++++++++++++++++++++++--------------------------- 1 file changed, 27 insertions(+), 27 deletions(-) diff --git a/CODE.md b/CODE.md index 8b45aa9..5a6dfb4 100644 --- a/CODE.md +++ b/CODE.md @@ -33,42 +33,42 @@ Every noun has one home in code: a type, a module or crate, or a binary. A noun | Noun | Meaning | Home | |---|---|---| -| cead | The project, the operator's binary, and its shell over a declaration and its state. | crate and binary `cead` | -| operator | The human at depth 0. Types `cead` or `cead run`; never types a call. | | -| machine | The unit: pinned kernel, core, task image, descriptors, calls, policy and model endpoint, booted in a microVM by a backend. | | -| declaration | The one file that pins a machine. Equal declarations are the same experiment; its hashes are the version vector. | | +| authority | How far a binary can go beyond its argv: fixed, launcher, client, interpreter, service. | | | backend | What boots a machine: Firecracker on Linux, Virtualization.framework on macOS. Same guest, same evidence. | | -| init | PID 1 in the guest. Assembles the view (task image as root, overlay, core first on PATH, descriptors), applies policy, execs the harness. | | -| harness | The Rust program in the machine, its memory manager. Runs each process's cycle, installs kernel policy in the fork-exec gap, supplies the calls, writes receipts. | | -| process | One harness cycle with its own cgroup, window, shell, limits and budget. Started by `run` at depth 0 or by `rlm` below it. | | -| run | One machine, one root process and its tree, one log. From the operator shell or one-shot `cead run`; the machine ends with it. | | -| step | One command and its observation. The unit of budget and of measurement. | | -| window | The context the model can address now. A cache over state. | | -| pinned | The part of the window eviction never touches: the system prompt. | | | bounded | Output admitted to the window, constructible only by truncation. The remainder **spills** to a file. | | -| limit | A cap on one process: window size, bound, steps, wall time. The rlimit analogue: set in the fork-exec gap, inherited as a copy. | | | budget | What a process tree may spend. A parent moves part of what remains into each child, never copies it. What it counts is declaration policy. | | -| slice | The bytes a child receives on stdin, sealed. | | -| descriptor | State the model holds this session, bound to an object with rights. Minted by cead, never discovered; a capability. A child's is **attenuated**. | | -| command | What the model writes: shell over the core plus the task image. | | -| core | The invariant tools every machine has: brush, uutils, grep, git, sqlite3. nix-built, static, first on PATH. | | -| task image | The tools one task brings: a read-only OCI image with a label declaring its tools, attached at boot. | | -| query | The argv of `run` or `rlm`, commit-message sized. Anything longer is context. | | | call | A command whose effect is on the harness: `rlm`, `finish`. | | | call table | The single source; renders builtins, exec policy, prompt lines, man pages. | | +| cead | The project, the operator's binary, and its shell over a declaration and its state. | crate and binary `cead` | +| command | What the model writes: shell over the core plus the task image. | | +| contract | One of the three lines everything else is swappable between. | | +| core | The invariant tools every machine has: brush, uutils, grep, git, sqlite3. nix-built, static, first on PATH. | | +| declaration | The one file that pins a machine. Equal declarations are the same experiment; its hashes are the version vector. | | +| descriptor | State the model holds this session, bound to an object with rights. Minted by cead, never discovered; a capability. A child's is **attenuated**. | | +| evict | Dispose at any tier: window span, KV block, process, machine. | | +| harness | The Rust program in the machine, its memory manager. Runs each process's cycle, installs kernel policy in the fork-exec gap, supplies the calls, writes receipts. | | +| init | PID 1 in the guest. Assembles the view (task image as root, overlay, core first on PATH, descriptors), applies policy, execs the harness. | | +| limit | A cap on one process: window size, bound, steps, wall time. The rlimit analogue: set in the fork-exec gap, inherited as a copy. | | +| log | The append-only sequence of receipts, a flat file on the host. A finished run cites its hash. | | +| machine | The unit: pinned kernel, core, task image, descriptors, calls, policy and model endpoint, booted in a microVM by a backend. | | | membrane | The calls as boundary: untyped argv and stdin in, typed request inside, text and exit code out. | | -| rights | What a call may do to state: read, write. | | -| authority | How far a binary can go beyond its argv: fixed, launcher, client, interpreter, service. | | -| policy | The rows of the call table in Cedar, compiled to seccomp and Landlock, installed before exec. Permit-all is a declared policy, not an absence. | | -| verdict | The adjudication of a command: permit or forbid. | | +| model endpoint | Where inference is, reached only through the host proxy; keys never enter the guest. | | | observer | eBPF keyed by cgroup, outside the model's reach. | | +| operator | The human at depth 0. Types `cead` or `cead run`; never types a call. | | +| pinned | The part of the window eviction never touches: the system prompt. | | +| policy | The rows of the call table in Cedar, compiled to seccomp and Landlock, installed before exec. Permit-all is a declared policy, not an absence. | | +| process | One harness cycle with its own cgroup, window, shell, limits and budget. Started by `run` at depth 0 or by `rlm` below it. | | +| query | The argv of `run` or `rlm`, commit-message sized. Anything longer is context. | | | receipt | One record per command, three streams under one invocation id: intent, adjudication, witness. | | -| log | The append-only sequence of receipts, a flat file on the host. A finished run cites its hash. | | -| snapshot | The whole guest at an instant. The fork mechanism. | | -| model endpoint | Where inference is, reached only through the host proxy; keys never enter the guest. | | -| contract | One of the three lines everything else is swappable between. | | +| rights | What a call may do to state: read, write. | | | ring | A privilege layer: model processes; harness and observer; host. | | -| evict | Dispose at any tier: window span, KV block, process, machine. | | +| run | One machine, one root process and its tree, one log. From the operator shell or one-shot `cead run`; the machine ends with it. | | +| slice | The bytes a child receives on stdin, sealed. | | +| snapshot | The whole guest at an instant. The fork mechanism. | | +| step | One command and its observation. The unit of budget and of measurement. | | +| task image | The tools one task brings: a read-only OCI image with a label declaring its tools, attached at boot. | | +| verdict | The adjudication of a command: permit or forbid. | | +| window | The context the model can address now. A cache over state. | | # Rust From a2d9c6fc1ce054811f1f17c6bd925557a0fffaea Mon Sep 17 00:00:00 2001 From: Roone Date: Sun, 27 Sep 2026 21:13:30 -0600 Subject: [PATCH 03/15] Name the host, drop guest for machine, keep the log outside the machine Co-Authored-By: Claude Opus 5.5 (1M context) --- CODE.md | 20 ++++++++++---------- README.md | 11 ++++++----- 2 files changed, 16 insertions(+), 15 deletions(-) diff --git a/CODE.md b/CODE.md index 5a6dfb4..5877069 100644 --- a/CODE.md +++ b/CODE.md @@ -22,7 +22,7 @@ Spec, skeleton, fill. TLA+, Lean and Rust are one pipeline, not alternatives: TL ## Boundaries -- Which side of which contract is new code on: model-facing, guest tool, harness, observer, host? What is its source of stability: written spec, ABI promise, pinned version, none? Below the ABI, what re-validates it when the pinned kernel changes? +- Which side of which contract is new code on: model-facing, machine tool, harness, observer, host? What is its source of stability: written spec, ABI promise, pinned version, none? Below the ABI, what re-validates it when the pinned kernel changes? - The model's side is untyped and GNU-flavoured. Types live between the shell and the kernel, never in the shell. Widening the model-facing surface is GNU-flavoured POSIX or a third call in disguise. - The call table is the single source: builtins, exec policy, prompt lines and man text render from it, never a second list. Two calls; new capability arrives as state or a well-known CLI. - A dependency's types stay inside the boundary module that wraps it. The skeleton names our nouns; swapping a dependency is a module change. @@ -34,10 +34,10 @@ Every noun has one home in code: a type, a module or crate, or a binary. A noun | Noun | Meaning | Home | |---|---|---| | authority | How far a binary can go beyond its argv: fixed, launcher, client, interpreter, service. | | -| backend | What boots a machine: Firecracker on Linux, Virtualization.framework on macOS. Same guest, same evidence. | | +| backend | What boots a machine: Firecracker on Linux, Virtualization.framework on macOS. Same machine, same evidence. | | | bounded | Output admitted to the window, constructible only by truncation. The remainder **spills** to a file. | | | budget | What a process tree may spend. A parent moves part of what remains into each child, never copies it. What it counts is declaration policy. | | -| call | A command whose effect is on the harness: `rlm`, `finish`. | | +| call | A command whose effect is on the harness: `rlm`, `finish`. Untyped argv and stdin in, text and exit code out; typed only inside. | | | call table | The single source; renders builtins, exec policy, prompt lines, man pages. | | | cead | The project, the operator's binary, and its shell over a declaration and its state. | crate and binary `cead` | | command | What the model writes: shell over the core plus the task image. | | @@ -47,12 +47,12 @@ Every noun has one home in code: a type, a module or crate, or a binary. A noun | descriptor | State the model holds this session, bound to an object with rights. Minted by cead, never discovered; a capability. A child's is **attenuated**. | | | evict | Dispose at any tier: window span, KV block, process, machine. | | | harness | The Rust program in the machine, its memory manager. Runs each process's cycle, installs kernel policy in the fork-exec gap, supplies the calls, writes receipts. | | -| init | PID 1 in the guest. Assembles the view (task image as root, overlay, core first on PATH, descriptors), applies policy, execs the harness. | | +| host | What runs a machine: hardware, a kernel with a hypervisor, the backend's process and `cead`. The model cannot reach it. | | +| init | PID 1 in the machine. Assembles the view (task image as root, overlay, core first on PATH, descriptors), applies policy, execs the harness. | | | limit | A cap on one process: window size, bound, steps, wall time. The rlimit analogue: set in the fork-exec gap, inherited as a copy. | | -| log | The append-only sequence of receipts, a flat file on the host. A finished run cites its hash. | | +| log | The append-only sequence of receipts, held outside the machine. A finished run cites its hash. | | | machine | The unit: pinned kernel, core, task image, descriptors, calls, policy and model endpoint, booted in a microVM by a backend. | | -| membrane | The calls as boundary: untyped argv and stdin in, typed request inside, text and exit code out. | | -| model endpoint | Where inference is, reached only through the host proxy; keys never enter the guest. | | +| model endpoint | Where inference is, reached only through the host proxy; keys never enter the machine. | | | observer | eBPF keyed by cgroup, outside the model's reach. | | | operator | The human at depth 0. Types `cead` or `cead run`; never types a call. | | | pinned | The part of the window eviction never touches: the system prompt. | | @@ -64,7 +64,7 @@ Every noun has one home in code: a type, a module or crate, or a binary. A noun | ring | A privilege layer: model processes; harness and observer; host. | | | run | One machine, one root process and its tree, one log. From the operator shell or one-shot `cead run`; the machine ends with it. | | | slice | The bytes a child receives on stdin, sealed. | | -| snapshot | The whole guest at an instant. The fork mechanism. | | +| snapshot | The whole machine at an instant. The fork mechanism. | | | step | One command and its observation. The unit of budget and of measurement. | | | task image | The tools one task brings: a read-only OCI image with a label declaring its tools, attached at boot. | | | verdict | The adjudication of a command: permit or forbid. | | @@ -100,8 +100,8 @@ Everything else (fields, structs and enums, most traits, invariants like `len - `Cargo.toml` and `clippy.toml` lints are the rules. `cargo check` on every edit; `cargo clippy --all-targets -- -D warnings` and `cargo test` green before ready. Frontier lints warn, so a draft compiles and a ready PR cannot. - eBPF program crates alone lift `unsafe_code`, in their own `Cargo.toml`, visibly. - `Cargo.toml` is the allowlist: no new dependency without approval. Preferences: rustix, never libc directly; clap derive; anyhow in binaries, thiserror in libraries; serde. Boundary crates: rustix, aya, seccompiler, landlock. -- One published crate, `cead`. When the workspace splits (core, guest, observer, host, backends) members are `publish = false`. -- Host crates build on macOS: rustix with its libc backend, std, nothing Linux-specific. A Linux-only crate in the host tree is the axis being violated. Guest crates are `#![cfg(target_os = "linux")]` and use linux_raw and Linux-only crates freely. +- One published crate, `cead`. When the workspace splits (core, machine, observer, host, backends) members are `publish = false`. +- Host crates build on macOS: rustix with its libc backend, std, nothing Linux-specific. A Linux-only crate in the host tree is the axis being violated. Machine crates are `#![cfg(target_os = "linux")]` and use linux_raw and Linux-only crates freely. - The core is nix-built and static. # TLA+ diff --git a/README.md b/README.md index 349fd84..304a59f 100644 --- a/README.md +++ b/README.md @@ -28,7 +28,7 @@ Three contracts; everything between two lines is swappable. | Line | Contract | |---|---| -| backend ↔ guest | boot protocol and virtio | +| backend ↔ machine | boot protocol and virtio | | kernel ↔ commands | Linux syscall ABI | | commands ↔ model | POSIX sh, GNU flags and error text | @@ -134,12 +134,13 @@ Work fans out three ways, told apart by who spawns and when: - Authority is per tool: how far a tool can go beyond what its command line says. `grep` does only what its arguments say; `python` can do anything the process may. The class picks the tool's kernel policy and says how to read its trace. -- The host is out of reach. - API keys, the grader and the log stay on the host. +- The host is out of reach, and trusted. + API keys and the grader stay on the host; the log is held outside the machine. + cead trusts the host's operator and hardware. ### Hardware -Two backends boot the same guest and leave the same evidence: Firecracker on Linux, Virtualization.framework on macOS. +Two backends boot the same machine and leave the same evidence: Firecracker on Linux, Virtualization.framework on macOS. The host needs a hypervisor and nothing else. ### Network @@ -179,6 +180,6 @@ Rules beyond that come with the first release. - eBPF records what the model's processes do: which programs they start, which files they read, and each call to the model endpoint. - Every action has a cause. The observer is keyed by cgroup, so each action is attributed to the command that caused it, however many processes that command spawned. -- The log is one entry per command, written on the host. +- The log is one receipt per command, held outside the machine. The operator reads it from the CLI, live during a run and after. - Cost per command is a first-release measurement. From c879be2e3e77c3bcabf898623620083b745ad53b Mon Sep 17 00:00:00 2001 From: Roone Date: Sun, 27 Sep 2026 21:35:13 -0600 Subject: [PATCH 04/15] Name cead in its lineage: calls, meters, audit records, VMMs, tracer Co-Authored-By: Claude Opus 5.5 (1M context) --- CODE.md | 44 +++++++++++++++++++++++--------------------- README.md | 42 +++++++++++++++++++++--------------------- 2 files changed, 44 insertions(+), 42 deletions(-) diff --git a/CODE.md b/CODE.md index 5877069..79d430e 100644 --- a/CODE.md +++ b/CODE.md @@ -22,9 +22,9 @@ Spec, skeleton, fill. TLA+, Lean and Rust are one pipeline, not alternatives: TL ## Boundaries -- Which side of which contract is new code on: model-facing, machine tool, harness, observer, host? What is its source of stability: written spec, ABI promise, pinned version, none? Below the ABI, what re-validates it when the pinned kernel changes? +- Which side of which interface is new code on: model-facing, machine tool, harness, tracer, host? What is its source of stability: written spec, ABI promise, pinned version, none? Below the ABI, what re-validates it when the pinned kernel changes? - The model's side is untyped and GNU-flavoured. Types live between the shell and the kernel, never in the shell. Widening the model-facing surface is GNU-flavoured POSIX or a third call in disguise. -- The call table is the single source: builtins, exec policy, prompt lines and man text render from it, never a second list. Two calls; new capability arrives as state or a well-known CLI. +- The call table is the single source: builtins, exec policy, prompt lines and man text render from it, never a second list. New capability arrives as state or a well-known CLI. - A dependency's types stay inside the boundary module that wraps it. The skeleton names our nouns; swapping a dependency is a module change. # Vocabulary @@ -33,41 +33,43 @@ Every noun has one home in code: a type, a module or crate, or a binary. A noun | Noun | Meaning | Home | |---|---|---| +| audit record | One per call, in three parts under the call's id: intent, decision, witness. Linux audit's shape. | | | authority | How far a binary can go beyond its argv: fixed, launcher, client, interpreter, service. | | -| backend | What boots a machine: Firecracker on Linux, Virtualization.framework on macOS. Same machine, same evidence. | | | bounded | Output admitted to the window, constructible only by truncation. The remainder **spills** to a file. | | -| budget | What a process tree may spend. A parent moves part of what remains into each child, never copies it. What it counts is declaration policy. | | -| call | A command whose effect is on the harness: `rlm`, `finish`. Untyped argv and stdin in, text and exit code out; typed only inside. | | -| call table | The single source; renders builtins, exec policy, prompt lines, man pages. | | -| cead | The project, the operator's binary, and its shell over a declaration and its state. | crate and binary `cead` | +| call | One command the model issues and what it gets back: a system call into the harness. Untyped argv and stdin in, text and exit code out. The unit of limits and measurement. cead adds `rlm` and `finish`; every other call is a well-known CLI. | | +| call table | The system call table: the toolset. | | +| cead | The project, the operator's binary, and its shell over a manifest and its state. | crate and binary `cead` | | command | What the model writes: shell over the core plus the task image. | | -| contract | One of the three lines everything else is swappable between. | | | core | The invariant tools every machine has: brush, uutils, grep, git, sqlite3. nix-built, static, first on PATH. | | -| declaration | The one file that pins a machine. Equal declarations are the same experiment; its hashes are the version vector. | | +| crash | The machine ends without `finish`. | | +| decision | The outcome of checking a call against policy: allow or deny. | | | descriptor | State the model holds this session, bound to an object with rights. Minted by cead, never discovered; a capability. A child's is **attenuated**. | | | evict | Dispose at any tier: window span, KV block, process, machine. | | -| harness | The Rust program in the machine, its memory manager. Runs each process's cycle, installs kernel policy in the fork-exec gap, supplies the calls, writes receipts. | | -| host | What runs a machine: hardware, a kernel with a hypervisor, the backend's process and `cead`. The model cannot reach it. | | +| executed | What the kernel ran: the truth an audit record records. | | +| harness | The Rust program in the machine: the model's kernel. Runs each process, installs kernel policy in the fork-exec gap, serves the calls, writes audit records. | | +| host | What runs a machine: hardware, a kernel with a hypervisor, the VMM's process and `cead`. The model cannot reach it. | | | init | PID 1 in the machine. Assembles the view (task image as root, overlay, core first on PATH, descriptors), applies policy, execs the harness. | | -| limit | A cap on one process: window size, bound, steps, wall time. The rlimit analogue: set in the fork-exec gap, inherited as a copy. | | -| log | The append-only sequence of receipts, held outside the machine. A finished run cites its hash. | | -| machine | The unit: pinned kernel, core, task image, descriptors, calls, policy and model endpoint, booted in a microVM by a backend. | | +| interface | One of the three lines everything else is swappable between. | | +| limit | A cap on one process: window size, bound, calls, wall time. The rlimit analogue: set in the fork-exec gap, inherited as a copy. | | +| log | The append-only sequence of audit records, held outside the machine. A finished run cites its hash. | | +| machine | The unit: pinned kernel, core, task image, descriptors, call table, policy and model endpoint, booted in a microVM by a VMM. | | +| manifest | The one file that pins a machine by content. Equal manifests are the same experiment; its hashes are the version vector. | | +| message | One part of an audit record in transit to the log. Can be lost, delayed, reordered, duplicated or forged; the log accepts only what the machine sent. | | +| meter | What a process tree may spend, from KeyKOS. A child's meter hangs below its parent's; every spend is charged to each meter above it, so a tree never outspends its root. A parent can cap or revoke a child's meter. What it counts is manifest policy. | | | model endpoint | Where inference is, reached only through the host proxy; keys never enter the machine. | | -| observer | eBPF keyed by cgroup, outside the model's reach. | | | operator | The human at depth 0. Types `cead` or `cead run`; never types a call. | | | pinned | The part of the window eviction never touches: the system prompt. | | | policy | The rows of the call table in Cedar, compiled to seccomp and Landlock, installed before exec. Permit-all is a declared policy, not an absence. | | -| process | One harness cycle with its own cgroup, window, shell, limits and budget. Started by `run` at depth 0 or by `rlm` below it. | | +| process | An OS process running one harness cycle, with its own cgroup, window, shell, limits and meter; each call runs as its child. Running, ready, blocked or zombie. Started by `run` at depth 0, `rlm` below. | | | query | The argv of `run` or `rlm`, commit-message sized. Anything longer is context. | | -| receipt | One record per command, three streams under one invocation id: intent, adjudication, witness. | | | rights | What a call may do to state: read, write. | | -| ring | A privilege layer: model processes; harness and observer; host. | | +| ring | A privilege layer: model processes; harness and tracer; host. | | | run | One machine, one root process and its tree, one log. From the operator shell or one-shot `cead run`; the machine ends with it. | | | slice | The bytes a child receives on stdin, sealed. | | | snapshot | The whole machine at an instant. The fork mechanism. | | -| step | One command and its observation. The unit of budget and of measurement. | | | task image | The tools one task brings: a read-only OCI image with a label declaring its tools, attached at boot. | | -| verdict | The adjudication of a command: permit or forbid. | | +| tracer | eBPF in the machine's kernel, keyed by cgroup, outside the model's reach. Produces the witness. | | +| VMM | What boots a machine: Firecracker on Linux, Virtualization.framework on macOS. Same machine, same evidence. | | | window | The context the model can address now. A cache over state. | | # Rust @@ -100,7 +102,7 @@ Everything else (fields, structs and enums, most traits, invariants like `len - `Cargo.toml` and `clippy.toml` lints are the rules. `cargo check` on every edit; `cargo clippy --all-targets -- -D warnings` and `cargo test` green before ready. Frontier lints warn, so a draft compiles and a ready PR cannot. - eBPF program crates alone lift `unsafe_code`, in their own `Cargo.toml`, visibly. - `Cargo.toml` is the allowlist: no new dependency without approval. Preferences: rustix, never libc directly; clap derive; anyhow in binaries, thiserror in libraries; serde. Boundary crates: rustix, aya, seccompiler, landlock. -- One published crate, `cead`. When the workspace splits (core, machine, observer, host, backends) members are `publish = false`. +- One published crate, `cead`. When the workspace splits (core, machine, tracer, host, VMMs) members are `publish = false`. - Host crates build on macOS: rustix with its libc backend, std, nothing Linux-specific. A Linux-only crate in the host tree is the axis being violated. Machine crates are `#![cfg(target_os = "linux")]` and use linux_raw and Linux-only crates freely. - The core is nix-built and static. diff --git a/README.md b/README.md index 304a59f..0d95751 100644 --- a/README.md +++ b/README.md @@ -24,11 +24,11 @@ The context window is a cache; the model's state lives in the machine, in files, A script that stands up a service, runs forty commands and prints `ok` has advanced the task by forty commands and cost the context window one line. All forty ran under kernel policy and were recorded, whether or not the model mentioned them. -Three contracts; everything between two lines is swappable. +Three interfaces; everything between two lines is swappable. -| Line | Contract | +| Line | Interface | |---|---| -| backend ↔ machine | boot protocol and virtio | +| VMM ↔ machine | boot protocol and virtio | | kernel ↔ commands | Linux syscall ABI | | commands ↔ model | POSIX sh, GNU flags and error text | @@ -60,19 +60,19 @@ System diagram to come with the first release. Install instructions come with the first release. -A declaration is one file that names a machine: kernel, task image, policy, backend, and model endpoint. +A manifest is one file that names a machine: kernel, task image, policy, VMM, and model endpoint. Two ways to run it: -- `cead` boots the machine the declaration describes and opens a shell over it. +- `cead` boots the machine the manifest describes and opens a shell over it. Each command in that shell is one operator verb; `run` starts the model. - `cead run` does one run from your own shell and returns. argv is the query, stdin is the context, stdout is the answer, and the exit code is the outcome. A query is the length of a commit message; anything longer is a file in the machine for the model to read. -What a run does, from declaration to first command: +What a run does, from manifest to first command: -1. The backend boots one kernel and attaches two read-only disks: the core (cead's tools, policy and eBPF programs, built by nix) and the task image. +1. The VMM boots one kernel and attaches two read-only disks: the core (cead's tools, policy and eBPF programs, built by nix) and the task image. 2. init runs as root, before any model process exists. It loads the eBPF programs into the kernel and compiles the policy into a seccomp filter and a Landlock ruleset. 3. init mounts one filesystem: the task image as root, the core first on PATH, and each descriptor (context on stdin, checkout, scratch, database file). @@ -99,21 +99,21 @@ Example run and screen recording to come with the first release. | kernel | Linux: cgroup v2, seccomp, Landlock, vsock; eBPF via aya | | shell and tools | brush, uutils, SQLite | | policy | Cedar | -| backends | Firecracker on Linux, Virtualization.framework on macOS | +| VMMs | Firecracker on Linux, Virtualization.framework on macOS | | images and build | OCI images, nix | ## Deployment The machine runs wherever the cead CLI runs: a laptop or a cloud VM with a hypervisor. -The model runs wherever the declaration's endpoint is: a hosted API or a local server. -The CLI drives everything below: it reads the declaration, boots, runs, snapshots, forks, and reads the log. +The model runs wherever the manifest's endpoint is: a hosted API or a local server. +The CLI drives everything below: it reads the manifest, boots, runs, snapshots, forks, and reads the log. The machine is the unit of scale. Work fans out three ways, told apart by who spawns and when: | Use | Who spawns | When | Mechanism | |---|---|---|---| -| evals | operator | before the run | scale-out: N machines from one declaration | +| evals | operator | before the run | scale-out: N machines from one manifest | | reinforcement learning | operator or trainer | mid-run, at a chosen state | fork: K machines from one snapshot, the way a git worktree forks a checkout | | long or autonomous tasks | the model | whenever it decides | `rlm`: a sub-agent process inside the machine | @@ -124,8 +124,8 @@ Work fans out three ways, told apart by who spawns and when: - The machine is the boundary. Everything a run can touch is inside one disposable microVM, so the questions that usually need users, roles and sessions collapse to one: which machine. -- A declaration answers it by hash. - Two machines with the same declaration are the same experiment. +- A manifest answers it by hash. + Two machines with the same manifest are the same experiment. - Operator and model are told apart by where they stand. The operator runs the CLI on the host; the model runs inside the machine as an unprivileged user. - Access is granted; content is discovered. @@ -140,7 +140,7 @@ Work fans out three ways, told apart by who spawns and when: ### Hardware -Two backends boot the same machine and leave the same evidence: Firecracker on Linux, Virtualization.framework on macOS. +Two VMMs boot the same machine and leave the same evidence: Firecracker on Linux, Virtualization.framework on macOS. The host needs a hypervisor and nothing else. ### Network @@ -153,11 +153,11 @@ Rules beyond that come with the first release. - Build time. A task's tools are packed into a read-only OCI image; a SWE-bench instance image works as is. -- Each step. +- Each call. The harness assembles the context window from the system prompt, the query and the bounded output of every command so far, and sends it to the model endpoint. - It runs the command that comes back and adds the output, cut at a size cap, to the next step; the full output goes to a file the model can read piecewise. + It runs the command that comes back and adds the output, cut at a size cap, to the window; the full output goes to a file the model can read piecewise. - Recursion, inside the machine. - `rlm` starts a child process with a slice of the parent's context, part of its budget, the same tools, and its own context window. + `rlm` starts a child process with a slice of the parent's context, a meter under its parent's, the same tools, and its own context window. It is a sub-agent, built from process structure rather than at the application layer. - Forking, of the machine. A snapshot of a running machine boots another machine that diverges from the same state. @@ -177,9 +177,9 @@ Rules beyond that come with the first release. ### Observability -- eBPF records what the model's processes do: which programs they start, which files they read, and each call to the model endpoint. +- eBPF records what the model's processes do: which programs they start, which files they read, and each request to the model endpoint. - Every action has a cause. - The observer is keyed by cgroup, so each action is attributed to the command that caused it, however many processes that command spawned. -- The log is one receipt per command, held outside the machine. + The tracer is keyed by cgroup, so each action is attributed to the command that caused it, however many processes that command spawned. +- The log is one audit record per call, held outside the machine. The operator reads it from the CLI, live during a run and after. -- Cost per command is a first-release measurement. +- Cost per call is a first-release measurement. From 770237105782481410841bb1ee88a4dd8b337ce7 Mon Sep 17 00:00:00 2001 From: Roone Date: Sun, 27 Sep 2026 23:09:10 -0600 Subject: [PATCH 05/15] Specify layer 1: one job, one boot, one process (TLC 2.19; 2 commands, 1 denied, 3 calls) Co-Authored-By: Claude Opus 5.5 (1M context) --- spec/cead.cfg | 24 +++++ spec/cead.tla | 251 ++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 275 insertions(+) create mode 100644 spec/cead.cfg create mode 100644 spec/cead.tla diff --git a/spec/cead.cfg b/spec/cead.cfg new file mode 100644 index 0000000..295e031 --- /dev/null +++ b/spec/cead.cfg @@ -0,0 +1,24 @@ +CONSTANTS + Commands = {c1, c2} + Policy = {c2} + CallLimit = 3 + NoMsg = NoMsg + +SPECIFICATION Spec + +INVARIANTS + TypeOK + IntentFirst + DenyNeverRuns + WithinLimit + OnlyMachine + ExecutedOnce + Unambiguous + FinishHonest + Complete + +PROPERTIES + LogOnlyGrows + JobEnds + +CHECK_DEADLOCK FALSE diff --git a/spec/cead.tla b/spec/cead.tla new file mode 100644 index 0000000..da1b1f8 --- /dev/null +++ b/spec/cead.tla @@ -0,0 +1,251 @@ +-------------------------------- MODULE cead -------------------------------- +(***************************************************************************) +(* cead as a system. Layer 1: one job, one boot, one process. *) +(***************************************************************************) +EXTENDS Naturals, Sequences + +CONSTANTS + Commands, \* what the model can write; the spec never sees shell text + Policy, \* the commands the policy denies; {} is permit-all + CallLimit, \* the limit on calls for one process + NoMsg \* a model value: no message awaiting acknowledgment + +ASSUME /\ Policy \subseteq Commands + /\ CallLimit \in Nat + +Decision(c) == IF c \in Policy THEN "deny" ELSE "allow" + +Parts == {"intent", "decision", "witness"} \* of one call's audit record +Reasons == {"finish", "timeout"} \* what an exit record can say +Senders == {"machine", "path"} \* whose key signed a message +MaxSeq == 3 * CallLimit + 1 \* every part of every call, then the exit + +\* One link in the machine's chain. `seq` is its place in the chain: the +\* order the machine sent it, whatever order it arrives in. An audit record +\* part carries its call's id and command; the exit record carries id 0 and +\* how the machine exited. +Message == [seq : 1..MaxSeq, id : 0..CallLimit, part : Parts \cup {"exit"}, + body : Commands \cup Reasons, sender : Senders] + +VARIABLES + machine, \* "off", "up", "exiting", "evicted" + process, \* "initial", "running", "blocked", "zombie" + calls, \* calls issued so far; the current call's id + seq, \* the machine's last sequence number + pending, \* the message awaiting the log's acknowledgment, or NoMsg + executed, \* what the kernel ran, in order: the truth + messages, \* in transit: can be lost, delayed, reordered, duplicated + log \* held outside the machine: the record, a set of links + +vars == <> + +Msg(s, i, p, b) == [seq |-> s, id |-> i, part |-> p, body |-> b, sender |-> "machine"] +Logged(s) == \E m \in log : m.seq = s +LoggedPart(i, p) == \E m \in log : m.id = i /\ m.part = p + +----------------------------------------------------------------------------- +(* The machine and its process *) + +Init == + /\ machine = "off" + /\ process = "initial" + /\ calls = 0 + /\ seq = 0 + /\ pending = NoMsg + /\ executed = <<>> + /\ messages = {} + /\ log = {} + +\* The VMM boots the machine, init assembles the view, the harness starts +\* the root process. +Boot == + /\ machine = "off" + /\ machine' = "up" + /\ process' = "running" + /\ UNCHANGED <> + +\* The model issues a call. The harness blocks the process and sends the +\* intent, which awaits acknowledgment. +Issue(c) == + /\ machine = "up" + /\ process = "running" + /\ calls < CallLimit + /\ process' = "blocked" + /\ calls' = calls + 1 + /\ seq' = seq + 1 + /\ pending' = Msg(seq + 1, calls + 1, "intent", c) + /\ messages' = messages \cup {pending'} + /\ UNCHANGED <> + +\* The log has not acknowledged the pending message: send it again. +Resend == + /\ machine \in {"up", "exiting"} + /\ pending # NoMsg + /\ ~Logged(pending.seq) + /\ messages' = messages \cup {pending} + /\ UNCHANGED <> + +\* The log has acknowledged the intent: the harness checks the call against +\* policy. Deny returns to the model. Allow runs the command, and the tracer +\* witnesses it; both parts go through the harness, which sequences them. +Decide == + /\ machine = "up" + /\ process = "blocked" + /\ pending # NoMsg + /\ pending.part = "intent" + /\ Logged(pending.seq) + /\ LET c == pending.body + i == pending.id + IN IF Decision(c) = "allow" + THEN /\ executed' = Append(executed, [id |-> i, cmd |-> c]) + /\ messages' = messages \cup + {Msg(seq + 1, i, "decision", c), Msg(seq + 2, i, "witness", c)} + /\ seq' = seq + 2 + ELSE /\ executed' = executed + /\ messages' = messages \cup {Msg(seq + 1, i, "decision", c)} + /\ seq' = seq + 1 + /\ process' = "running" + /\ pending' = NoMsg + /\ UNCHANGED <> + +\* The model calls `finish`: the process is a zombie until the harness reaps it. +Finish == + /\ machine = "up" + /\ process = "running" + /\ process' = "zombie" + /\ UNCHANGED <> + +\* The machine signs its exit record, the last link in its chain, and waits +\* for the log to acknowledge it. Any call in progress is cut off. +Exit(reason) == + /\ machine = "up" + /\ machine' = "exiting" + /\ seq' = seq + 1 + /\ pending' = Msg(seq + 1, 0, "exit", reason) + /\ messages' = messages \cup {pending'} + /\ UNCHANGED <> + +\* The harness reaps the root process. +Reap == process = "zombie" /\ Exit("finish") +\* The machine's own wall-time limit fires. +Timeout == Exit("timeout") + +\* The log has the exit record: the machine is gone. +Leave == + /\ machine = "exiting" + /\ Logged(pending.seq) + /\ machine' = "evicted" + /\ pending' = NoMsg + /\ UNCHANGED <> + +\* The machine ends without an acknowledged exit record. A crash can happen +\* at any point. The host's hard kill is the same event, but it is assumed +\* to happen (see Spec): it is what makes every job end. +Evict == + /\ machine \in {"up", "exiting"} + /\ machine' = "evicted" + /\ pending' = NoMsg + /\ UNCHANGED <> + +Crash == Evict +HostKill == Evict + +----------------------------------------------------------------------------- +(* Messages: outside the machine, so they go on after it is evicted *) + +\* The log keeps a message only if the machine signed it, and keeps the first +\* message for each place in the chain. A duplicate or resend changes nothing. +\* First-wins matters only if the machine's key is stolen, which this spec +\* assumes away, so TLC never exercises it. +Arrive(m) == + /\ m.sender = "machine" + /\ ~Logged(m.seq) + /\ log' = log \cup {m} + /\ UNCHANGED <> + +Deliver(m) == m \in messages /\ Arrive(m) + +Lose(m) == + /\ m \in messages + /\ messages' = messages \ {m} + /\ UNCHANGED <> + +\* Anything on the path, the host included, can send the log a message at +\* any moment, but can sign only as itself. A forgery affects nothing until +\* it reaches the log, so it is modelled as arriving there directly. +Forge(m) == m.sender = "path" /\ Arrive(m) + +----------------------------------------------------------------------------- + +Next == + \/ Boot + \/ \E c \in Commands : Issue(c) + \/ Resend + \/ Decide + \/ Finish + \/ Reap + \/ Timeout + \/ Leave + \/ Crash + \/ HostKill + \/ \E m \in messages : Deliver(m) \/ Lose(m) + \/ \E m \in Message : Forge(m) + +Spec == Init /\ [][Next]_vars /\ WF_vars(HostKill) + +----------------------------------------------------------------------------- +(* Properties *) + +TypeOK == + /\ machine \in {"off", "up", "exiting", "evicted"} + /\ process \in {"initial", "running", "blocked", "zombie"} + /\ calls \in Nat + /\ seq \in Nat + /\ pending \in Message \cup {NoMsg} + /\ executed \in Seq([id : 1..CallLimit, cmd : Commands]) + /\ messages \subseteq Message + /\ log \subseteq Message + +\* 1. Nothing is executed before its intent is in the log. +IntentFirst == \A k \in 1..Len(executed) : LoggedPart(executed[k].id, "intent") + +\* 2. The log only gains links. +LogOnlyGrows == [][log \subseteq log']_log + +\* 3. Nothing whose decision is deny is executed. +DenyNeverRuns == \A k \in 1..Len(executed) : Decision(executed[k].cmd) = "allow" + +\* 4. A process makes at most CallLimit calls. +WithinLimit == calls <= CallLimit + +\* 5. Every job that starts ends, and its machine is evicted. +JobEnds == (machine = "up") ~> (machine = "evicted") + +\* 6. The log holds only what the machine signed. +OnlyMachine == \A m \in log : m.sender = "machine" + +\* 7. Each call is executed at most once. +ExecutedOnce == + \A j, k \in 1..Len(executed) : j # k => executed[j].id # executed[k].id + +\* 8. The machine never signs two different messages for one place in the +\* chain, so the chain gives one order. +Unambiguous == + LET Seen == {m \in messages : m.sender = "machine"} \cup + log + IN \A m1, m2 \in Seen : m1.seq = m2.seq => m1 = m2 + +\* 9. An exit record saying `finish` means the model called `finish`: no +\* call was cut off. +FinishHonest == + \A m \in log : (m.part = "exit" /\ m.body = "finish") => process = "zombie" + +\* 10. An exit record with an unbroken chain before it proves the log +\* complete: every executed call has all three parts logged. +Complete == + \A x \in log : + (x.part = "exit" /\ \A s \in 1..x.seq - 1 : Logged(s)) + => \A e \in 1..Len(executed) : + \A p \in Parts : LoggedPart(executed[e].id, p) + +============================================================================= From d7d7438a9a4b012ab573005f875c6df2c76d57ba Mon Sep 17 00:00:00 2001 From: Roone Date: Sun, 27 Sep 2026 23:09:32 -0600 Subject: [PATCH 06/15] Name the job, the processor and the security triad the spec relies on Co-Authored-By: Claude Opus 5.5 (1M context) --- CODE.md | 14 +++++++++----- README.md | 18 +++++++++--------- 2 files changed, 18 insertions(+), 14 deletions(-) diff --git a/CODE.md b/CODE.md index 79d430e..e79e6da 100644 --- a/CODE.md +++ b/CODE.md @@ -35,36 +35,40 @@ Every noun has one home in code: a type, a module or crate, or a binary. A noun |---|---|---| | audit record | One per call, in three parts under the call's id: intent, decision, witness. Linux audit's shape. | | | authority | How far a binary can go beyond its argv: fixed, launcher, client, interpreter, service. | | +| availability | The job runs and ends. The host guarantees it, and can always deny it. | `spec/cead.tla` | | bounded | Output admitted to the window, constructible only by truncation. The remainder **spills** to a file. | | | call | One command the model issues and what it gets back: a system call into the harness. Untyped argv and stdin in, text and exit code out. The unit of limits and measurement. cead adds `rlm` and `finish`; every other call is a well-known CLI. | | | call table | The system call table: the toolset. | | | cead | The project, the operator's binary, and its shell over a manifest and its state. | crate and binary `cead` | | command | What the model writes: shell over the core plus the task image. | | +| confidentiality | No one outside the machine can read it. Only the confidential backend claims it, guaranteed by its processor. | | | core | The invariant tools every machine has: brush, uutils, grep, git, sqlite3. nix-built, static, first on PATH. | | -| crash | The machine ends without `finish`. | | +| crash | The machine ends without an acknowledged exit record. The job is unknown. | `spec/cead.tla` | | decision | The outcome of checking a call against policy: allow or deny. | | | descriptor | State the model holds this session, bound to an object with rights. Minted by cead, never discovered; a capability. A child's is **attenuated**. | | | evict | Dispose at any tier: window span, KV block, process, machine. | | -| executed | What the kernel ran: the truth an audit record records. | | +| executed | What the kernel ran: the truth an audit record records. | `spec/cead.tla` | | harness | The Rust program in the machine: the model's kernel. Runs each process, installs kernel policy in the fork-exec gap, serves the calls, writes audit records. | | | host | What runs a machine: hardware, a kernel with a hypervisor, the VMM's process and `cead`. The model cannot reach it. | | | init | PID 1 in the machine. Assembles the view (task image as root, overlay, core first on PATH, descriptors), applies policy, execs the harness. | | +| integrity | The log says only what the machine signed, in the machine's order. Guaranteed by the machine's signature and hash chain. | `spec/cead.tla` | | interface | One of the three lines everything else is swappable between. | | +| job | One query's work: a root process, its tree, one log. Started by `cead run`. Spans one boot until recovery resumes it on another. | | | limit | A cap on one process: window size, bound, calls, wall time. The rlimit analogue: set in the fork-exec gap, inherited as a copy. | | -| log | The append-only sequence of audit records, held outside the machine. A finished run cites its hash. | | +| log | The machine's signed hash chain of audit records, ending in its exit record (`finish` or `timeout`), held outside the machine. With the exit record and no gap, provably complete; without it, the job is unknown. | `spec/cead.tla` | | machine | The unit: pinned kernel, core, task image, descriptors, call table, policy and model endpoint, booted in a microVM by a VMM. | | | manifest | The one file that pins a machine by content. Equal manifests are the same experiment; its hashes are the version vector. | | -| message | One part of an audit record in transit to the log. Can be lost, delayed, reordered, duplicated or forged; the log accepts only what the machine sent. | | +| message | One link of the machine's chain in transit to the log. Can be lost, delayed, reordered, duplicated or forged; the log accepts only what the machine signed. | `spec/cead.tla` | | meter | What a process tree may spend, from KeyKOS. A child's meter hangs below its parent's; every spend is charged to each meter above it, so a tree never outspends its root. A parent can cap or revoke a child's meter. What it counts is manifest policy. | | | model endpoint | Where inference is, reached only through the host proxy; keys never enter the machine. | | | operator | The human at depth 0. Types `cead` or `cead run`; never types a call. | | | pinned | The part of the window eviction never touches: the system prompt. | | | policy | The rows of the call table in Cedar, compiled to seccomp and Landlock, installed before exec. Permit-all is a declared policy, not an absence. | | | process | An OS process running one harness cycle, with its own cgroup, window, shell, limits and meter; each call runs as its child. Running, ready, blocked or zombie. Started by `run` at depth 0, `rlm` below. | | +| processor | What a process runs on. For the machine, the CPU; for the model's process, the inference engine behind the model endpoint. | | | query | The argv of `run` or `rlm`, commit-message sized. Anything longer is context. | | | rights | What a call may do to state: read, write. | | | ring | A privilege layer: model processes; harness and tracer; host. | | -| run | One machine, one root process and its tree, one log. From the operator shell or one-shot `cead run`; the machine ends with it. | | | slice | The bytes a child receives on stdin, sealed. | | | snapshot | The whole machine at an instant. The fork mechanism. | | | task image | The tools one task brings: a read-only OCI image with a label declaring its tools, attached at boot. | | diff --git a/README.md b/README.md index 0d95751..72af2c8 100644 --- a/README.md +++ b/README.md @@ -48,8 +48,8 @@ System diagram to come with the first release. - Not a container runtime. cead uses container images and container schedulers, and replaces the container itself with a microVM. - Not a conversation. - Nothing carries between runs except state in the machine. - A run's context window is the system prompt, the query, and what the model has read since. + Nothing carries between jobs except state in the machine. + A job's context window is the system prompt, the query, and what the model has read since. - Not a policy. You bring your own, written in Cedar, and cead compiles it into kernel rules; cead does not decide what a model should be allowed to do. - Not a new interface for the model. @@ -70,7 +70,7 @@ Two ways to run it: A query is the length of a commit message; anything longer is a file in the machine for the model to read. -What a run does, from manifest to first command: +What a job does, from manifest to first command: 1. The VMM boots one kernel and attaches two read-only disks: the core (cead's tools, policy and eBPF programs, built by nix) and the task image. 2. init runs as root, before any model process exists. @@ -113,8 +113,8 @@ Work fans out three ways, told apart by who spawns and when: | Use | Who spawns | When | Mechanism | |---|---|---|---| -| evals | operator | before the run | scale-out: N machines from one manifest | -| reinforcement learning | operator or trainer | mid-run, at a chosen state | fork: K machines from one snapshot, the way a git worktree forks a checkout | +| evals | operator | before the job | scale-out: N machines from one manifest | +| reinforcement learning | operator or trainer | mid-job, at a chosen state | fork: K machines from one snapshot, the way a git worktree forks a checkout | | long or autonomous tasks | the model | whenever it decides | `rlm`: a sub-agent process inside the machine | - Kubernetes can schedule machines as pods; Firecracker was built for this shape of workload. @@ -123,7 +123,7 @@ Work fans out three ways, told apart by who spawns and when: ### Identity - The machine is the boundary. - Everything a run can touch is inside one disposable microVM, so the questions that usually need users, roles and sessions collapse to one: which machine. + Everything a job can touch is inside one disposable microVM, so the questions that usually need users, roles and sessions collapse to one: which machine. - A manifest answers it by hash. Two machines with the same manifest are the same experiment. - Operator and model are told apart by where they stand. @@ -162,7 +162,7 @@ Rules beyond that come with the first release. - Forking, of the machine. A snapshot of a running machine boots another machine that diverges from the same state. - Finish. - `finish` ends a process with its answer; when the root process finishes, the run is over and the machine is gone. + `finish` ends a process with its answer; when the root process finishes, the job is over and the machine is gone. ### Data @@ -172,7 +172,7 @@ Rules beyond that come with the first release. - Postgres is a task tool for tasks that need extensions, concurrency or an existing data directory. It runs inside the machine, so a snapshot still captures it. - State leaves the machine on purpose. - A run's answer is stdout; a checkout can be pushed; a snapshot can be exported. + A job's answer is stdout; a checkout can be pushed; a snapshot can be exported. Nothing else leaves. ### Observability @@ -181,5 +181,5 @@ Rules beyond that come with the first release. - Every action has a cause. The tracer is keyed by cgroup, so each action is attributed to the command that caused it, however many processes that command spawned. - The log is one audit record per call, held outside the machine. - The operator reads it from the CLI, live during a run and after. + The operator reads it from the CLI, live during a job and after. - Cost per call is a first-release measurement. From a272ef0e8ff9216e47b0827a442eb98d63cbde30 Mon Sep 17 00:00:00 2001 From: Roone Date: Sun, 27 Sep 2026 23:29:53 -0600 Subject: [PATCH 07/15] Name the model's side: weights, engine, scheduler, and one host per executor Co-Authored-By: Claude Opus 5.5 (1M context) --- CODE.md | 16 ++++++++++------ README.md | 15 ++++++++------- 2 files changed, 18 insertions(+), 13 deletions(-) diff --git a/CODE.md b/CODE.md index e79e6da..cfe4619 100644 --- a/CODE.md +++ b/CODE.md @@ -39,41 +39,45 @@ Every noun has one home in code: a type, a module or crate, or a binary. A noun | bounded | Output admitted to the window, constructible only by truncation. The remainder **spills** to a file. | | | call | One command the model issues and what it gets back: a system call into the harness. Untyped argv and stdin in, text and exit code out. The unit of limits and measurement. cead adds `rlm` and `finish`; every other call is a well-known CLI. | | | call table | The system call table: the toolset. | | -| cead | The project, the operator's binary, and its shell over a manifest and its state. | crate and binary `cead` | +| cead | The project and the operator's binary. With no verb, it opens the console. | crate and binary `cead` | | command | What the model writes: shell over the core plus the task image. | | | confidentiality | No one outside the machine can read it. Only the confidential backend claims it, guaranteed by its processor. | | +| console | The operator's interface to manifests, machines and their state: `cead` with no verb. Its verbs drive the scheduler. | | | core | The invariant tools every machine has: brush, uutils, grep, git, sqlite3. nix-built, static, first on PATH. | | | crash | The machine ends without an acknowledged exit record. The job is unknown. | `spec/cead.tla` | | decision | The outcome of checking a call against policy: allow or deny. | | | descriptor | State the model holds this session, bound to an object with rights. Minted by cead, never discovered; a capability. A child's is **attenuated**. | | +| engine | Executes the weights and signs what it produces: the model's counterpart to the machine. vLLM by default. | | | evict | Dispose at any tier: window span, KV block, process, machine. | | | executed | What the kernel ran: the truth an audit record records. | `spec/cead.tla` | | harness | The Rust program in the machine: the model's kernel. Runs each process, installs kernel policy in the fork-exec gap, serves the calls, writes audit records. | | -| host | What runs a machine: hardware, a kernel with a hypervisor, the VMM's process and `cead`. The model cannot reach it. | | +| host | What runs a machine or an engine: hardware, its processors, and what schedules onto them. Trusted for availability only; the model's processes cannot reach it. | | | init | PID 1 in the machine. Assembles the view (task image as root, overlay, core first on PATH, descriptors), applies policy, execs the harness. | | | integrity | The log says only what the machine signed, in the machine's order. Guaranteed by the machine's signature and hash chain. | `spec/cead.tla` | | interface | One of the three lines everything else is swappable between. | | | job | One query's work: a root process, its tree, one log. Started by `cead run`. Spans one boot until recovery resumes it on another. | | | limit | A cap on one process: window size, bound, calls, wall time. The rlimit analogue: set in the fork-exec gap, inherited as a copy. | | -| log | The machine's signed hash chain of audit records, ending in its exit record (`finish` or `timeout`), held outside the machine. With the exit record and no gap, provably complete; without it, the job is unknown. | `spec/cead.tla` | -| machine | The unit: pinned kernel, core, task image, descriptors, call table, policy and model endpoint, booted in a microVM by a VMM. | | +| log | The machine's signed hash chain of audit records, ending in its exit record (`finish` or `timeout`), held outside the machine. With the exit record and no gap, provably complete; without it, the job is unknown. One writer per chain: never consensus. | `spec/cead.tla` | +| machine | The unit: pinned kernel, core, task image, descriptors, call table, policy and model, booted in a microVM by a VMM. | | | manifest | The one file that pins a machine by content. Equal manifests are the same experiment; its hashes are the version vector. | | | message | One link of the machine's chain in transit to the log. Can be lost, delayed, reordered, duplicated or forged; the log accepts only what the machine signed. | `spec/cead.tla` | | meter | What a process tree may spend, from KeyKOS. A child's meter hangs below its parent's; every spend is charged to each meter above it, so a tree never outspends its root. A parent can cap or revoke a child's meter. What it counts is manifest policy. | | -| model endpoint | Where inference is, reached only through the host proxy; keys never enter the machine. | | +| model | The machine's user: weights running on an engine, reached by the harness over TLS that every host between only relays. Keys never reach the model's processes. | | | operator | The human at depth 0. Types `cead` or `cead run`; never types a call. | | | pinned | The part of the window eviction never touches: the system prompt. | | | policy | The rows of the call table in Cedar, compiled to seccomp and Landlock, installed before exec. Permit-all is a declared policy, not an absence. | | | process | An OS process running one harness cycle, with its own cgroup, window, shell, limits and meter; each call runs as its child. Running, ready, blocked or zombie. Started by `run` at depth 0, `rlm` below. | | -| processor | What a process runs on. For the machine, the CPU; for the model's process, the inference engine behind the model endpoint. | | +| processor | What a process runs on. For the machine, the CPU; for the model, the GPU, a coprocessor to the model's process. | | | query | The argv of `run` or `rlm`, commit-message sized. Anything longer is context. | | | rights | What a call may do to state: read, write. | | | ring | A privilege layer: model processes; harness and tracer; host. | | +| scheduler | Decides what runs where: machines on hosts, requests on engines. Trusted for availability only; needs consensus once there is more than one. | | | slice | The bytes a child receives on stdin, sealed. | | | snapshot | The whole machine at an instant. The fork mechanism. | | | task image | The tools one task brings: a read-only OCI image with a label declaring its tools, attached at boot. | | | tracer | eBPF in the machine's kernel, keyed by cgroup, outside the model's reach. Produces the witness. | | | VMM | What boots a machine: Firecracker on Linux, Virtualization.framework on macOS. Same machine, same evidence. | | +| weights | The model's program text, pinned by hash in the manifest. Part of the version vector. | | | window | The context the model can address now. A cache over state. | | # Rust diff --git a/README.md b/README.md index 72af2c8..36b6e7c 100644 --- a/README.md +++ b/README.md @@ -60,7 +60,7 @@ System diagram to come with the first release. Install instructions come with the first release. -A manifest is one file that names a machine: kernel, task image, policy, VMM, and model endpoint. +A manifest is one file that names a machine: kernel, task image, policy, VMM, and the model: its weights and engine. Two ways to run it: - `cead` boots the machine the manifest describes and opens a shell over it. @@ -78,7 +78,7 @@ What a job does, from manifest to first command: 3. init mounts one filesystem: the task image as root, the core first on PATH, and each descriptor (context on stdin, checkout, scratch, database file). 4. The harness forks the root process, attaches the policy, drops to an unprivileged uid, and execs the shell. Every child inherits the policy; no process can remove it. -5. The harness renders the system prompt from what it mounted, so it cannot claim what is not there, and sends it with the query to the model endpoint. +5. The harness renders the system prompt from what it mounted, so it cannot claim what is not there, and sends it with the query to the engine. 6. The model writes its first command. Three kinds of file, three fates: @@ -105,7 +105,7 @@ Example run and screen recording to come with the first release. ## Deployment The machine runs wherever the cead CLI runs: a laptop or a cloud VM with a hypervisor. -The model runs wherever the manifest's endpoint is: a hosted API or a local server. +The model runs wherever the manifest's engine is: a hosted API or a local server. The CLI drives everything below: it reads the manifest, boots, runs, snapshots, forks, and reads the log. The machine is the unit of scale. @@ -135,7 +135,7 @@ Work fans out three ways, told apart by who spawns and when: `grep` does only what its arguments say; `python` can do anything the process may. The class picks the tool's kernel policy and says how to read its trace. - The host is out of reach, and trusted. - API keys and the grader stay on the host; the log is held outside the machine. + The grader stays on the host, API keys never reach the model's processes, and the log is held outside the machine. cead trusts the host's operator and hardware. ### Hardware @@ -146,7 +146,8 @@ The host needs a hypervisor and nothing else. ### Network The model's processes have no network. -The machine reaches the host over vsock only, through a proxy, for inference and for the log. +The machine reaches the host over vsock only. +The host relays inference, encrypted between the harness and the engine, and the machine's messages to the log. Rules beyond that come with the first release. ### Workloads @@ -154,7 +155,7 @@ Rules beyond that come with the first release. - Build time. A task's tools are packed into a read-only OCI image; a SWE-bench instance image works as is. - Each call. - The harness assembles the context window from the system prompt, the query and the bounded output of every command so far, and sends it to the model endpoint. + The harness assembles the context window from the system prompt, the query and the bounded output of every command so far, and sends it to the engine. It runs the command that comes back and adds the output, cut at a size cap, to the window; the full output goes to a file the model can read piecewise. - Recursion, inside the machine. `rlm` starts a child process with a slice of the parent's context, a meter under its parent's, the same tools, and its own context window. @@ -177,7 +178,7 @@ Rules beyond that come with the first release. ### Observability -- eBPF records what the model's processes do: which programs they start, which files they read, and each request to the model endpoint. +- eBPF records what the model's processes do: which programs they start, which files they read, and each request to the engine. - Every action has a cause. The tracer is keyed by cgroup, so each action is attributed to the command that caused it, however many processes that command spawned. - The log is one audit record per call, held outside the machine. From dc9b03c9aa3403a64c13ddc243793a6340afbc99 Mon Sep 17 00:00:00 2001 From: Roone Date: Sun, 27 Sep 2026 23:32:09 -0600 Subject: [PATCH 08/15] Keep long-lived keys on the host; the machine holds a job-scoped token Co-Authored-By: Claude Opus 5.5 (1M context) --- CODE.md | 2 +- README.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CODE.md b/CODE.md index cfe4619..693907a 100644 --- a/CODE.md +++ b/CODE.md @@ -62,7 +62,7 @@ Every noun has one home in code: a type, a module or crate, or a binary. A noun | manifest | The one file that pins a machine by content. Equal manifests are the same experiment; its hashes are the version vector. | | | message | One link of the machine's chain in transit to the log. Can be lost, delayed, reordered, duplicated or forged; the log accepts only what the machine signed. | `spec/cead.tla` | | meter | What a process tree may spend, from KeyKOS. A child's meter hangs below its parent's; every spend is charged to each meter above it, so a tree never outspends its root. A parent can cap or revoke a child's meter. What it counts is manifest policy. | | -| model | The machine's user: weights running on an engine, reached by the harness over TLS that every host between only relays. Keys never reach the model's processes. | | +| model | The machine's user: weights running on an engine, reached by the harness over TLS that every host between only relays. The machine holds only a job-scoped token, never a long-lived key. | | | operator | The human at depth 0. Types `cead` or `cead run`; never types a call. | | | pinned | The part of the window eviction never touches: the system prompt. | | | policy | The rows of the call table in Cedar, compiled to seccomp and Landlock, installed before exec. Permit-all is a declared policy, not an absence. | | diff --git a/README.md b/README.md index 36b6e7c..2d80ed5 100644 --- a/README.md +++ b/README.md @@ -135,7 +135,7 @@ Work fans out three ways, told apart by who spawns and when: `grep` does only what its arguments say; `python` can do anything the process may. The class picks the tool's kernel policy and says how to read its trace. - The host is out of reach, and trusted. - The grader stays on the host, API keys never reach the model's processes, and the log is held outside the machine. + The grader and long-lived API keys stay on the host; the machine holds only a token scoped to its job, and the log is held outside the machine. cead trusts the host's operator and hardware. ### Hardware From 6bb45c9580b2895e1ef72a00dbd69aa0cbc7214b Mon Sep 17 00:00:00 2001 From: Roone Date: Mon, 28 Sep 2026 20:07:43 -0600 Subject: [PATCH 09/15] Make the confidential machine the default: boots, reports, and a host trusted only to keep jobs running Co-Authored-By: Claude Opus 5.5 (1M context) --- CODE.md | 12 +++++++----- README.md | 26 ++++++++++++++++---------- 2 files changed, 23 insertions(+), 15 deletions(-) diff --git a/CODE.md b/CODE.md index 693907a..1591e2e 100644 --- a/CODE.md +++ b/CODE.md @@ -36,12 +36,13 @@ Every noun has one home in code: a type, a module or crate, or a binary. A noun | audit record | One per call, in three parts under the call's id: intent, decision, witness. Linux audit's shape. | | | authority | How far a binary can go beyond its argv: fixed, launcher, client, interpreter, service. | | | availability | The job runs and ends. The host guarantees it, and can always deny it. | `spec/cead.tla` | +| boot | One life of a machine's kernel, from the VMM starting it to eviction. One key, one report, one chain; a boot from a snapshot is a new boot. Linux's `boot_id`. | `spec/cead.tla` | | bounded | Output admitted to the window, constructible only by truncation. The remainder **spills** to a file. | | | call | One command the model issues and what it gets back: a system call into the harness. Untyped argv and stdin in, text and exit code out. The unit of limits and measurement. cead adds `rlm` and `finish`; every other call is a well-known CLI. | | | call table | The system call table: the toolset. | | | cead | The project and the operator's binary. With no verb, it opens the console. | crate and binary `cead` | | command | What the model writes: shell over the core plus the task image. | | -| confidentiality | No one outside the machine can read it. Only the confidential backend claims it, guaranteed by its processor. | | +| confidentiality | No one outside the machine can read it. Guaranteed by the processor on an attested boot; claimed by no one in trusted-host mode. | | | console | The operator's interface to manifests, machines and their state: `cead` with no verb. Its verbs drive the scheduler. | | | core | The invariant tools every machine has: brush, uutils, grep, git, sqlite3. nix-built, static, first on PATH. | | | crash | The machine ends without an acknowledged exit record. The job is unknown. | `spec/cead.tla` | @@ -53,11 +54,11 @@ Every noun has one home in code: a type, a module or crate, or a binary. A noun | harness | The Rust program in the machine: the model's kernel. Runs each process, installs kernel policy in the fork-exec gap, serves the calls, writes audit records. | | | host | What runs a machine or an engine: hardware, its processors, and what schedules onto them. Trusted for availability only; the model's processes cannot reach it. | | | init | PID 1 in the machine. Assembles the view (task image as root, overlay, core first on PATH, descriptors), applies policy, execs the harness. | | -| integrity | The log says only what the machine signed, in the machine's order. Guaranteed by the machine's signature and hash chain. | `spec/cead.tla` | +| integrity | The log says only what the machine signed, in the machine's order. Guaranteed by the machine's signature and hash chain, rooted in its report. | `spec/cead.tla` | | interface | One of the three lines everything else is swappable between. | | | job | One query's work: a root process, its tree, one log. Started by `cead run`. Spans one boot until recovery resumes it on another. | | | limit | A cap on one process: window size, bound, calls, wall time. The rlimit analogue: set in the fork-exec gap, inherited as a copy. | | -| log | The machine's signed hash chain of audit records, ending in its exit record (`finish` or `timeout`), held outside the machine. With the exit record and no gap, provably complete; without it, the job is unknown. One writer per chain: never consensus. | `spec/cead.tla` | +| log | The machine's signed hash chains, one per boot, held outside the machine: a report first, audit records, an exit record (`finish` or `timeout`) last. A chain with its exit record and no gap is provably complete; without it, the boot is unknown. A job's chains link through their reports. One writer per chain: never consensus. | `spec/cead.tla` | | machine | The unit: pinned kernel, core, task image, descriptors, call table, policy and model, booted in a microVM by a VMM. | | | manifest | The one file that pins a machine by content. Equal manifests are the same experiment; its hashes are the version vector. | | | message | One link of the machine's chain in transit to the log. Can be lost, delayed, reordered, duplicated or forged; the log accepts only what the machine signed. | `spec/cead.tla` | @@ -69,14 +70,15 @@ Every noun has one home in code: a type, a module or crate, or a binary. A noun | process | An OS process running one harness cycle, with its own cgroup, window, shell, limits and meter; each call runs as its child. Running, ready, blocked or zombie. Started by `run` at depth 0, `rlm` below. | | | processor | What a process runs on. For the machine, the CPU; for the model, the GPU, a coprocessor to the model's process. | | | query | The argv of `run` or `rlm`, commit-message sized. Anything longer is context. | | +| report | The first link of every chain: the processor's signed statement binding the boot's key, and for a fork the parent's chain head, to the manifest's measurement. Unsigned in trusted-host mode. Linux's TSM report. | `spec/cead.tla` | | rights | What a call may do to state: read, write. | | | ring | A privilege layer: model processes; harness and tracer; host. | | | scheduler | Decides what runs where: machines on hosts, requests on engines. Trusted for availability only; needs consensus once there is more than one. | | | slice | The bytes a child receives on stdin, sealed. | | -| snapshot | The whole machine at an instant. The fork mechanism. | | +| snapshot | The whole machine at an instant. The fork mechanism: boot from it, with a new key. | | | task image | The tools one task brings: a read-only OCI image with a label declaring its tools, attached at boot. | | | tracer | eBPF in the machine's kernel, keyed by cgroup, outside the model's reach. Produces the witness. | | -| VMM | What boots a machine: Firecracker on Linux, Virtualization.framework on macOS. Same machine, same evidence. | | +| VMM | What boots a machine: Cloud Hypervisor, attested on SEV-SNP or unattested on KVM; Firecracker and Virtualization.framework, unattested. Same machine, same chain; only an attested boot's report is signed. | | | weights | The model's program text, pinned by hash in the manifest. Part of the version vector. | | | window | The context the model can address now. A cache over state. | | diff --git a/README.md b/README.md index 2d80ed5..e9edea2 100644 --- a/README.md +++ b/README.md @@ -6,18 +6,23 @@ cead (Irish: permission; "kyad")

-cead is an agent harness built as a microVM: a userspace whose user is a model. +cead is an agent harness built as a confidential microVM: a userspace for a model, over a kernel that enforces and witnesses, whose evidence does not depend on who owns the hardware. The model gets a Linux machine of its own and a shell to drive it: the kernel permits each command, and eBPF witnesses it. ## What cead is -A pinned Linux kernel in a microVM. +A pinned Linux kernel in a confidential microVM. The model gets a system prompt and a shell, as in any agent harness. Every command it writes runs as a Linux process under the kernel's own controls: seccomp, Landlock and cgroups. An eBPF program in the kernel records what each process did, in a place the model's processes cannot reach. -Most agent harnesses state their limits in prompt text and application code, then report what happened from inside the process that did it. -cead has the kernel enforce the limits and the kernel write the record, so the report does not depend on the model or the harness telling the truth. +Most agent harnesses state their limits in prompt text and application code, then say what happened from inside the process that did it. +cead has the kernel enforce the limits and the kernel write the record, so the record does not depend on the model or the harness telling the truth. + +Nor does it depend on the host. +The processor attests what booted, and the machine signs its record with a key the host cannot read. +The host can stop a job, but cannot read it or forge its record. +On hardware without attestation, the same machine runs unattested and says so. Harness design is memory-management policy. The context window is a cache; the model's state lives in the machine, in files, and the model reaches it through the shell. @@ -28,7 +33,7 @@ Three interfaces; everything between two lines is swappable. | Line | Interface | |---|---| -| VMM ↔ machine | boot protocol and virtio | +| VMM ↔ machine | measured boot, content-addressed disks, attestation; devices are untrusted input | | kernel ↔ commands | Linux syscall ABI | | commands ↔ model | POSIX sh, GNU flags and error text | @@ -99,7 +104,7 @@ Example run and screen recording to come with the first release. | kernel | Linux: cgroup v2, seccomp, Landlock, vsock; eBPF via aya | | shell and tools | brush, uutils, SQLite | | policy | Cedar | -| VMMs | Firecracker on Linux, Virtualization.framework on macOS | +| VMMs | Cloud Hypervisor (SEV-SNP on KVM); Firecracker and Virtualization.framework, unattested | | images and build | OCI images, nix | ## Deployment @@ -134,14 +139,15 @@ Work fans out three ways, told apart by who spawns and when: - Authority is per tool: how far a tool can go beyond what its command line says. `grep` does only what its arguments say; `python` can do anything the process may. The class picks the tool's kernel policy and says how to read its trace. -- The host is out of reach, and trusted. +- The host is out of reach, and untrusted. The grader and long-lived API keys stay on the host; the machine holds only a token scoped to its job, and the log is held outside the machine. - cead trusts the host's operator and hardware. + The host is trusted only to keep a job running: it can stop one, but not read it or forge its log. + Trusted-host mode asserts the rest instead of proving it. ### Hardware -Two VMMs boot the same machine and leave the same evidence: Firecracker on Linux, Virtualization.framework on macOS. -The host needs a hypervisor and nothing else. +Cloud Hypervisor boots attested machines on bare-metal AMD EPYC with SEV-SNP, and the same machine unattested on any KVM host. +Firecracker and Virtualization.framework boot it unattested, so the harness runs where developers are. ### Network From f3865854e3b33066ada9ba1662bdf5a90edc697c Mon Sep 17 00:00:00 2001 From: Roone Date: Mon, 28 Sep 2026 20:30:20 -0600 Subject: [PATCH 10/15] Root each chain in a report: the log learns the machine's key only from the processor (TLC 2.19; 2 commands, 1 denied, 3 calls) Co-Authored-By: Claude Opus 5.5 (1M context) --- spec/cead.cfg | 1 + spec/cead.tla | 75 +++++++++++++++++++++++++++++++++++++-------------- 2 files changed, 56 insertions(+), 20 deletions(-) diff --git a/spec/cead.cfg b/spec/cead.cfg index 295e031..ae4aed2 100644 --- a/spec/cead.cfg +++ b/spec/cead.cfg @@ -16,6 +16,7 @@ INVARIANTS Unambiguous FinishHonest Complete + ReportFirst PROPERTIES LogOnlyGrows diff --git a/spec/cead.tla b/spec/cead.tla index da1b1f8..4fdaf3c 100644 --- a/spec/cead.tla +++ b/spec/cead.tla @@ -1,6 +1,17 @@ -------------------------------- MODULE cead -------------------------------- (***************************************************************************) (* cead as a system. Layer 1: one job, one boot, one process. *) +(* *) +(* Assumptions, and who guarantees each. An attested boot proves them; *) +(* trusted-host mode asserts them. The protocol is the same in both. *) +(* KeySecret Only the machine can sign with its key. *) +(* Attested: the processor. Trusted host: asserted. *) +(* KeyBound Only the processor can sign a report, so a report names *) +(* the key of the boot that made it. *) +(* Attested: the processor. Trusted host: the host. *) +(* Availability is the host's in both modes: it can always stop a job. *) +(* Everything on the path, the host included, is a Dolev-Yao network: it *) +(* can lose, delay, replay and forge messages, but signs only as itself. *) (***************************************************************************) EXTENDS Naturals, Sequences @@ -17,15 +28,18 @@ Decision(c) == IF c \in Policy THEN "deny" ELSE "allow" Parts == {"intent", "decision", "witness"} \* of one call's audit record Reasons == {"finish", "timeout"} \* what an exit record can say -Senders == {"machine", "path"} \* whose key signed a message -MaxSeq == 3 * CallLimit + 1 \* every part of every call, then the exit +Keys == {"machine", "path"} \* who can sign: the boot's key, the path's +Signers == Keys \cup {"processor"} \* the processor signs only reports +MaxSeq == 3 * CallLimit + 2 \* the report, every part of every call, the exit \* One link in the machine's chain. `seq` is its place in the chain: the -\* order the machine sent it, whatever order it arrives in. An audit record -\* part carries its call's id and command; the exit record carries id 0 and -\* how the machine exited. -Message == [seq : 1..MaxSeq, id : 0..CallLimit, part : Parts \cup {"exit"}, - body : Commands \cup Reasons, sender : Senders] +\* order the machine sent it, whatever order it arrives in. The report +\* (seq 1, id 0) names the key the rest of the chain is signed with. An +\* audit record part carries its call's id and command; the exit record +\* carries id 0 and how the machine exited. +Message == [seq : 1..MaxSeq, id : 0..CallLimit, + part : Parts \cup {"report", "exit"}, + body : Commands \cup Reasons \cup Keys, key : Signers] VARIABLES machine, \* "off", "up", "exiting", "evicted" @@ -39,9 +53,12 @@ VARIABLES vars == <> -Msg(s, i, p, b) == [seq |-> s, id |-> i, part |-> p, body |-> b, sender |-> "machine"] +Msg(s, i, p, b) == [seq |-> s, id |-> i, part |-> p, body |-> b, key |-> "machine"] +Report == [seq |-> 1, id |-> 0, part |-> "report", body |-> "machine", key |-> "processor"] Logged(s) == \E m \in log : m.seq = s LoggedPart(i, p) == \E m \in log : m.id = i /\ m.part = p +\* The log holds a processor-signed report naming key k. +Vouched(k) == \E r \in log : r.part = "report" /\ r.key = "processor" /\ r.body = k ----------------------------------------------------------------------------- (* The machine and its process *) @@ -56,13 +73,26 @@ Init == /\ messages = {} /\ log = {} -\* The VMM boots the machine, init assembles the view, the harness starts -\* the root process. +\* The VMM boots the machine. It makes its key and sends the report, the +\* first link of its chain, which awaits acknowledgment. Boot == /\ machine = "off" /\ machine' = "up" + /\ seq' = 1 + /\ pending' = Report + /\ messages' = messages \cup {Report} + /\ UNCHANGED <> + +\* The log holds the report: init assembles the view, the harness starts the +\* root process. Nothing runs on a boot the log has not heard of. +Start == + /\ machine = "up" + /\ process = "initial" + /\ pending = Report + /\ Logged(1) /\ process' = "running" - /\ UNCHANGED <> + /\ pending' = NoMsg + /\ UNCHANGED <> \* The model issues a call. The harness blocks the process and sends the \* intent, which awaits acknowledgment. @@ -153,12 +183,13 @@ HostKill == Evict ----------------------------------------------------------------------------- (* Messages: outside the machine, so they go on after it is evicted *) -\* The log keeps a message only if the machine signed it, and keeps the first -\* message for each place in the chain. A duplicate or resend changes nothing. -\* First-wins matters only if the machine's key is stolen, which this spec -\* assumes away, so TLC never exercises it. +\* The log keeps a report only if the processor signed it, and any other +\* message only if a key it vouched for signed it. It keeps the first +\* message for each place in the chain; a duplicate or resend changes +\* nothing. First-wins matters only if KeySecret fails, so TLC never +\* exercises it. Arrive(m) == - /\ m.sender = "machine" + /\ IF m.part = "report" THEN m.key = "processor" ELSE Vouched(m.key) /\ ~Logged(m.seq) /\ log' = log \cup {m} /\ UNCHANGED <> @@ -173,12 +204,13 @@ Lose(m) == \* Anything on the path, the host included, can send the log a message at \* any moment, but can sign only as itself. A forgery affects nothing until \* it reaches the log, so it is modelled as arriving there directly. -Forge(m) == m.sender = "path" /\ Arrive(m) +Forge(m) == m.key = "path" /\ Arrive(m) ----------------------------------------------------------------------------- Next == \/ Boot + \/ Start \/ \E c \in Commands : Issue(c) \/ Resend \/ Decide @@ -221,8 +253,8 @@ WithinLimit == calls <= CallLimit \* 5. Every job that starts ends, and its machine is evicted. JobEnds == (machine = "up") ~> (machine = "evicted") -\* 6. The log holds only what the machine signed. -OnlyMachine == \A m \in log : m.sender = "machine" +\* 6. The log holds only what the processor signed, or a key it vouched for. +OnlyMachine == \A m \in log : m.key = "processor" \/ Vouched(m.key) \* 7. Each call is executed at most once. ExecutedOnce == @@ -231,7 +263,7 @@ ExecutedOnce == \* 8. The machine never signs two different messages for one place in the \* chain, so the chain gives one order. Unambiguous == - LET Seen == {m \in messages : m.sender = "machine"} \cup + LET Seen == {m \in messages : m.key # "path"} \cup log IN \A m1, m2 \in Seen : m1.seq = m2.seq => m1 = m2 @@ -248,4 +280,7 @@ Complete == => \A e \in 1..Len(executed) : \A p \in Parts : LoggedPart(executed[e].id, p) +\* 11. Nothing runs on a boot until the log holds its report. +ReportFirst == process # "initial" => Vouched("machine") + ============================================================================= From 3c04b0517dede0df451859f5b7ba246bf60b02b8 Mon Sep 17 00:00:00 2001 From: Roone Date: Mon, 28 Sep 2026 20:45:22 -0600 Subject: [PATCH 11/15] Fold audit records, messages, the exit record and the report into one noun, the record, as Linux audit does Co-Authored-By: Claude Opus 5.5 (1M context) --- CODE.md | 24 +++++---- README.md | 4 +- spec/cead.cfg | 2 +- spec/cead.tla | 132 +++++++++++++++++++++++++------------------------- 4 files changed, 80 insertions(+), 82 deletions(-) diff --git a/CODE.md b/CODE.md index 1591e2e..224d6a5 100644 --- a/CODE.md +++ b/CODE.md @@ -33,35 +33,32 @@ Every noun has one home in code: a type, a module or crate, or a binary. A noun | Noun | Meaning | Home | |---|---|---| -| audit record | One per call, in three parts under the call's id: intent, decision, witness. Linux audit's shape. | | | authority | How far a binary can go beyond its argv: fixed, launcher, client, interpreter, service. | | | availability | The job runs and ends. The host guarantees it, and can always deny it. | `spec/cead.tla` | -| boot | One life of a machine's kernel, from the VMM starting it to eviction. One key, one report, one chain; a boot from a snapshot is a new boot. Linux's `boot_id`. | `spec/cead.tla` | +| boot | One life of a machine's kernel, from the VMM starting it to eviction, with one key. Its records form one hash chain signed with that key, its report first. **Complete** when the log holds its records through its exit record with no gap; otherwise **unknown** (crash, host kill, lost report). Linux's `boot_id`. | `spec/cead.tla` | | bounded | Output admitted to the window, constructible only by truncation. The remainder **spills** to a file. | | | call | One command the model issues and what it gets back: a system call into the harness. Untyped argv and stdin in, text and exit code out. The unit of limits and measurement. cead adds `rlm` and `finish`; every other call is a well-known CLI. | | | call table | The system call table: the toolset. | | -| cead | The project and the operator's binary. With no verb, it opens the console. | crate and binary `cead` | +| cead | The project and the operator's binary. | crate and binary `cead` | | command | What the model writes: shell over the core plus the task image. | | | confidentiality | No one outside the machine can read it. Guaranteed by the processor on an attested boot; claimed by no one in trusted-host mode. | | | console | The operator's interface to manifests, machines and their state: `cead` with no verb. Its verbs drive the scheduler. | | | core | The invariant tools every machine has: brush, uutils, grep, git, sqlite3. nix-built, static, first on PATH. | | -| crash | The machine ends without an acknowledged exit record. The job is unknown. | `spec/cead.tla` | | decision | The outcome of checking a call against policy: allow or deny. | | | descriptor | State the model holds this session, bound to an object with rights. Minted by cead, never discovered; a capability. A child's is **attenuated**. | | | engine | Executes the weights and signs what it produces: the model's counterpart to the machine. vLLM by default. | | | evict | Dispose at any tier: window span, KV block, process, machine. | | -| executed | What the kernel ran: the truth an audit record records. | `spec/cead.tla` | -| harness | The Rust program in the machine: the model's kernel. Runs each process, installs kernel policy in the fork-exec gap, serves the calls, writes audit records. | | +| executed | What the kernel ran: the truth the records record. | `spec/cead.tla` | +| harness | The Rust program in the machine: the model's kernel. Runs each process, installs kernel policy in the fork-exec gap, serves the calls, writes records. | | | host | What runs a machine or an engine: hardware, its processors, and what schedules onto them. Trusted for availability only; the model's processes cannot reach it. | | | init | PID 1 in the machine. Assembles the view (task image as root, overlay, core first on PATH, descriptors), applies policy, execs the harness. | | -| integrity | The log says only what the machine signed, in the machine's order. Guaranteed by the machine's signature and hash chain, rooted in its report. | `spec/cead.tla` | +| integrity | The log says only what the machine signed, in the machine's order. Guaranteed by each boot's signature and hash chain, rooted in its report. | `spec/cead.tla` | | interface | One of the three lines everything else is swappable between. | | -| job | One query's work: a root process, its tree, one log. Started by `cead run`. Spans one boot until recovery resumes it on another. | | +| job | One query's work: a root process and its tree. Started by `cead run`. Spans one boot, or more through recovery. | | | limit | A cap on one process: window size, bound, calls, wall time. The rlimit analogue: set in the fork-exec gap, inherited as a copy. | | -| log | The machine's signed hash chains, one per boot, held outside the machine: a report first, audit records, an exit record (`finish` or `timeout`) last. A chain with its exit record and no gap is provably complete; without it, the boot is unknown. A job's chains link through their reports. One writer per chain: never consensus. | `spec/cead.tla` | +| log | Every boot's records, held outside the machine. Records in transit can be lost, delayed, replayed or forged; the log keeps only what the processor or a boot's key signed. A complete boot's records are all it did; an unknown boot's are true but may be partial. A job's boots link through their reports. One writer per boot: never consensus. | `spec/cead.tla` | | machine | The unit: pinned kernel, core, task image, descriptors, call table, policy and model, booted in a microVM by a VMM. | | | manifest | The one file that pins a machine by content. Equal manifests are the same experiment; its hashes are the version vector. | | -| message | One link of the machine's chain in transit to the log. Can be lost, delayed, reordered, duplicated or forged; the log accepts only what the machine signed. | `spec/cead.tla` | | meter | What a process tree may spend, from KeyKOS. A child's meter hangs below its parent's; every spend is charged to each meter above it, so a tree never outspends its root. A parent can cap or revoke a child's meter. What it counts is manifest policy. | | | model | The machine's user: weights running on an engine, reached by the harness over TLS that every host between only relays. The machine holds only a job-scoped token, never a long-lived key. | | | operator | The human at depth 0. Types `cead` or `cead run`; never types a call. | | @@ -70,15 +67,16 @@ Every noun has one home in code: a type, a module or crate, or a binary. A noun | process | An OS process running one harness cycle, with its own cgroup, window, shell, limits and meter; each call runs as its child. Running, ready, blocked or zombie. Started by `run` at depth 0, `rlm` below. | | | processor | What a process runs on. For the machine, the CPU; for the model, the GPU, a coprocessor to the model's process. | | | query | The argv of `run` or `rlm`, commit-message sized. Anything longer is context. | | -| report | The first link of every chain: the processor's signed statement binding the boot's key, and for a fork the parent's chain head, to the manifest's measurement. Unsigned in trusted-host mode. Linux's TSM report. | `spec/cead.tla` | +| report | A boot's first record: the processor's signed statement binding the boot's key, and for a fork or recovery the parent boot and its last record, to the manifest's measurement. Unsigned in trusted-host mode. Linux's TSM report. | `spec/cead.tla` | +| record | One entry the machine signs for the log, Linux audit's unit. Types: report, intent, decision, witness, exit. A call's intent, decision and witness share its id, as Linux audit's records share an event. | `spec/cead.tla` | | rights | What a call may do to state: read, write. | | | ring | A privilege layer: model processes; harness and tracer; host. | | | scheduler | Decides what runs where: machines on hosts, requests on engines. Trusted for availability only; needs consensus once there is more than one. | | | slice | The bytes a child receives on stdin, sealed. | | -| snapshot | The whole machine at an instant. The fork mechanism: boot from it, with a new key. | | +| snapshot | The whole machine at an instant, taken between calls once the log holds every record so far. A boot from one is a **fork** (a new job; unlimited) or a **recovery** (the same job, after its boot is unknown; at most one per unknown boot; the operator's choice, manual by default). | | | task image | The tools one task brings: a read-only OCI image with a label declaring its tools, attached at boot. | | | tracer | eBPF in the machine's kernel, keyed by cgroup, outside the model's reach. Produces the witness. | | -| VMM | What boots a machine: Cloud Hypervisor, attested on SEV-SNP or unattested on KVM; Firecracker and Virtualization.framework, unattested. Same machine, same chain; only an attested boot's report is signed. | | +| VMM | What boots a machine: Cloud Hypervisor, attested on SEV-SNP or unattested on KVM; Firecracker and Virtualization.framework, unattested. Same machine, same records; only an attested boot's report is signed. | | | weights | The model's program text, pinned by hash in the manifest. Part of the version vector. | | | window | The context the model can address now. A cache over state. | | diff --git a/README.md b/README.md index e9edea2..5e8eed7 100644 --- a/README.md +++ b/README.md @@ -153,7 +153,7 @@ Firecracker and Virtualization.framework boot it unattested, so the harness runs The model's processes have no network. The machine reaches the host over vsock only. -The host relays inference, encrypted between the harness and the engine, and the machine's messages to the log. +The host relays inference, encrypted between the harness and the engine, and the machine's records to the log. Rules beyond that come with the first release. ### Workloads @@ -187,6 +187,6 @@ Rules beyond that come with the first release. - eBPF records what the model's processes do: which programs they start, which files they read, and each request to the engine. - Every action has a cause. The tracer is keyed by cgroup, so each action is attributed to the command that caused it, however many processes that command spawned. -- The log is one audit record per call, held outside the machine. +- The log holds the machine's records, three per call, outside the machine. The operator reads it from the CLI, live during a job and after. - Cost per call is a first-release measurement. diff --git a/spec/cead.cfg b/spec/cead.cfg index ae4aed2..3f0fe11 100644 --- a/spec/cead.cfg +++ b/spec/cead.cfg @@ -2,7 +2,7 @@ CONSTANTS Commands = {c1, c2} Policy = {c2} CallLimit = 3 - NoMsg = NoMsg + NoRecord = NoRecord SPECIFICATION Spec diff --git a/spec/cead.tla b/spec/cead.tla index 4fdaf3c..570c478 100644 --- a/spec/cead.tla +++ b/spec/cead.tla @@ -11,7 +11,7 @@ (* Attested: the processor. Trusted host: the host. *) (* Availability is the host's in both modes: it can always stop a job. *) (* Everything on the path, the host included, is a Dolev-Yao network: it *) -(* can lose, delay, replay and forge messages, but signs only as itself. *) +(* can lose, delay, replay and forge records, but signs only as itself. *) (***************************************************************************) EXTENDS Naturals, Sequences @@ -19,26 +19,26 @@ CONSTANTS Commands, \* what the model can write; the spec never sees shell text Policy, \* the commands the policy denies; {} is permit-all CallLimit, \* the limit on calls for one process - NoMsg \* a model value: no message awaiting acknowledgment + NoRecord \* a model value: no record awaiting acknowledgment ASSUME /\ Policy \subseteq Commands /\ CallLimit \in Nat Decision(c) == IF c \in Policy THEN "deny" ELSE "allow" -Parts == {"intent", "decision", "witness"} \* of one call's audit record +CallTypes == {"intent", "decision", "witness"} \* one call's records Reasons == {"finish", "timeout"} \* what an exit record can say Keys == {"machine", "path"} \* who can sign: the boot's key, the path's Signers == Keys \cup {"processor"} \* the processor signs only reports -MaxSeq == 3 * CallLimit + 2 \* the report, every part of every call, the exit +MaxSeq == 3 * CallLimit + 2 \* the report, every call's records, the exit -\* One link in the machine's chain. `seq` is its place in the chain: the +\* One record of the boot. `seq` is its place in the boot's hash chain: the \* order the machine sent it, whatever order it arrives in. The report -\* (seq 1, id 0) names the key the rest of the chain is signed with. An -\* audit record part carries its call's id and command; the exit record -\* carries id 0 and how the machine exited. -Message == [seq : 1..MaxSeq, id : 0..CallLimit, - part : Parts \cup {"report", "exit"}, +\* (seq 1, id 0) names the key the rest are signed with. A call's intent, +\* decision and witness carry its id and command; the exit record carries +\* id 0 and how the machine exited. +Record == [seq : 1..MaxSeq, id : 0..CallLimit, + type : CallTypes \cup {"report", "exit"}, body : Commands \cup Reasons \cup Keys, key : Signers] VARIABLES @@ -46,19 +46,19 @@ VARIABLES process, \* "initial", "running", "blocked", "zombie" calls, \* calls issued so far; the current call's id seq, \* the machine's last sequence number - pending, \* the message awaiting the log's acknowledgment, or NoMsg + pending, \* the record awaiting the log's acknowledgment, or NoRecord executed, \* what the kernel ran, in order: the truth - messages, \* in transit: can be lost, delayed, reordered, duplicated - log \* held outside the machine: the record, a set of links + transit, \* records in transit: can be lost, delayed, reordered, duplicated + log \* held outside the machine: a set of records -vars == <> +vars == <> -Msg(s, i, p, b) == [seq |-> s, id |-> i, part |-> p, body |-> b, key |-> "machine"] -Report == [seq |-> 1, id |-> 0, part |-> "report", body |-> "machine", key |-> "processor"] +Rec(s, i, p, b) == [seq |-> s, id |-> i, type |-> p, body |-> b, key |-> "machine"] +Report == [seq |-> 1, id |-> 0, type |-> "report", body |-> "machine", key |-> "processor"] Logged(s) == \E m \in log : m.seq = s -LoggedPart(i, p) == \E m \in log : m.id = i /\ m.part = p +LoggedType(i, p) == \E m \in log : m.id = i /\ m.type = p \* The log holds a processor-signed report naming key k. -Vouched(k) == \E r \in log : r.part = "report" /\ r.key = "processor" /\ r.body = k +Vouched(k) == \E r \in log : r.type = "report" /\ r.key = "processor" /\ r.body = k ----------------------------------------------------------------------------- (* The machine and its process *) @@ -68,19 +68,19 @@ Init == /\ process = "initial" /\ calls = 0 /\ seq = 0 - /\ pending = NoMsg + /\ pending = NoRecord /\ executed = <<>> - /\ messages = {} + /\ transit = {} /\ log = {} \* The VMM boots the machine. It makes its key and sends the report, the -\* first link of its chain, which awaits acknowledgment. +\* first record, which awaits acknowledgment. Boot == /\ machine = "off" /\ machine' = "up" /\ seq' = 1 /\ pending' = Report - /\ messages' = messages \cup {Report} + /\ transit' = transit \cup {Report} /\ UNCHANGED <> \* The log holds the report: init assembles the view, the harness starts the @@ -91,8 +91,8 @@ Start == /\ pending = Report /\ Logged(1) /\ process' = "running" - /\ pending' = NoMsg - /\ UNCHANGED <> + /\ pending' = NoRecord + /\ UNCHANGED <> \* The model issues a call. The harness blocks the process and sends the \* intent, which awaits acknowledgment. @@ -103,39 +103,39 @@ Issue(c) == /\ process' = "blocked" /\ calls' = calls + 1 /\ seq' = seq + 1 - /\ pending' = Msg(seq + 1, calls + 1, "intent", c) - /\ messages' = messages \cup {pending'} + /\ pending' = Rec(seq + 1, calls + 1, "intent", c) + /\ transit' = transit \cup {pending'} /\ UNCHANGED <> -\* The log has not acknowledged the pending message: send it again. +\* The log has not acknowledged the pending record: send it again. Resend == /\ machine \in {"up", "exiting"} - /\ pending # NoMsg + /\ pending # NoRecord /\ ~Logged(pending.seq) - /\ messages' = messages \cup {pending} + /\ transit' = transit \cup {pending} /\ UNCHANGED <> \* The log has acknowledged the intent: the harness checks the call against \* policy. Deny returns to the model. Allow runs the command, and the tracer -\* witnesses it; both parts go through the harness, which sequences them. +\* witnesses it; both records go through the harness, which sequences them. Decide == /\ machine = "up" /\ process = "blocked" - /\ pending # NoMsg - /\ pending.part = "intent" + /\ pending # NoRecord + /\ pending.type = "intent" /\ Logged(pending.seq) /\ LET c == pending.body i == pending.id IN IF Decision(c) = "allow" THEN /\ executed' = Append(executed, [id |-> i, cmd |-> c]) - /\ messages' = messages \cup - {Msg(seq + 1, i, "decision", c), Msg(seq + 2, i, "witness", c)} + /\ transit' = transit \cup + {Rec(seq + 1, i, "decision", c), Rec(seq + 2, i, "witness", c)} /\ seq' = seq + 2 ELSE /\ executed' = executed - /\ messages' = messages \cup {Msg(seq + 1, i, "decision", c)} + /\ transit' = transit \cup {Rec(seq + 1, i, "decision", c)} /\ seq' = seq + 1 /\ process' = "running" - /\ pending' = NoMsg + /\ pending' = NoRecord /\ UNCHANGED <> \* The model calls `finish`: the process is a zombie until the harness reaps it. @@ -143,16 +143,16 @@ Finish == /\ machine = "up" /\ process = "running" /\ process' = "zombie" - /\ UNCHANGED <> + /\ UNCHANGED <> -\* The machine signs its exit record, the last link in its chain, and waits +\* The machine signs its exit record, its last record, and waits \* for the log to acknowledge it. Any call in progress is cut off. Exit(reason) == /\ machine = "up" /\ machine' = "exiting" /\ seq' = seq + 1 - /\ pending' = Msg(seq + 1, 0, "exit", reason) - /\ messages' = messages \cup {pending'} + /\ pending' = Rec(seq + 1, 0, "exit", reason) + /\ transit' = transit \cup {pending'} /\ UNCHANGED <> \* The harness reaps the root process. @@ -165,8 +165,8 @@ Leave == /\ machine = "exiting" /\ Logged(pending.seq) /\ machine' = "evicted" - /\ pending' = NoMsg - /\ UNCHANGED <> + /\ pending' = NoRecord + /\ UNCHANGED <> \* The machine ends without an acknowledged exit record. A crash can happen \* at any point. The host's hard kill is the same event, but it is assumed @@ -174,34 +174,34 @@ Leave == Evict == /\ machine \in {"up", "exiting"} /\ machine' = "evicted" - /\ pending' = NoMsg - /\ UNCHANGED <> + /\ pending' = NoRecord + /\ UNCHANGED <> Crash == Evict HostKill == Evict ----------------------------------------------------------------------------- -(* Messages: outside the machine, so they go on after it is evicted *) +(* Records in transit: outside the machine, so they go on after eviction *) \* The log keeps a report only if the processor signed it, and any other -\* message only if a key it vouched for signed it. It keeps the first -\* message for each place in the chain; a duplicate or resend changes +\* record only if a key it vouched for signed it. It keeps the first +\* record for each place in the chain; a duplicate or resend changes \* nothing. First-wins matters only if KeySecret fails, so TLC never \* exercises it. Arrive(m) == - /\ IF m.part = "report" THEN m.key = "processor" ELSE Vouched(m.key) + /\ IF m.type = "report" THEN m.key = "processor" ELSE Vouched(m.key) /\ ~Logged(m.seq) /\ log' = log \cup {m} - /\ UNCHANGED <> + /\ UNCHANGED <> -Deliver(m) == m \in messages /\ Arrive(m) +Deliver(m) == m \in transit /\ Arrive(m) Lose(m) == - /\ m \in messages - /\ messages' = messages \ {m} + /\ m \in transit + /\ transit' = transit \ {m} /\ UNCHANGED <> -\* Anything on the path, the host included, can send the log a message at +\* Anything on the path, the host included, can send the log a record at \* any moment, but can sign only as itself. A forgery affects nothing until \* it reaches the log, so it is modelled as arriving there directly. Forge(m) == m.key = "path" /\ Arrive(m) @@ -220,8 +220,8 @@ Next == \/ Leave \/ Crash \/ HostKill - \/ \E m \in messages : Deliver(m) \/ Lose(m) - \/ \E m \in Message : Forge(m) + \/ \E m \in transit : Deliver(m) \/ Lose(m) + \/ \E m \in Record : Forge(m) Spec == Init /\ [][Next]_vars /\ WF_vars(HostKill) @@ -233,15 +233,15 @@ TypeOK == /\ process \in {"initial", "running", "blocked", "zombie"} /\ calls \in Nat /\ seq \in Nat - /\ pending \in Message \cup {NoMsg} + /\ pending \in Record \cup {NoRecord} /\ executed \in Seq([id : 1..CallLimit, cmd : Commands]) - /\ messages \subseteq Message - /\ log \subseteq Message + /\ transit \subseteq Record + /\ log \subseteq Record \* 1. Nothing is executed before its intent is in the log. -IntentFirst == \A k \in 1..Len(executed) : LoggedPart(executed[k].id, "intent") +IntentFirst == \A k \in 1..Len(executed) : LoggedType(executed[k].id, "intent") -\* 2. The log only gains links. +\* 2. The log only gains records. LogOnlyGrows == [][log \subseteq log']_log \* 3. Nothing whose decision is deny is executed. @@ -260,25 +260,25 @@ OnlyMachine == \A m \in log : m.key = "processor" \/ Vouched(m.key) ExecutedOnce == \A j, k \in 1..Len(executed) : j # k => executed[j].id # executed[k].id -\* 8. The machine never signs two different messages for one place in the +\* 8. The machine never signs two different records for one place in the \* chain, so the chain gives one order. Unambiguous == - LET Seen == {m \in messages : m.key # "path"} \cup + LET Seen == {m \in transit : m.key # "path"} \cup log IN \A m1, m2 \in Seen : m1.seq = m2.seq => m1 = m2 \* 9. An exit record saying `finish` means the model called `finish`: no \* call was cut off. FinishHonest == - \A m \in log : (m.part = "exit" /\ m.body = "finish") => process = "zombie" + \A m \in log : (m.type = "exit" /\ m.body = "finish") => process = "zombie" \* 10. An exit record with an unbroken chain before it proves the log -\* complete: every executed call has all three parts logged. +\* complete: every executed call has all three records logged. Complete == \A x \in log : - (x.part = "exit" /\ \A s \in 1..x.seq - 1 : Logged(s)) + (x.type = "exit" /\ \A s \in 1..x.seq - 1 : Logged(s)) => \A e \in 1..Len(executed) : - \A p \in Parts : LoggedPart(executed[e].id, p) + \A p \in CallTypes : LoggedType(executed[e].id, p) \* 11. Nothing runs on a boot until the log holds its report. ReportFirst == process # "initial" => Vouched("machine") From 376ef4b4519a8a2e19dba34d24fc6a19eb2ba938 Mon Sep 17 00:00:00 2001 From: Roone Date: Mon, 28 Sep 2026 21:19:21 -0600 Subject: [PATCH 12/15] Specify layer 2: snapshot, fork and recovery, with a recovery fencing its parent (TLC 2.19; 2 commands, 1 denied, 2 calls, 2 boots) Co-Authored-By: Claude Opus 5.5 (1M context) --- CODE.md | 2 +- spec/cead.cfg | 9 +- spec/cead.tla | 446 ++++++++++++++++++++++++++++---------------------- 3 files changed, 259 insertions(+), 198 deletions(-) diff --git a/CODE.md b/CODE.md index 224d6a5..8010663 100644 --- a/CODE.md +++ b/CODE.md @@ -73,7 +73,7 @@ Every noun has one home in code: a type, a module or crate, or a binary. A noun | ring | A privilege layer: model processes; harness and tracer; host. | | | scheduler | Decides what runs where: machines on hosts, requests on engines. Trusted for availability only; needs consensus once there is more than one. | | | slice | The bytes a child receives on stdin, sealed. | | -| snapshot | The whole machine at an instant, taken between calls once the log holds every record so far. A boot from one is a **fork** (a new job; unlimited) or a **recovery** (the same job, after its boot is unknown; at most one per unknown boot; the operator's choice, manual by default). | | +| snapshot | The whole machine at an instant, taken between calls once the log holds every record so far. A boot from one is a **fork** (a new job; unlimited) or a **recovery** (the same job, after its boot is unknown; at most one per unknown boot; the operator's choice, manual by default). A recovery **fences** its parent: the log keeps no record of the parent's after it. | | | task image | The tools one task brings: a read-only OCI image with a label declaring its tools, attached at boot. | | | tracer | eBPF in the machine's kernel, keyed by cgroup, outside the model's reach. Produces the witness. | | | VMM | What boots a machine: Cloud Hypervisor, attested on SEV-SNP or unattested on KVM; Firecracker and Virtualization.framework, unattested. Same machine, same records; only an attested boot's report is signed. | | diff --git a/spec/cead.cfg b/spec/cead.cfg index 3f0fe11..0f1f585 100644 --- a/spec/cead.cfg +++ b/spec/cead.cfg @@ -1,7 +1,9 @@ CONSTANTS Commands = {c1, c2} Policy = {c2} - CallLimit = 3 + CallLimit = 2 + Boots = {b1, b2} + Root = b1 NoRecord = NoRecord SPECIFICATION Spec @@ -10,16 +12,17 @@ INVARIANTS TypeOK IntentFirst DenyNeverRuns - WithinLimit OnlyMachine ExecutedOnce Unambiguous FinishHonest Complete ReportFirst + Rooted + OneOutcome PROPERTIES LogOnlyGrows - JobEnds + BootEnds CHECK_DEADLOCK FALSE diff --git a/spec/cead.tla b/spec/cead.tla index 570c478..71283f3 100644 --- a/spec/cead.tla +++ b/spec/cead.tla @@ -1,14 +1,18 @@ -------------------------------- MODULE cead -------------------------------- (***************************************************************************) -(* cead as a system. Layer 1: one job, one boot, one process. *) +(* cead as a system. *) +(* Layer 1: a boot, its process, its records and the log. *) +(* Layer 2: snapshot, and boots from one: fork and recovery. *) (* *) (* Assumptions, and who guarantees each. An attested boot proves them; *) (* trusted-host mode asserts them. The protocol is the same in both. *) -(* KeySecret Only the machine can sign with its key. *) -(* Attested: the processor. Trusted host: asserted. *) -(* KeyBound Only the processor can sign a report, so a report names *) -(* the key of the boot that made it. *) -(* Attested: the processor. Trusted host: the host. *) +(* KeySecret Only a boot can sign with its key. *) +(* Attested: the processor. Trusted host: asserted. *) +(* KeyBound Only the processor can sign a report, so a report *) +(* names the key of the boot that made it. *) +(* Attested: the processor. Trusted host: the host. *) +(* SnapshotSealed The host cannot alter a snapshot or read its key. *) +(* Attested: open research. Trusted host: asserted. *) (* Availability is the host's in both modes: it can always stop a job. *) (* Everything on the path, the host included, is a Dolev-Yao network: it *) (* can lose, delay, replay and forge records, but signs only as itself. *) @@ -19,268 +23,322 @@ CONSTANTS Commands, \* what the model can write; the spec never sees shell text Policy, \* the commands the policy denies; {} is permit-all CallLimit, \* the limit on calls for one process - NoRecord \* a model value: no record awaiting acknowledgment + Boots, \* model values: each boot, which is also its key + Root, \* the boot `cead run` starts + NoRecord \* a model value: no record awaiting acknowledgment ASSUME /\ Policy \subseteq Commands /\ CallLimit \in Nat + /\ Root \in Boots Decision(c) == IF c \in Policy THEN "deny" ELSE "allow" -CallTypes == {"intent", "decision", "witness"} \* one call's records -Reasons == {"finish", "timeout"} \* what an exit record can say -Keys == {"machine", "path"} \* who can sign: the boot's key, the path's -Signers == Keys \cup {"processor"} \* the processor signs only reports -MaxSeq == 3 * CallLimit + 2 \* the report, every call's records, the exit - -\* One record of the boot. `seq` is its place in the boot's hash chain: the -\* order the machine sent it, whatever order it arrives in. The report -\* (seq 1, id 0) names the key the rest are signed with. A call's intent, -\* decision and witness carry its id and command; the exit record carries -\* id 0 and how the machine exited. -Record == [seq : 1..MaxSeq, id : 0..CallLimit, - type : CallTypes \cup {"report", "exit"}, - body : Commands \cup Reasons \cup Keys, key : Signers] +CallTypes == {"intent", "decision", "witness"} \* one call's records +Reasons == {"finish", "timeout"} \* what an exit record can say +Origins == {"run", "fork", "recovery"} \* what a report says started its boot +Signers == Boots \cup {"path", "processor"} \* the processor signs only reports +MaxSeq == 3 * CallLimit + 2 \* the report, every call's records, the exit +None == "none" \* a report with no parent + +\* One record of a boot. `seq` is its place in the boot's hash chain: the +\* order the machine sent it, whatever order it arrives in. A report (seq 1, +\* id 0) names its boot, whose key signs the rest, what started it, and for +\* a fork or recovery the parent boot and the parent's last record. A call's +\* intent, decision and witness carry its id and command; the exit record +\* carries id 0 and how the machine exited. +Record == [boot : Boots, seq : 1..MaxSeq, id : 0..CallLimit, + type : CallTypes \cup {"report", "exit"}, + body : Commands \cup Reasons \cup Origins, key : Signers, + parent : Boots \cup {None}, head : 0..MaxSeq] VARIABLES - machine, \* "off", "up", "exiting", "evicted" - process, \* "initial", "running", "blocked", "zombie" - calls, \* calls issued so far; the current call's id - seq, \* the machine's last sequence number - pending, \* the record awaiting the log's acknowledgment, or NoRecord - executed, \* what the kernel ran, in order: the truth - transit, \* records in transit: can be lost, delayed, reordered, duplicated - log \* held outside the machine: a set of records - -vars == <> - -Rec(s, i, p, b) == [seq |-> s, id |-> i, type |-> p, body |-> b, key |-> "machine"] -Report == [seq |-> 1, id |-> 0, type |-> "report", body |-> "machine", key |-> "processor"] -Logged(s) == \E m \in log : m.seq = s -LoggedType(i, p) == \E m \in log : m.id = i /\ m.type = p -\* The log holds a processor-signed report naming key k. -Vouched(k) == \E r \in log : r.type = "report" /\ r.key = "processor" /\ r.body = k + machine, \* per boot: "off", "up", "exiting", "evicted" + process, \* per boot, its root process: "initial", "running", "blocked", "zombie" + calls, \* per boot: calls issued so far; the current call's id + seq, \* per boot: the machine's last sequence number + pending, \* per boot: the record awaiting the log's acknowledgment, or NoRecord + executed, \* per boot: what the kernel ran, in order: the truth + job, \* per boot: the boot that started its job + snapshots, \* every snapshot taken: a boot, its last record, its calls + transit, \* every record sent: each can be lost, delayed, reordered, duplicated + log \* held outside the machine: a set of records + +vars == <> +boot == <> + +Rec(b, s, i, t, x) == [boot |-> b, seq |-> s, id |-> i, type |-> t, body |-> x, + key |-> b, parent |-> None, head |-> 0] +Report(b, o, p, h) == [boot |-> b, seq |-> 1, id |-> 0, type |-> "report", body |-> o, + key |-> "processor", parent |-> p, head |-> h] +Logged(b, s) == \E r \in log : r.boot = b /\ r.seq = s +LoggedType(b, i, t) == \E r \in log : r.boot = b /\ r.id = i /\ r.type = t +\* The log holds boot b's report: b's key is vouched for. +Vouched(b) == Logged(b, 1) +\* The log holds a report recovering boot b. +Recovered(b) == \E r \in log : r.type = "report" /\ r.body = "recovery" /\ r.parent = b +\* Boot b is evicted without its exit record in the log. +Unknown(b) == machine[b] = "evicted" /\ ~\E r \in log : r.boot = b /\ r.type = "exit" ----------------------------------------------------------------------------- -(* The machine and its process *) +(* A boot and its process *) Init == - /\ machine = "off" - /\ process = "initial" - /\ calls = 0 - /\ seq = 0 - /\ pending = NoRecord - /\ executed = <<>> - /\ transit = {} - /\ log = {} - -\* The VMM boots the machine. It makes its key and sends the report, the -\* first record, which awaits acknowledgment. -Boot == - /\ machine = "off" - /\ machine' = "up" - /\ seq' = 1 - /\ pending' = Report - /\ transit' = transit \cup {Report} - /\ UNCHANGED <> + /\ machine = [b \in Boots |-> "off"] + /\ process = [b \in Boots |-> "initial"] + /\ calls = [b \in Boots |-> 0] + /\ seq = [b \in Boots |-> 0] + /\ pending = [b \in Boots |-> NoRecord] + /\ executed = [b \in Boots |-> <<>>] + /\ job = [b \in Boots |-> b] + /\ snapshots = {} + /\ transit = {} + /\ log = {} + +\* The VMM starts boot b: it makes its key and sends its report, which +\* awaits acknowledgment. `c` is the calls its process has already issued. +Begin(b, r, c, j) == + /\ machine' = [machine EXCEPT ![b] = "up"] + /\ seq' = [seq EXCEPT ![b] = 1] + /\ calls' = [calls EXCEPT ![b] = c] + /\ pending' = [pending EXCEPT ![b] = r] + /\ job' = [job EXCEPT ![b] = j] + /\ transit' = transit \cup {r} + /\ UNCHANGED <> + +\* `cead run` boots the root. +Boot == machine[Root] = "off" /\ Begin(Root, Report(Root, "run", None, 0), 0, Root) + +\* A boot from a snapshot. A fork starts a new job, whenever anyone asks; +\* a recovery continues the snapshot's job, once its boot is unknown. +BootFrom(b, s, o) == + /\ b # Root + /\ machine[b] = "off" + /\ o = "recovery" => Unknown(s.boot) + /\ Begin(b, Report(b, o, s.boot, s.head), s.calls, + IF o = "fork" THEN b ELSE job[s.boot]) \* The log holds the report: init assembles the view, the harness starts the \* root process. Nothing runs on a boot the log has not heard of. -Start == - /\ machine = "up" - /\ process = "initial" - /\ pending = Report - /\ Logged(1) - /\ process' = "running" - /\ pending' = NoRecord - /\ UNCHANGED <> +Start(b) == + /\ machine[b] = "up" + /\ process[b] = "initial" + /\ pending[b] # NoRecord + /\ pending[b].type = "report" + /\ Logged(b, 1) + /\ process' = [process EXCEPT ![b] = "running"] + /\ pending' = [pending EXCEPT ![b] = NoRecord] + /\ UNCHANGED <> \* The model issues a call. The harness blocks the process and sends the \* intent, which awaits acknowledgment. -Issue(c) == - /\ machine = "up" - /\ process = "running" - /\ calls < CallLimit - /\ process' = "blocked" - /\ calls' = calls + 1 - /\ seq' = seq + 1 - /\ pending' = Rec(seq + 1, calls + 1, "intent", c) - /\ transit' = transit \cup {pending'} - /\ UNCHANGED <> - -\* The log has not acknowledged the pending record: send it again. -Resend == - /\ machine \in {"up", "exiting"} - /\ pending # NoRecord - /\ ~Logged(pending.seq) - /\ transit' = transit \cup {pending} - /\ UNCHANGED <> +Issue(b, c) == + /\ machine[b] = "up" + /\ process[b] = "running" + /\ calls[b] < CallLimit + /\ LET r == Rec(b, seq[b] + 1, calls[b] + 1, "intent", c) + IN /\ process' = [process EXCEPT ![b] = "blocked"] + /\ calls' = [calls EXCEPT ![b] = calls[b] + 1] + /\ seq' = [seq EXCEPT ![b] = seq[b] + 1] + /\ pending' = [pending EXCEPT ![b] = r] + /\ transit' = transit \cup {r} + /\ UNCHANGED <> \* The log has acknowledged the intent: the harness checks the call against \* policy. Deny returns to the model. Allow runs the command, and the tracer \* witnesses it; both records go through the harness, which sequences them. -Decide == - /\ machine = "up" - /\ process = "blocked" - /\ pending # NoRecord - /\ pending.type = "intent" - /\ Logged(pending.seq) - /\ LET c == pending.body - i == pending.id +Decide(b) == + /\ machine[b] = "up" + /\ process[b] = "blocked" + /\ pending[b] # NoRecord + /\ pending[b].type = "intent" + /\ Logged(b, pending[b].seq) + /\ LET c == pending[b].body + i == pending[b].id + s == seq[b] IN IF Decision(c) = "allow" - THEN /\ executed' = Append(executed, [id |-> i, cmd |-> c]) + THEN /\ executed' = [executed EXCEPT ![b] = Append(@, [id |-> i, cmd |-> c])] /\ transit' = transit \cup - {Rec(seq + 1, i, "decision", c), Rec(seq + 2, i, "witness", c)} - /\ seq' = seq + 2 + {Rec(b, s + 1, i, "decision", c), Rec(b, s + 2, i, "witness", c)} + /\ seq' = [seq EXCEPT ![b] = s + 2] ELSE /\ executed' = executed - /\ transit' = transit \cup {Rec(seq + 1, i, "decision", c)} - /\ seq' = seq + 1 - /\ process' = "running" - /\ pending' = NoRecord - /\ UNCHANGED <> + /\ transit' = transit \cup {Rec(b, s + 1, i, "decision", c)} + /\ seq' = [seq EXCEPT ![b] = s + 1] + /\ process' = [process EXCEPT ![b] = "running"] + /\ pending' = [pending EXCEPT ![b] = NoRecord] + /\ UNCHANGED <> + +\* The whole machine at an instant, between calls, once the log holds every +\* record so far. +Snapshot(b) == + /\ machine[b] = "up" + /\ process[b] = "running" + /\ \A s \in 1..seq[b] : Logged(b, s) + /\ snapshots' = snapshots \cup {[boot |-> b, head |-> seq[b], calls |-> calls[b]]} + /\ UNCHANGED <> \* The model calls `finish`: the process is a zombie until the harness reaps it. -Finish == - /\ machine = "up" - /\ process = "running" - /\ process' = "zombie" - /\ UNCHANGED <> - -\* The machine signs its exit record, its last record, and waits -\* for the log to acknowledge it. Any call in progress is cut off. -Exit(reason) == - /\ machine = "up" - /\ machine' = "exiting" - /\ seq' = seq + 1 - /\ pending' = Rec(seq + 1, 0, "exit", reason) - /\ transit' = transit \cup {pending'} - /\ UNCHANGED <> +Finish(b) == + /\ machine[b] = "up" + /\ process[b] = "running" + /\ process' = [process EXCEPT ![b] = "zombie"] + /\ UNCHANGED <> + +\* The machine signs its exit record, its last record, and waits for the log +\* to acknowledge it. Any call in progress is cut off. +Exit(b, reason) == + /\ machine[b] = "up" + /\ LET r == Rec(b, seq[b] + 1, 0, "exit", reason) + IN /\ machine' = [machine EXCEPT ![b] = "exiting"] + /\ seq' = [seq EXCEPT ![b] = seq[b] + 1] + /\ pending' = [pending EXCEPT ![b] = r] + /\ transit' = transit \cup {r} + /\ UNCHANGED <> \* The harness reaps the root process. -Reap == process = "zombie" /\ Exit("finish") +Reap(b) == process[b] = "zombie" /\ Exit(b, "finish") \* The machine's own wall-time limit fires. -Timeout == Exit("timeout") +Timeout(b) == Exit(b, "timeout") \* The log has the exit record: the machine is gone. -Leave == - /\ machine = "exiting" - /\ Logged(pending.seq) - /\ machine' = "evicted" - /\ pending' = NoRecord - /\ UNCHANGED <> +Leave(b) == + /\ machine[b] = "exiting" + /\ Logged(b, pending[b].seq) + /\ machine' = [machine EXCEPT ![b] = "evicted"] + /\ pending' = [pending EXCEPT ![b] = NoRecord] + /\ UNCHANGED <> \* The machine ends without an acknowledged exit record. A crash can happen \* at any point. The host's hard kill is the same event, but it is assumed \* to happen (see Spec): it is what makes every job end. -Evict == - /\ machine \in {"up", "exiting"} - /\ machine' = "evicted" - /\ pending' = NoRecord - /\ UNCHANGED <> +Evict(b) == + /\ machine[b] \in {"up", "exiting"} + /\ machine' = [machine EXCEPT ![b] = "evicted"] + /\ pending' = [pending EXCEPT ![b] = NoRecord] + /\ UNCHANGED <> -Crash == Evict -HostKill == Evict +Crash(b) == Evict(b) +HostKill(b) == Evict(b) ----------------------------------------------------------------------------- (* Records in transit: outside the machine, so they go on after eviction *) - -\* The log keeps a report only if the processor signed it, and any other -\* record only if a key it vouched for signed it. It keeps the first -\* record for each place in the chain; a duplicate or resend changes -\* nothing. First-wins matters only if KeySecret fails, so TLC never -\* exercises it. -Arrive(m) == - /\ IF m.type = "report" THEN m.key = "processor" ELSE Vouched(m.key) - /\ ~Logged(m.seq) - /\ log' = log \cup {m} - /\ UNCHANGED <> - -Deliver(m) == m \in transit /\ Arrive(m) - -Lose(m) == - /\ m \in transit - /\ transit' = transit \ {m} - /\ UNCHANGED <> - -\* Anything on the path, the host included, can send the log a record at -\* any moment, but can sign only as itself. A forgery affects nothing until -\* it reaches the log, so it is modelled as arriving there directly. -Forge(m) == m.key = "path" /\ Arrive(m) +(* A record once sent stays in transit: one never delivered is lost, one *) +(* delivered twice is duplicated, and the machine's resends add nothing. *) + +\* The log keeps a report only if the processor signed it; a recovery only +\* while its parent is not complete, and only the first for that parent. +\* It keeps any other record only if its boot's key signed it, the log holds +\* that boot's report, and no recovery has taken the boot's place. It keeps +\* the first record for each place in a boot's hash chain; a duplicate or +\* resend changes nothing. First-wins matters only if KeySecret fails, so +\* TLC never exercises it. +Arrive(r) == + /\ IF r.type = "report" + THEN /\ r.key = "processor" + /\ r.body = "recovery" => + /\ ~LoggedType(r.parent, 0, "exit") + /\ ~Recovered(r.parent) + ELSE /\ r.key = r.boot + /\ Vouched(r.boot) + /\ ~Recovered(r.boot) + /\ ~Logged(r.boot, r.seq) + /\ log' = log \cup {r} + /\ UNCHANGED <> + +Deliver(r) == r \in transit /\ Arrive(r) + +\* Anything on the path, the host included, can send the log any record at +\* any moment, but can sign only as itself: it can copy a record it has +\* seen and sign the copy. A forgery affects nothing until it reaches the +\* log, so it is modelled as arriving there directly. +Forge(r) == Arrive([r EXCEPT !.key = "path"]) ----------------------------------------------------------------------------- Next == \/ Boot - \/ Start - \/ \E c \in Commands : Issue(c) - \/ Resend - \/ Decide - \/ Finish - \/ Reap - \/ Timeout - \/ Leave - \/ Crash - \/ HostKill - \/ \E m \in transit : Deliver(m) \/ Lose(m) - \/ \E m \in Record : Forge(m) - -Spec == Init /\ [][Next]_vars /\ WF_vars(HostKill) + \/ \E b \in Boots, s \in snapshots, o \in {"fork", "recovery"} : BootFrom(b, s, o) + \/ \E b \in Boots : + \/ Start(b) \/ Decide(b) \/ Snapshot(b) \/ Finish(b) + \/ Reap(b) \/ Timeout(b) \/ Leave(b) \/ Crash(b) \/ HostKill(b) + \/ \E c \in Commands : Issue(b, c) + \/ \E r \in transit : Deliver(r) \/ Forge(r) + +Spec == Init /\ [][Next]_vars /\ \A b \in Boots : WF_vars(HostKill(b)) ----------------------------------------------------------------------------- (* Properties *) TypeOK == - /\ machine \in {"off", "up", "exiting", "evicted"} - /\ process \in {"initial", "running", "blocked", "zombie"} - /\ calls \in Nat - /\ seq \in Nat - /\ pending \in Record \cup {NoRecord} - /\ executed \in Seq([id : 1..CallLimit, cmd : Commands]) + /\ machine \in [Boots -> {"off", "up", "exiting", "evicted"}] + /\ process \in [Boots -> {"initial", "running", "blocked", "zombie"}] + /\ calls \in [Boots -> 0..CallLimit] + /\ seq \in [Boots -> 0..MaxSeq] + /\ pending \in [Boots -> Record \cup {NoRecord}] + /\ \A b \in Boots : executed[b] \in Seq([id : 1..CallLimit, cmd : Commands]) + /\ job \in [Boots -> Boots] /\ transit \subseteq Record /\ log \subseteq Record \* 1. Nothing is executed before its intent is in the log. -IntentFirst == \A k \in 1..Len(executed) : LoggedType(executed[k].id, "intent") +IntentFirst == + \A b \in Boots : \A k \in 1..Len(executed[b]) : + LoggedType(b, executed[b][k].id, "intent") \* 2. The log only gains records. LogOnlyGrows == [][log \subseteq log']_log \* 3. Nothing whose decision is deny is executed. -DenyNeverRuns == \A k \in 1..Len(executed) : Decision(executed[k].cmd) = "allow" +DenyNeverRuns == + \A b \in Boots : \A k \in 1..Len(executed[b]) : + Decision(executed[b][k].cmd) = "allow" -\* 4. A process makes at most CallLimit calls. -WithinLimit == calls <= CallLimit +\* 4. A process makes at most CallLimit calls: TypeOK bounds `calls`. -\* 5. Every job that starts ends, and its machine is evicted. -JobEnds == (machine = "up") ~> (machine = "evicted") +\* 5. Every boot that starts ends, and its machine is evicted. +BootEnds == \A b \in Boots : (machine[b] = "up") ~> (machine[b] = "evicted") -\* 6. The log holds only what the processor signed, or a key it vouched for. -OnlyMachine == \A m \in log : m.key = "processor" \/ Vouched(m.key) +\* 6. The log holds only what the processor signed, or a boot's own key. +OnlyMachine == \A r \in log : r.key = "processor" \/ (r.key = r.boot /\ Vouched(r.boot)) -\* 7. Each call is executed at most once. +\* 7. Each call is executed at most once on a boot. ExecutedOnce == - \A j, k \in 1..Len(executed) : j # k => executed[j].id # executed[k].id + \A b \in Boots : \A j, k \in 1..Len(executed[b]) : + j # k => executed[b][j].id # executed[b][k].id -\* 8. The machine never signs two different records for one place in the -\* chain, so the chain gives one order. +\* 8. No boot signs two different records for one place in its hash chain, +\* so each chain gives one order. Unambiguous == - LET Seen == {m \in transit : m.key # "path"} \cup - log - IN \A m1, m2 \in Seen : m1.seq = m2.seq => m1 = m2 + LET Seen == {r \in transit : r.key # "path"} \cup log + IN \A r1, r2 \in Seen : (r1.boot = r2.boot /\ r1.seq = r2.seq) => r1 = r2 \* 9. An exit record saying `finish` means the model called `finish`: no \* call was cut off. FinishHonest == - \A m \in log : (m.type = "exit" /\ m.body = "finish") => process = "zombie" + \A r \in log : (r.type = "exit" /\ r.body = "finish") => process[r.boot] = "zombie" -\* 10. An exit record with an unbroken chain before it proves the log -\* complete: every executed call has all three records logged. +\* 10. A boot is complete when the log holds its exit record with no gap +\* before it: then every call it executed has all three records logged. Complete == \A x \in log : - (x.type = "exit" /\ \A s \in 1..x.seq - 1 : Logged(s)) - => \A e \in 1..Len(executed) : - \A p \in CallTypes : LoggedType(executed[e].id, p) + (x.type = "exit" /\ \A s \in 1..x.seq - 1 : Logged(x.boot, s)) + => \A e \in 1..Len(executed[x.boot]) : + \A t \in CallTypes : LoggedType(x.boot, executed[x.boot][e].id, t) \* 11. Nothing runs on a boot until the log holds its report. -ReportFirst == process # "initial" => Vouched("machine") +ReportFirst == \A b \in Boots : process[b] # "initial" => Vouched(b) + +\* 12. A fork or recovery names a record the log holds: its parent's last +\* record when the snapshot was taken. +Rooted == + \A r \in log : (r.type = "report" /\ r.parent # None) => Logged(r.parent, r.head) + +\* 13. A job has one outcome: a recovered boot is never complete, and no two +\* boots of one job run at once. +OneOutcome == + /\ \A r \in log : (r.type = "report" /\ r.body = "recovery") => + ~LoggedType(r.parent, 0, "exit") + /\ \A x, y \in Boots : + (x # y /\ job[x] = job[y] /\ Vouched(x) /\ Vouched(y)) => + ~(machine[x] = "up" /\ machine[y] = "up") ============================================================================= From 7225157fadb086ca06d61f2e6033bb27567554b0 Mon Sep 17 00:00:00 2001 From: Roone Date: Mon, 28 Sep 2026 22:28:13 -0600 Subject: [PATCH 13/15] Keep one level per term: agent spawns processes, fork copies machines; a turn without a command ends a process Co-Authored-By: Claude Opus 5.5 (1M context) --- CODE.md | 22 +++++++++++----------- README.md | 16 ++++++++++------ spec/cead.tla | 35 +++++++++++++++++++---------------- 3 files changed, 40 insertions(+), 33 deletions(-) diff --git a/CODE.md b/CODE.md index 8010663..2884e9f 100644 --- a/CODE.md +++ b/CODE.md @@ -23,7 +23,7 @@ Spec, skeleton, fill. TLA+, Lean and Rust are one pipeline, not alternatives: TL ## Boundaries - Which side of which interface is new code on: model-facing, machine tool, harness, tracer, host? What is its source of stability: written spec, ABI promise, pinned version, none? Below the ABI, what re-validates it when the pinned kernel changes? -- The model's side is untyped and GNU-flavoured. Types live between the shell and the kernel, never in the shell. Widening the model-facing surface is GNU-flavoured POSIX or a third call in disguise. +- The model's side is untyped and GNU-flavoured. Types live between the shell and the kernel, never in the shell. Widening the model-facing surface is GNU-flavoured POSIX or a second call in disguise. - The call table is the single source: builtins, exec policy, prompt lines and man text render from it, never a second list. New capability arrives as state or a well-known CLI. - A dependency's types stay inside the boundary module that wraps it. The skeleton names our nouns; swapping a dependency is a module change. @@ -37,7 +37,7 @@ Every noun has one home in code: a type, a module or crate, or a binary. A noun | availability | The job runs and ends. The host guarantees it, and can always deny it. | `spec/cead.tla` | | boot | One life of a machine's kernel, from the VMM starting it to eviction, with one key. Its records form one hash chain signed with that key, its report first. **Complete** when the log holds its records through its exit record with no gap; otherwise **unknown** (crash, host kill, lost report). Linux's `boot_id`. | `spec/cead.tla` | | bounded | Output admitted to the window, constructible only by truncation. The remainder **spills** to a file. | | -| call | One command the model issues and what it gets back: a system call into the harness. Untyped argv and stdin in, text and exit code out. The unit of limits and measurement. cead adds `rlm` and `finish`; every other call is a well-known CLI. | | +| call | One command the model issues and what it gets back: a system call into the harness. Untyped argv and stdin in, text and exit code out. The unit of limits and measurement. cead adds `agent`; every other call is a well-known CLI. | | | call table | The system call table: the toolset. | | | cead | The project and the operator's binary. | crate and binary `cead` | | command | What the model writes: shell over the core plus the task image. | | @@ -45,7 +45,7 @@ Every noun has one home in code: a type, a module or crate, or a binary. A noun | console | The operator's interface to manifests, machines and their state: `cead` with no verb. Its verbs drive the scheduler. | | | core | The invariant tools every machine has: brush, uutils, grep, git, sqlite3. nix-built, static, first on PATH. | | | decision | The outcome of checking a call against policy: allow or deny. | | -| descriptor | State the model holds this session, bound to an object with rights. Minted by cead, never discovered; a capability. A child's is **attenuated**. | | +| descriptor | State the model holds this session, bound to an object with rights. Minted by cead, never discovered; a capability. A child process's is **attenuated** when it is spawned, and never grows; revoking it is `kill`. | | | engine | Executes the weights and signs what it produces: the model's counterpart to the machine. vLLM by default. | | | evict | Dispose at any tier: window span, KV block, process, machine. | | | executed | What the kernel ran: the truth the records record. | `spec/cead.tla` | @@ -55,25 +55,25 @@ Every noun has one home in code: a type, a module or crate, or a binary. A noun | integrity | The log says only what the machine signed, in the machine's order. Guaranteed by each boot's signature and hash chain, rooted in its report. | `spec/cead.tla` | | interface | One of the three lines everything else is swappable between. | | | job | One query's work: a root process and its tree. Started by `cead run`. Spans one boot, or more through recovery. | | -| limit | A cap on one process: window size, bound, calls, wall time. The rlimit analogue: set in the fork-exec gap, inherited as a copy. | | +| limit | A cap on one process: window size, bound, calls, wall time, depth. The rlimit analogue: set in the fork-exec gap, inherited as a copy. | | | log | Every boot's records, held outside the machine. Records in transit can be lost, delayed, replayed or forged; the log keeps only what the processor or a boot's key signed. A complete boot's records are all it did; an unknown boot's are true but may be partial. A job's boots link through their reports. One writer per boot: never consensus. | `spec/cead.tla` | | machine | The unit: pinned kernel, core, task image, descriptors, call table, policy and model, booted in a microVM by a VMM. | | | manifest | The one file that pins a machine by content. Equal manifests are the same experiment; its hashes are the version vector. | | -| meter | What a process tree may spend, from KeyKOS. A child's meter hangs below its parent's; every spend is charged to each meter above it, so a tree never outspends its root. A parent can cap or revoke a child's meter. What it counts is manifest policy. | | +| meter | What a process tree may spend, from KeyKOS. A child process's meter hangs below its parent's; every spend is charged to each meter above it, so a tree never outspends its root. A parent caps a child's meter in `agent`'s argv and revokes it with `kill`. What it counts is manifest policy. | | | model | The machine's user: weights running on an engine, reached by the harness over TLS that every host between only relays. The machine holds only a job-scoped token, never a long-lived key. | | | operator | The human at depth 0. Types `cead` or `cead run`; never types a call. | | | pinned | The part of the window eviction never touches: the system prompt. | | | policy | The rows of the call table in Cedar, compiled to seccomp and Landlock, installed before exec. Permit-all is a declared policy, not an absence. | | -| process | An OS process running one harness cycle, with its own cgroup, window, shell, limits and meter; each call runs as its child. Running, ready, blocked or zombie. Started by `run` at depth 0, `rlm` below. | | -| processor | What a process runs on. For the machine, the CPU; for the model, the GPU, a coprocessor to the model's process. | | -| query | The argv of `run` or `rlm`, commit-message sized. Anything longer is context. | | -| report | A boot's first record: the processor's signed statement binding the boot's key, and for a fork or recovery the parent boot and its last record, to the manifest's measurement. Unsigned in trusted-host mode. Linux's TSM report. | `spec/cead.tla` | +| process | An OS process running one harness cycle, with its own cgroup, window, shell, limits and meter; each call runs as its child. Running, ready, blocked or zombie. Started by `run` at depth 0, `agent` below. It ends when the model replies without a command; its reply is its stdout. Each `agent` child is spawned in its own PID namespace, so `kill` reaches only its descendants. | | +| processor | What a process runs on. For the machine, the CPU; for the model, the GPU, a coprocessor to the model's process. A boot sees the model's processors as virtual, like vCPUs; how the engine shares its GPU among them (batching) is its scheduler's. | | +| query | The argv of `run` or `agent`, commit-message sized. Anything longer is context. | | +| report | A boot's first record: the processor's signed statement binding the boot's key, and for a fork or recovery the snapshot it booted from (that boot and its last record), to the manifest's measurement. Unsigned in trusted-host mode. Linux's TSM report. | `spec/cead.tla` | | record | One entry the machine signs for the log, Linux audit's unit. Types: report, intent, decision, witness, exit. A call's intent, decision and witness share its id, as Linux audit's records share an event. | `spec/cead.tla` | | rights | What a call may do to state: read, write. | | | ring | A privilege layer: model processes; harness and tracer; host. | | -| scheduler | Decides what runs where: machines on hosts, requests on engines. Trusted for availability only; needs consensus once there is more than one. | | +| scheduler | Decides what runs where: machines on hosts (Kubernetes), requests on engines (Dynamo). Trusted for availability only; needs consensus once there is more than one. | | | slice | The bytes a child receives on stdin, sealed. | | -| snapshot | The whole machine at an instant, taken between calls once the log holds every record so far. A boot from one is a **fork** (a new job; unlimited) or a **recovery** (the same job, after its boot is unknown; at most one per unknown boot; the operator's choice, manual by default). A recovery **fences** its parent: the log keeps no record of the parent's after it. | | +| snapshot | The whole machine at an instant, taken between calls once the log holds every record so far. A boot from one is a **fork** (a new job; unlimited) or a **recovery** (the same job, after its boot is unknown; at most one per unknown boot; the operator's choice, manual by default). A recovery **fences** the boot it recovers: the log keeps none of that boot's records after it. | | | task image | The tools one task brings: a read-only OCI image with a label declaring its tools, attached at boot. | | | tracer | eBPF in the machine's kernel, keyed by cgroup, outside the model's reach. Produces the witness. | | | VMM | What boots a machine: Cloud Hypervisor, attested on SEV-SNP or unattested on KVM; Firecracker and Virtualization.framework, unattested. Same machine, same records; only an attested boot's report is signed. | | diff --git a/README.md b/README.md index 5e8eed7..920fc27 100644 --- a/README.md +++ b/README.md @@ -44,6 +44,7 @@ System diagram to come with the first release. - [Recursive Language Models](https://arxiv.org/abs/2512.24601) (Zhang, Kraska, Khattab) - [Language model harnesses are compositional generalizers](https://alexzhang13.github.io/blog/2026/harness/) (Zhang, Khattab) - [OSTEP](https://pages.cs.wisc.edu/~remzi/OSTEP/) (Arpaci-Dusseau) +- [The Datacenter as a Computer](https://link.springer.com/book/10.1007/978-3-031-01761-2) (Barroso, Hölzle, Ranganathan) - [Capability Myths Demolished](https://srl.cs.jhu.edu/pubs/SRL2003-02.pdf) (Miller, Yee, Shapiro) - [Robust Composition](http://www.erights.org/talks/thesis/) (Miller) - [Prime Agent](https://www.primeintellect.ai/blog/prime-agent) ([source](https://github.com/PrimeIntellect-ai/prime-agent)) and [Sandboxes](https://www.primeintellect.ai/blog/sandboxes) (Prime Intellect) @@ -120,7 +121,7 @@ Work fans out three ways, told apart by who spawns and when: |---|---|---|---| | evals | operator | before the job | scale-out: N machines from one manifest | | reinforcement learning | operator or trainer | mid-job, at a chosen state | fork: K machines from one snapshot, the way a git worktree forks a checkout | -| long or autonomous tasks | the model | whenever it decides | `rlm`: a sub-agent process inside the machine | +| long or autonomous tasks | the model | whenever it decides | `agent`: a sub-agent process inside the machine | - Kubernetes can schedule machines as pods; Firecracker was built for this shape of workload. - The long-term direction is one box: model, inference engine, kernel and cead. @@ -163,13 +164,16 @@ Rules beyond that come with the first release. - Each call. The harness assembles the context window from the system prompt, the query and the bounded output of every command so far, and sends it to the engine. It runs the command that comes back and adds the output, cut at a size cap, to the window; the full output goes to a file the model can read piecewise. -- Recursion, inside the machine. - `rlm` starts a child process with a slice of the parent's context, a meter under its parent's, the same tools, and its own context window. - It is a sub-agent, built from process structure rather than at the application layer. +- Sub-agents, called programmatically. + `agent` starts a child process with a slice of the parent's context on stdin, a meter under its parent's, the same tools, and its own context window. + It is a command, so the shell composes it: loops, pipes, `&`, `wait`, `kill`. + A child's answer lands in a file or a shell variable and enters a window only when read. - Forking, of the machine. A snapshot of a running machine boots another machine that diverges from the same state. -- Finish. - `finish` ends a process with its answer; when the root process finishes, the job is over and the machine is gone. +- Ending. + A process ends when the model replies without a command; the reply is its answer on stdout. + Ending kills its running sub-agents, so `wait` first to keep them. + When the root process ends, the job is over and the machine is gone. ### Data diff --git a/spec/cead.tla b/spec/cead.tla index 71283f3..28ab2d1 100644 --- a/spec/cead.tla +++ b/spec/cead.tla @@ -38,18 +38,19 @@ Reasons == {"finish", "timeout"} \* what an exit record can say Origins == {"run", "fork", "recovery"} \* what a report says started its boot Signers == Boots \cup {"path", "processor"} \* the processor signs only reports MaxSeq == 3 * CallLimit + 2 \* the report, every call's records, the exit -None == "none" \* a report with no parent +None == "none" \* a report not booted from a snapshot \* One record of a boot. `seq` is its place in the boot's hash chain: the \* order the machine sent it, whatever order it arrives in. A report (seq 1, \* id 0) names its boot, whose key signs the rest, what started it, and for -\* a fork or recovery the parent boot and the parent's last record. A call's +\* a fork or recovery the snapshot it booted from: that boot and its last +\* record. A call's \* intent, decision and witness carry its id and command; the exit record \* carries id 0 and how the machine exited. Record == [boot : Boots, seq : 1..MaxSeq, id : 0..CallLimit, type : CallTypes \cup {"report", "exit"}, body : Commands \cup Reasons \cup Origins, key : Signers, - parent : Boots \cup {None}, head : 0..MaxSeq] + from : Boots \cup {None}, last : 0..MaxSeq] VARIABLES machine, \* per boot: "off", "up", "exiting", "evicted" @@ -67,15 +68,15 @@ vars == <> Rec(b, s, i, t, x) == [boot |-> b, seq |-> s, id |-> i, type |-> t, body |-> x, - key |-> b, parent |-> None, head |-> 0] + key |-> b, from |-> None, last |-> 0] Report(b, o, p, h) == [boot |-> b, seq |-> 1, id |-> 0, type |-> "report", body |-> o, - key |-> "processor", parent |-> p, head |-> h] + key |-> "processor", from |-> p, last |-> h] Logged(b, s) == \E r \in log : r.boot = b /\ r.seq = s LoggedType(b, i, t) == \E r \in log : r.boot = b /\ r.id = i /\ r.type = t \* The log holds boot b's report: b's key is vouched for. Vouched(b) == Logged(b, 1) \* The log holds a report recovering boot b. -Recovered(b) == \E r \in log : r.type = "report" /\ r.body = "recovery" /\ r.parent = b +Recovered(b) == \E r \in log : r.type = "report" /\ r.body = "recovery" /\ r.from = b \* Boot b is evicted without its exit record in the log. Unknown(b) == machine[b] = "evicted" /\ ~\E r \in log : r.boot = b /\ r.type = "exit" @@ -114,7 +115,7 @@ BootFrom(b, s, o) == /\ b # Root /\ machine[b] = "off" /\ o = "recovery" => Unknown(s.boot) - /\ Begin(b, Report(b, o, s.boot, s.head), s.calls, + /\ Begin(b, Report(b, o, s.boot, s.last), s.calls, IF o = "fork" THEN b ELSE job[s.boot]) \* The log holds the report: init assembles the view, the harness starts the @@ -173,10 +174,11 @@ Snapshot(b) == /\ machine[b] = "up" /\ process[b] = "running" /\ \A s \in 1..seq[b] : Logged(b, s) - /\ snapshots' = snapshots \cup {[boot |-> b, head |-> seq[b], calls |-> calls[b]]} + /\ snapshots' = snapshots \cup {[boot |-> b, last |-> seq[b], calls |-> calls[b]]} /\ UNCHANGED <> -\* The model calls `finish`: the process is a zombie until the harness reaps it. +\* The model replies without a command: the process is a zombie until the +\* harness reaps it. The exit record calls this `finish`. Finish(b) == /\ machine[b] = "up" /\ process[b] = "running" @@ -225,7 +227,8 @@ HostKill(b) == Evict(b) (* delivered twice is duplicated, and the machine's resends add nothing. *) \* The log keeps a report only if the processor signed it; a recovery only -\* while its parent is not complete, and only the first for that parent. +\* while the boot it recovers is not complete, and only the first for that +\* boot. \* It keeps any other record only if its boot's key signed it, the log holds \* that boot's report, and no recovery has taken the boot's place. It keeps \* the first record for each place in a boot's hash chain; a duplicate or @@ -235,8 +238,8 @@ Arrive(r) == /\ IF r.type = "report" THEN /\ r.key = "processor" /\ r.body = "recovery" => - /\ ~LoggedType(r.parent, 0, "exit") - /\ ~Recovered(r.parent) + /\ ~LoggedType(r.from, 0, "exit") + /\ ~Recovered(r.from) ELSE /\ r.key = r.boot /\ Vouched(r.boot) /\ ~Recovered(r.boot) @@ -311,7 +314,7 @@ Unambiguous == LET Seen == {r \in transit : r.key # "path"} \cup log IN \A r1, r2 \in Seen : (r1.boot = r2.boot /\ r1.seq = r2.seq) => r1 = r2 -\* 9. An exit record saying `finish` means the model called `finish`: no +\* 9. An exit record saying `finish` means the model ended its turn: no \* call was cut off. FinishHonest == \A r \in log : (r.type = "exit" /\ r.body = "finish") => process[r.boot] = "zombie" @@ -327,16 +330,16 @@ Complete == \* 11. Nothing runs on a boot until the log holds its report. ReportFirst == \A b \in Boots : process[b] # "initial" => Vouched(b) -\* 12. A fork or recovery names a record the log holds: its parent's last +\* 12. A fork or recovery names a record the log holds: its snapshot's last \* record when the snapshot was taken. Rooted == - \A r \in log : (r.type = "report" /\ r.parent # None) => Logged(r.parent, r.head) + \A r \in log : (r.type = "report" /\ r.from # None) => Logged(r.from, r.last) \* 13. A job has one outcome: a recovered boot is never complete, and no two \* boots of one job run at once. OneOutcome == /\ \A r \in log : (r.type = "report" /\ r.body = "recovery") => - ~LoggedType(r.parent, 0, "exit") + ~LoggedType(r.from, 0, "exit") /\ \A x, y \in Boots : (x # y /\ job[x] = job[y] /\ Vouched(x) /\ Vouched(y)) => ~(machine[x] = "up" /\ machine[y] = "up") From e6aa5c57ab5b7fe4be27e3aa0cbbde0d2a91810b Mon Sep 17 00:00:00 2001 From: Roone Date: Mon, 28 Sep 2026 23:11:47 -0600 Subject: [PATCH 14/15] Specify layer 3: sub-agents, the model's processors and meters, under their own cfg (TLC 2.19; cead.cfg 1 call, 2 boots; tree.cfg 2 processes, depth 1, 2 calls) Co-Authored-By: Claude Opus 5.5 (1M context) --- CODE.md | 2 +- README.md | 2 +- spec/cead.cfg | 22 ++- spec/cead.tla | 398 ++++++++++++++++++++++++++++++++++---------------- spec/tree.cfg | 38 +++++ 5 files changed, 329 insertions(+), 133 deletions(-) create mode 100644 spec/tree.cfg diff --git a/CODE.md b/CODE.md index 2884e9f..f4412a5 100644 --- a/CODE.md +++ b/CODE.md @@ -116,7 +116,7 @@ Everything else (fields, structs and enums, most traits, invariants like `len # TLA+ -- Modules are `spec/.tla` with `.cfg`; the system spec is `spec/cead.tla`. TLC is green before any Rust exists; the commit line records the TLA+ tools version and the bounds it passed at. +- Modules are `spec/.tla` with `.cfg`; the system spec is `spec/cead.tla`. A layer whose state multiplies another's gets its own cfg over the same module (`spec/tree.cfg`). TLC is green before any Rust exists; the commit line records the TLA+ tools version and the bounds it passed at. - A PR that changes a protocol re-runs TLC, by hand until CI is demanded. - **spec**: a formula over behaviours of a state machine. **action**: one transition; one signature. **invariant**: what every reachable state satisfies; what TLC checks. **instance**: the bounds TLC searched; a proof only up to them. diff --git a/README.md b/README.md index 920fc27..d498437 100644 --- a/README.md +++ b/README.md @@ -44,7 +44,7 @@ System diagram to come with the first release. - [Recursive Language Models](https://arxiv.org/abs/2512.24601) (Zhang, Kraska, Khattab) - [Language model harnesses are compositional generalizers](https://alexzhang13.github.io/blog/2026/harness/) (Zhang, Khattab) - [OSTEP](https://pages.cs.wisc.edu/~remzi/OSTEP/) (Arpaci-Dusseau) -- [The Datacenter as a Computer](https://link.springer.com/book/10.1007/978-3-031-01761-2) (Barroso, Hölzle, Ranganathan) +- [The Datacenter as a Computer](https://web.eecs.umich.edu/~mosharaf/Readings/DC-Computer.pdf) (Barroso, Clidaras, Hölzle) - [Capability Myths Demolished](https://srl.cs.jhu.edu/pubs/SRL2003-02.pdf) (Miller, Yee, Shapiro) - [Robust Composition](http://www.erights.org/talks/thesis/) (Miller) - [Prime Agent](https://www.primeintellect.ai/blog/prime-agent) ([source](https://github.com/PrimeIntellect-ai/prime-agent)) and [Sandboxes](https://www.primeintellect.ai/blog/sandboxes) (Prime Intellect) diff --git a/spec/cead.cfg b/spec/cead.cfg index 0f1f585..7e085b5 100644 --- a/spec/cead.cfg +++ b/spec/cead.cfg @@ -1,10 +1,16 @@ CONSTANTS - Commands = {c1, c2} - Policy = {c2} - CallLimit = 2 - Boots = {b1, b2} - Root = b1 - NoRecord = NoRecord + Commands = {c1, c2} + Policy = {c2} + CallLimit = 1 + Depth = 0 + MeterCap = 2 + Rights = {} + Processors = 1 + Procs = {p1} + RootProc = p1 + Boots = {b1, b2} + Root = b1 + NoRecord = NoRecord SPECIFICATION Spec @@ -20,6 +26,10 @@ INVARIANTS ReportFirst Rooted OneOutcome + OnProcessors + WithinMeter + Attenuated + KillReach PROPERTIES LogOnlyGrows diff --git a/spec/cead.tla b/spec/cead.tla index 28ab2d1..0f14130 100644 --- a/spec/cead.tla +++ b/spec/cead.tla @@ -1,8 +1,11 @@ -------------------------------- MODULE cead -------------------------------- (***************************************************************************) (* cead as a system. *) -(* Layer 1: a boot, its process, its records and the log. *) +(* Layer 1: a boot, its processes, their records and the log. *) (* Layer 2: snapshot, and boots from one: fork and recovery. *) +(* Layer 3: sub-agents (`agent`), the model's processors, and meters, *) +(* inside one boot. cead.cfg checks boots; tree.cfg checks one *) +(* boot's process tree. *) (* *) (* Assumptions, and who guarantees each. An attested boot proves them; *) (* trusted-host mode asserts them. The protocol is the same in both. *) @@ -13,64 +16,92 @@ (* Attested: the processor. Trusted host: the host. *) (* SnapshotSealed The host cannot alter a snapshot or read its key. *) (* Attested: open research. Trusted host: asserted. *) -(* Availability is the host's in both modes: it can always stop a job. *) +(* Descendants A process can signal only its descendants. *) +(* Both modes: a PID namespace per spawn. *) +(* Availability is the host's and the scheduler's in both modes: the host *) +(* can always stop a job; the scheduler decides when a ready process runs. *) (* Everything on the path, the host included, is a Dolev-Yao network: it *) (* can lose, delay, replay and forge records, but signs only as itself. *) (***************************************************************************) -EXTENDS Naturals, Sequences +EXTENDS Naturals, Sequences, FiniteSets CONSTANTS - Commands, \* what the model can write; the spec never sees shell text - Policy, \* the commands the policy denies; {} is permit-all - CallLimit, \* the limit on calls for one process - Boots, \* model values: each boot, which is also its key - Root, \* the boot `cead run` starts - NoRecord \* a model value: no record awaiting acknowledgment + Commands, \* what the model can write; the spec never sees shell text + Policy, \* the commands the policy denies; {} is permit-all + CallLimit, \* the limit on calls for one process + Depth, \* the limit on depth for the root process + MeterCap, \* the root's meter, and the most `agent` can cap a child's at + Rights, \* what descriptors the root holds rights to + Processors, \* how many of a boot's processes the model can run at once + Procs, \* model values: process slots in a boot + RootProc, \* the process `cead run` starts + Boots, \* model values: each boot, which is also its key + Root, \* the boot `cead run` starts + NoRecord \* a model value: no record awaiting acknowledgment ASSUME /\ Policy \subseteq Commands - /\ CallLimit \in Nat + /\ {CallLimit, Depth, MeterCap, Processors} \subseteq Nat + /\ RootProc \in Procs /\ Root \in Boots Decision(c) == IF c \in Policy THEN "deny" ELSE "allow" -CallTypes == {"intent", "decision", "witness"} \* one call's records -Reasons == {"finish", "timeout"} \* what an exit record can say -Origins == {"run", "fork", "recovery"} \* what a report says started its boot -Signers == Boots \cup {"path", "processor"} \* the processor signs only reports -MaxSeq == 3 * CallLimit + 2 \* the report, every call's records, the exit -None == "none" \* a report not booted from a snapshot +CallTypes == {"intent", "decision", "witness"} \* one call's records +Reasons == {"finish", "meter", "limit", "timeout"} \* why a process or boot ended +Origins == {"run", "fork", "recovery"} \* what a report says started its boot +Signers == Boots \cup {"path", "processor"} \* the processor signs only reports +MaxId == Cardinality(Procs) * CallLimit \* every call of every process +MaxSeq == 3 * MaxId + 2 \* the report, every call's records, the exit +None == "none" \* no process, or no snapshot +Live == {"ready", "running", "blocked"} \* One record of a boot. `seq` is its place in the boot's hash chain: the \* order the machine sent it, whatever order it arrives in. A report (seq 1, \* id 0) names its boot, whose key signs the rest, what started it, and for \* a fork or recovery the snapshot it booted from: that boot and its last -\* record. A call's -\* intent, decision and witness carry its id and command; the exit record -\* carries id 0 and how the machine exited. -Record == [boot : Boots, seq : 1..MaxSeq, id : 0..CallLimit, +\* record. A call's intent, decision and witness carry its id and command; +\* the exit record carries id 0 and why the boot ended. +Record == [boot : Boots, seq : 1..MaxSeq, id : 0..MaxId, type : CallTypes \cup {"report", "exit"}, body : Commands \cup Reasons \cup Origins, key : Signers, from : Boots \cup {None}, last : 0..MaxSeq] +\* One process, as the harness holds it. `cap` is the meter it was given, +\* `meter` what remains; `waits` is the child it waits for in the foreground; +\* `status` is why it ended, and `by` the process that killed it. +Proc == [state : {"unused", "zombie", "reaped"} \cup Live, + parent : Procs \cup {None}, calls : 0..CallLimit, + cap : 0..MeterCap, meter : 0..MeterCap, depth : 0..Depth, + rights : SUBSET Rights, waits : Procs \cup {None}, + status : Reasons \cup {"killed", None}, by : Procs \cup {None}] + +Unused == [state |-> "unused", parent |-> None, calls |-> 0, cap |-> 0, meter |-> 0, + depth |-> 0, rights |-> {}, waits |-> None, status |-> None, by |-> None] +Spawned(parent, cap, depth, rights) == + [state |-> "ready", parent |-> parent, calls |-> 0, cap |-> cap, meter |-> cap, + depth |-> depth, rights |-> rights, waits |-> None, status |-> None, by |-> None] +RootTable == [p \in Procs |-> IF p = RootProc THEN Spawned(None, MeterCap, Depth, Rights) + ELSE Unused] + VARIABLES - machine, \* per boot: "off", "up", "exiting", "evicted" - process, \* per boot, its root process: "initial", "running", "blocked", "zombie" - calls, \* per boot: calls issued so far; the current call's id + machine, \* per boot: "off", "booting", "up", "exiting", "evicted" + ps, \* per boot and process: a Proc + intent, \* per boot and process: the intent awaiting acknowledgment, or NoRecord + ids, \* per boot: the last call id seq, \* per boot: the machine's last sequence number - pending, \* per boot: the record awaiting the log's acknowledgment, or NoRecord + pending, \* per boot: the report or exit record awaiting acknowledgment, or NoRecord executed, \* per boot: what the kernel ran, in order: the truth job, \* per boot: the boot that started its job - snapshots, \* every snapshot taken: a boot, its last record, its calls + snapshots, \* every snapshot taken: a boot, its last record, its processes transit, \* every record sent: each can be lost, delayed, reordered, duplicated log \* held outside the machine: a set of records -vars == <> -boot == <> +vars == <> Rec(b, s, i, t, x) == [boot |-> b, seq |-> s, id |-> i, type |-> t, body |-> x, key |-> b, from |-> None, last |-> 0] -Report(b, o, p, h) == [boot |-> b, seq |-> 1, id |-> 0, type |-> "report", body |-> o, - key |-> "processor", from |-> p, last |-> h] +Report(b, o, f, l) == [boot |-> b, seq |-> 1, id |-> 0, type |-> "report", body |-> o, + key |-> "processor", from |-> f, last |-> l] Logged(b, s) == \E r \in log : r.boot = b /\ r.seq = s LoggedType(b, i, t) == \E r \in log : r.boot = b /\ r.id = i /\ r.type = t \* The log holds boot b's report: b's key is vouched for. @@ -80,13 +111,40 @@ Recovered(b) == \E r \in log : r.type = "report" /\ r.body = "recovery" / \* Boot b is evicted without its exit record in the log. Unknown(b) == machine[b] = "evicted" /\ ~\E r \in log : r.boot = b /\ r.type = "exit" +RECURSIVE Ancestors(_, _) +Ancestors(b, p) == IF ps[b, p].parent = None THEN {} + ELSE {ps[b, p].parent} \cup Ancestors(b, ps[b, p].parent) +Descendants(b, p) == {q \in Procs : p \in Ancestors(b, q)} +Running(b) == {p \in Procs : ps[b, p].state = "running"} +\* Every meter from p up to the root has a unit left. +Chargeable(b, p) == \A a \in {p} \cup Ancestors(b, p) : ps[b, a].meter >= 1 + +RECURSIVE CallsIn(_, _) +CallsIn(b, S) == IF S = {} THEN 0 + ELSE LET p == CHOOSE p \in S : TRUE IN ps[b, p].calls + CallsIn(b, S \ {p}) + +\* Boot b's processes with p and its live descendants ended: p for `why`, +\* the rest killed by p. Their calls in progress are cut off. +Ended(b, p, why) == + LET T == {p} \cup {q \in Descendants(b, p) : ps[b, q].state \in Live} + IN [x \in Boots \X Procs |-> + IF x[1] = b /\ x[2] \in T + THEN [ps[x] EXCEPT !.state = "zombie", !.waits = None, + !.status = IF x[2] = p THEN why ELSE "killed", + !.by = IF x[2] = p THEN @ ELSE p] + ELSE ps[x]] +CutOff(b, p) == + [x \in Boots \X Procs |-> + IF x[1] = b /\ x[2] \in {p} \cup Descendants(b, p) THEN NoRecord ELSE intent[x]] + ----------------------------------------------------------------------------- -(* A boot and its process *) +(* A boot *) Init == /\ machine = [b \in Boots |-> "off"] - /\ process = [b \in Boots |-> "initial"] - /\ calls = [b \in Boots |-> 0] + /\ ps = [x \in Boots \X Procs |-> Unused] + /\ intent = [x \in Boots \X Procs |-> NoRecord] + /\ ids = [b \in Boots |-> 0] /\ seq = [b \in Boots |-> 0] /\ pending = [b \in Boots |-> NoRecord] /\ executed = [b \in Boots |-> <<>>] @@ -95,19 +153,20 @@ Init == /\ transit = {} /\ log = {} -\* The VMM starts boot b: it makes its key and sends its report, which -\* awaits acknowledgment. `c` is the calls its process has already issued. -Begin(b, r, c, j) == - /\ machine' = [machine EXCEPT ![b] = "up"] +\* The VMM starts boot b with processes `t`: it makes its key and sends its +\* report, which awaits acknowledgment. +Begin(b, r, t, i, j) == + /\ machine' = [machine EXCEPT ![b] = "booting"] + /\ ps' = [x \in Boots \X Procs |-> IF x[1] = b THEN t[x[2]] ELSE ps[x]] + /\ ids' = [ids EXCEPT ![b] = i] /\ seq' = [seq EXCEPT ![b] = 1] - /\ calls' = [calls EXCEPT ![b] = c] /\ pending' = [pending EXCEPT ![b] = r] /\ job' = [job EXCEPT ![b] = j] /\ transit' = transit \cup {r} - /\ UNCHANGED <> + /\ UNCHANGED <> \* `cead run` boots the root. -Boot == machine[Root] = "off" /\ Begin(Root, Report(Root, "run", None, 0), 0, Root) +Boot == machine[Root] = "off" /\ Begin(Root, Report(Root, "run", None, 0), RootTable, 0, Root) \* A boot from a snapshot. A fork starts a new job, whenever anyone asks; \* a recovery continues the snapshot's job, once its boot is unknown. @@ -115,75 +174,31 @@ BootFrom(b, s, o) == /\ b # Root /\ machine[b] = "off" /\ o = "recovery" => Unknown(s.boot) - /\ Begin(b, Report(b, o, s.boot, s.last), s.calls, + /\ Begin(b, Report(b, o, s.boot, s.last), s.procs, s.ids, IF o = "fork" THEN b ELSE job[s.boot]) -\* The log holds the report: init assembles the view, the harness starts the -\* root process. Nothing runs on a boot the log has not heard of. +\* The log holds the report: init assembles the view, the harness runs. +\* Nothing runs on a boot the log has not heard of. Start(b) == - /\ machine[b] = "up" - /\ process[b] = "initial" - /\ pending[b] # NoRecord - /\ pending[b].type = "report" + /\ machine[b] = "booting" /\ Logged(b, 1) - /\ process' = [process EXCEPT ![b] = "running"] - /\ pending' = [pending EXCEPT ![b] = NoRecord] - /\ UNCHANGED <> - -\* The model issues a call. The harness blocks the process and sends the -\* intent, which awaits acknowledgment. -Issue(b, c) == - /\ machine[b] = "up" - /\ process[b] = "running" - /\ calls[b] < CallLimit - /\ LET r == Rec(b, seq[b] + 1, calls[b] + 1, "intent", c) - IN /\ process' = [process EXCEPT ![b] = "blocked"] - /\ calls' = [calls EXCEPT ![b] = calls[b] + 1] - /\ seq' = [seq EXCEPT ![b] = seq[b] + 1] - /\ pending' = [pending EXCEPT ![b] = r] - /\ transit' = transit \cup {r} - /\ UNCHANGED <> - -\* The log has acknowledged the intent: the harness checks the call against -\* policy. Deny returns to the model. Allow runs the command, and the tracer -\* witnesses it; both records go through the harness, which sequences them. -Decide(b) == - /\ machine[b] = "up" - /\ process[b] = "blocked" - /\ pending[b] # NoRecord - /\ pending[b].type = "intent" - /\ Logged(b, pending[b].seq) - /\ LET c == pending[b].body - i == pending[b].id - s == seq[b] - IN IF Decision(c) = "allow" - THEN /\ executed' = [executed EXCEPT ![b] = Append(@, [id |-> i, cmd |-> c])] - /\ transit' = transit \cup - {Rec(b, s + 1, i, "decision", c), Rec(b, s + 2, i, "witness", c)} - /\ seq' = [seq EXCEPT ![b] = s + 2] - ELSE /\ executed' = executed - /\ transit' = transit \cup {Rec(b, s + 1, i, "decision", c)} - /\ seq' = [seq EXCEPT ![b] = s + 1] - /\ process' = [process EXCEPT ![b] = "running"] + /\ machine' = [machine EXCEPT ![b] = "up"] /\ pending' = [pending EXCEPT ![b] = NoRecord] - /\ UNCHANGED <> + /\ UNCHANGED <> -\* The whole machine at an instant, between calls, once the log holds every -\* record so far. +\* The whole machine at an instant: no call in progress, and the log holds +\* every record so far. A process that was running is ready: its inference +\* does not survive the snapshot. Snapshot(b) == /\ machine[b] = "up" - /\ process[b] = "running" + /\ \A p \in Procs : intent[b, p] = NoRecord /\ \A s \in 1..seq[b] : Logged(b, s) - /\ snapshots' = snapshots \cup {[boot |-> b, last |-> seq[b], calls |-> calls[b]]} - /\ UNCHANGED <> - -\* The model replies without a command: the process is a zombie until the -\* harness reaps it. The exit record calls this `finish`. -Finish(b) == - /\ machine[b] = "up" - /\ process[b] = "running" - /\ process' = [process EXCEPT ![b] = "zombie"] - /\ UNCHANGED <> + /\ snapshots' = snapshots \cup + {[boot |-> b, last |-> seq[b], ids |-> ids[b], + procs |-> [p \in Procs |-> IF ps[b, p].state = "running" + THEN [ps[b, p] EXCEPT !.state = "ready"] + ELSE ps[b, p]]]} + /\ UNCHANGED <> \* The machine signs its exit record, its last record, and waits for the log \* to acknowledge it. Any call in progress is cut off. @@ -194,10 +209,10 @@ Exit(b, reason) == /\ seq' = [seq EXCEPT ![b] = seq[b] + 1] /\ pending' = [pending EXCEPT ![b] = r] /\ transit' = transit \cup {r} - /\ UNCHANGED <> + /\ UNCHANGED <> -\* The harness reaps the root process. -Reap(b) == process[b] = "zombie" /\ Exit(b, "finish") +\* The root process has ended: the boot exits with its reason. +Reap(b) == ps[b, RootProc].state = "zombie" /\ Exit(b, ps[b, RootProc].status) \* The machine's own wall-time limit fires. Timeout(b) == Exit(b, "timeout") @@ -207,20 +222,127 @@ Leave(b) == /\ Logged(b, pending[b].seq) /\ machine' = [machine EXCEPT ![b] = "evicted"] /\ pending' = [pending EXCEPT ![b] = NoRecord] - /\ UNCHANGED <> + /\ UNCHANGED <> \* The machine ends without an acknowledged exit record. A crash can happen \* at any point. The host's hard kill is the same event, but it is assumed \* to happen (see Spec): it is what makes every job end. Evict(b) == - /\ machine[b] \in {"up", "exiting"} + /\ machine[b] \in {"booting", "up", "exiting"} /\ machine' = [machine EXCEPT ![b] = "evicted"] /\ pending' = [pending EXCEPT ![b] = NoRecord] - /\ UNCHANGED <> + /\ UNCHANGED <> Crash(b) == Evict(b) HostKill(b) == Evict(b) +----------------------------------------------------------------------------- +(* A boot's processes *) + +\* The scheduler gives a ready process one of the model's processors. +Dispatch(b, p) == + /\ machine[b] = "up" + /\ ps[b, p].state = "ready" + /\ Cardinality(Running(b)) < Processors + /\ ps' = [ps EXCEPT ![b, p].state = "running"] + /\ UNCHANGED <> + +\* The processor returns a command. Its unit is charged to every meter from +\* the process up to the root; the process releases the processor, blocks, +\* and sends the intent, which awaits acknowledgment. +Issue(b, p, c) == + /\ machine[b] = "up" + /\ ps[b, p].state = "running" + /\ ps[b, p].calls < CallLimit + /\ Chargeable(b, p) + /\ LET r == Rec(b, seq[b] + 1, ids[b] + 1, "intent", c) + A == {p} \cup Ancestors(b, p) + IN /\ ps' = [x \in Boots \X Procs |-> + IF x[1] = b /\ x[2] \in A + THEN [ps[x] EXCEPT !.meter = @ - 1, + !.calls = IF x[2] = p THEN @ + 1 ELSE @, + !.state = IF x[2] = p THEN "blocked" ELSE @] + ELSE ps[x]] + /\ intent' = [intent EXCEPT ![b, p] = r] + /\ ids' = [ids EXCEPT ![b] = ids[b] + 1] + /\ seq' = [seq EXCEPT ![b] = seq[b] + 1] + /\ transit' = transit \cup {r} + /\ UNCHANGED <> + +\* The log has acknowledged the intent: the harness checks the call against +\* policy. Deny returns to the model. Allow runs the command, and the tracer +\* witnesses it; both records go through the harness, which sequences them. +\* `agent` spawns a child in the foreground (the caller waits) or the +\* background; it fails if the caller's depth is spent or no slot is free. +\* `kill` ends one of the caller's live children and its descendants. +Decide(b, p) == + /\ machine[b] = "up" + /\ ps[b, p].state = "blocked" + /\ intent[b, p] # NoRecord + /\ Logged(b, intent[b, p].seq) + /\ LET c == intent[b, p].body + i == intent[b, p].id + s == seq[b] + me == ps[b, p] + Free == {q \in Procs : ps[b, q].state = "unused"} + Kids == {q \in Procs : ps[b, q].parent = p /\ ps[b, q].state \in Live} + Done(t) == [t EXCEPT ![b, p].state = "ready"] + IN /\ IF Decision(c) = "allow" + THEN /\ executed' = [executed EXCEPT ![b] = Append(@, [id |-> i, cmd |-> c])] + /\ transit' = transit \cup + {Rec(b, s + 1, i, "decision", c), Rec(b, s + 2, i, "witness", c)} + /\ seq' = [seq EXCEPT ![b] = s + 2] + /\ IF c = "agent" /\ me.depth > 0 /\ Free # {} + THEN \E q \in Free, m \in 1..MeterCap, R \in SUBSET me.rights, + fg \in BOOLEAN : + LET t == [ps EXCEPT ![b, q] = Spawned(p, m, me.depth - 1, R)] + IN ps' = IF fg THEN [t EXCEPT ![b, p].waits = q] ELSE Done(t) + ELSE IF c = "kill" /\ Kids # {} + THEN \E q \in Kids : + LET t == [Ended(b, q, "killed") EXCEPT ![b, q].by = p] + IN /\ ps' = Done(t) + /\ intent' = [CutOff(b, q) EXCEPT ![b, p] = NoRecord] + ELSE ps' = Done(ps) + ELSE /\ executed' = executed + /\ transit' = transit \cup {Rec(b, s + 1, i, "decision", c)} + /\ seq' = [seq EXCEPT ![b] = s + 1] + /\ ps' = Done(ps) + /\ (c # "kill" \/ Decision(c) = "deny" \/ Kids = {}) => + intent' = [intent EXCEPT ![b, p] = NoRecord] + /\ UNCHANGED <> + +\* The model replies without a command: the process ends, and its running +\* descendants are killed. The reply is its stdout. +Finish(b, p) == + /\ machine[b] = "up" + /\ ps[b, p].state = "running" + /\ ps' = Ended(b, p, "finish") + /\ intent' = CutOff(b, p) + /\ UNCHANGED <> + +\* The processor returns a command the process cannot pay for, or its call +\* limit is reached: it ends, and its descendants are killed. +Exhaust(b, p) == + /\ machine[b] = "up" + /\ ps[b, p].state = "running" + /\ \/ ~Chargeable(b, p) /\ ps' = Ended(b, p, "meter") + \/ ps[b, p].calls = CallLimit /\ ps' = Ended(b, p, "limit") + /\ intent' = CutOff(b, p) + /\ UNCHANGED <> + +\* The harness reaps an ended child; a parent waiting on it in the +\* foreground is ready again. +ReapChild(b, q) == + /\ machine[b] = "up" + /\ q # RootProc + /\ ps[b, q].state = "zombie" + /\ LET p == ps[b, q].parent + t == [ps EXCEPT ![b, q].state = "reaped"] + IN ps' = IF ps[b, p].waits = q /\ ps[b, p].state = "blocked" + THEN [t EXCEPT ![b, p].state = "ready", ![b, p].waits = None] + ELSE t + /\ UNCHANGED <> + ----------------------------------------------------------------------------- (* Records in transit: outside the machine, so they go on after eviction *) (* A record once sent stays in transit: one never delivered is lost, one *) @@ -228,12 +350,11 @@ HostKill(b) == Evict(b) \* The log keeps a report only if the processor signed it; a recovery only \* while the boot it recovers is not complete, and only the first for that -\* boot. -\* It keeps any other record only if its boot's key signed it, the log holds -\* that boot's report, and no recovery has taken the boot's place. It keeps -\* the first record for each place in a boot's hash chain; a duplicate or -\* resend changes nothing. First-wins matters only if KeySecret fails, so -\* TLC never exercises it. +\* boot. It keeps any other record only if its boot's key signed it, the log +\* holds that boot's report, and no recovery has taken the boot's place. It +\* keeps the first record for each place in a boot's hash chain; a +\* duplicate or resend changes nothing. First-wins matters only if +\* KeySecret fails, so TLC never exercises it. Arrive(r) == /\ IF r.type = "report" THEN /\ r.key = "processor" @@ -245,7 +366,7 @@ Arrive(r) == /\ ~Recovered(r.boot) /\ ~Logged(r.boot, r.seq) /\ log' = log \cup {r} - /\ UNCHANGED <> + /\ UNCHANGED <> Deliver(r) == r \in transit /\ Arrive(r) @@ -261,9 +382,12 @@ Next == \/ Boot \/ \E b \in Boots, s \in snapshots, o \in {"fork", "recovery"} : BootFrom(b, s, o) \/ \E b \in Boots : - \/ Start(b) \/ Decide(b) \/ Snapshot(b) \/ Finish(b) - \/ Reap(b) \/ Timeout(b) \/ Leave(b) \/ Crash(b) \/ HostKill(b) - \/ \E c \in Commands : Issue(b, c) + \/ Start(b) \/ Snapshot(b) \/ Reap(b) \/ Timeout(b) \/ Leave(b) + \/ Crash(b) \/ HostKill(b) + \/ \E p \in Procs : + \/ Dispatch(b, p) \/ Decide(b, p) \/ Finish(b, p) \/ Exhaust(b, p) + \/ ReapChild(b, p) + \/ \E c \in Commands : Issue(b, p, c) \/ \E r \in transit : Deliver(r) \/ Forge(r) Spec == Init /\ [][Next]_vars /\ \A b \in Boots : WF_vars(HostKill(b)) @@ -272,12 +396,13 @@ Spec == Init /\ [][Next]_vars /\ \A b \in Boots : WF_vars(HostKill(b)) (* Properties *) TypeOK == - /\ machine \in [Boots -> {"off", "up", "exiting", "evicted"}] - /\ process \in [Boots -> {"initial", "running", "blocked", "zombie"}] - /\ calls \in [Boots -> 0..CallLimit] + /\ machine \in [Boots -> {"off", "booting", "up", "exiting", "evicted"}] + /\ ps \in [Boots \X Procs -> Proc] + /\ intent \in [Boots \X Procs -> Record \cup {NoRecord}] + /\ ids \in [Boots -> 0..MaxId] /\ seq \in [Boots -> 0..MaxSeq] /\ pending \in [Boots -> Record \cup {NoRecord}] - /\ \A b \in Boots : executed[b] \in Seq([id : 1..CallLimit, cmd : Commands]) + /\ \A b \in Boots : executed[b] \in Seq([id : 1..MaxId, cmd : Commands]) /\ job \in [Boots -> Boots] /\ transit \subseteq Record /\ log \subseteq Record @@ -298,7 +423,7 @@ DenyNeverRuns == \* 4. A process makes at most CallLimit calls: TypeOK bounds `calls`. \* 5. Every boot that starts ends, and its machine is evicted. -BootEnds == \A b \in Boots : (machine[b] = "up") ~> (machine[b] = "evicted") +BootEnds == \A b \in Boots : (machine[b] = "booting") ~> (machine[b] = "evicted") \* 6. The log holds only what the processor signed, or a boot's own key. OnlyMachine == \A r \in log : r.key = "processor" \/ (r.key = r.boot /\ Vouched(r.boot)) @@ -314,10 +439,11 @@ Unambiguous == LET Seen == {r \in transit : r.key # "path"} \cup log IN \A r1, r2 \in Seen : (r1.boot = r2.boot /\ r1.seq = r2.seq) => r1 = r2 -\* 9. An exit record saying `finish` means the model ended its turn: no -\* call was cut off. +\* 9. An exit record saying `finish` means the root process ended its turn: +\* it was not cut off. FinishHonest == - \A r \in log : (r.type = "exit" /\ r.body = "finish") => process[r.boot] = "zombie" + \A r \in log : (r.type = "exit" /\ r.body = "finish") => + ps[r.boot, RootProc].status = "finish" \* 10. A boot is complete when the log holds its exit record with no gap \* before it: then every call it executed has all three records logged. @@ -328,10 +454,10 @@ Complete == \A t \in CallTypes : LoggedType(x.boot, executed[x.boot][e].id, t) \* 11. Nothing runs on a boot until the log holds its report. -ReportFirst == \A b \in Boots : process[b] # "initial" => Vouched(b) +ReportFirst == \A b \in Boots : machine[b] \in {"up", "exiting"} => Vouched(b) \* 12. A fork or recovery names a record the log holds: its snapshot's last -\* record when the snapshot was taken. +\* record. Rooted == \A r \in log : (r.type = "report" /\ r.from # None) => Logged(r.from, r.last) @@ -344,4 +470,26 @@ OneOutcome == (x # y /\ job[x] = job[y] /\ Vouched(x) /\ Vouched(y)) => ~(machine[x] = "up" /\ machine[y] = "up") +\* 14. The model runs at most Processors of a boot's processes at once. +OnProcessors == \A b \in Boots : Cardinality(Running(b)) <= Processors + +\* 15. No process tree spends more than its root's meter: every call below a +\* process was charged to it. +WithinMeter == + \A b \in Boots, p \in Procs : + ps[b, p].state # "unused" => CallsIn(b, {p} \cup Descendants(b, p)) <= ps[b, p].cap + +\* 16. A child holds no right and no depth its parent lacked. +Attenuated == + \A b \in Boots, p \in Procs : + LET q == ps[b, p].parent + IN (ps[b, p].state # "unused" /\ q # None) => + /\ ps[b, p].rights \subseteq ps[b, q].rights + /\ ps[b, p].depth < ps[b, q].depth + +\* 17. A process is killed only by one of its ancestors. +KillReach == + \A b \in Boots, p \in Procs : + ps[b, p].status = "killed" => ps[b, p].by \in Ancestors(b, p) + ============================================================================= diff --git a/spec/tree.cfg b/spec/tree.cfg new file mode 100644 index 0000000..57f65df --- /dev/null +++ b/spec/tree.cfg @@ -0,0 +1,38 @@ +CONSTANTS + Commands = {c1, "agent", "kill"} + Policy = {} + CallLimit = 2 + Depth = 1 + MeterCap = 2 + Rights = {r1} + Processors = 1 + Procs = {p1, p2} + RootProc = p1 + Boots = {b1} + Root = b1 + NoRecord = NoRecord + +SPECIFICATION Spec + +INVARIANTS + TypeOK + IntentFirst + DenyNeverRuns + OnlyMachine + ExecutedOnce + Unambiguous + FinishHonest + Complete + ReportFirst + Rooted + OneOutcome + OnProcessors + WithinMeter + Attenuated + KillReach + +PROPERTIES + LogOnlyGrows + BootEnds + +CHECK_DEADLOCK FALSE From 39fe16908229e7f95e86bee823e2f36f8c6863cd Mon Sep 17 00:00:00 2001 From: Roone Date: Mon, 28 Sep 2026 23:41:11 -0600 Subject: [PATCH 15/15] Make the README a whiteboard: what cead is and how it works, scannable, with no status to drift Co-Authored-By: Claude Opus 5.5 (1M context) --- README.md | 218 +++++++++++++++++++++++------------------------------- 1 file changed, 92 insertions(+), 126 deletions(-) diff --git a/README.md b/README.md index d498437..2ac215f 100644 --- a/README.md +++ b/README.md @@ -6,39 +6,36 @@ cead (Irish: permission; "kyad")

-cead is an agent harness built as a confidential microVM: a userspace for a model, over a kernel that enforces and witnesses, whose evidence does not depend on who owns the hardware. -The model gets a Linux machine of its own and a shell to drive it: the kernel permits each command, and eBPF witnesses it. +cead is an agent harness built as a confidential microVM. +A userspace for a model, over a kernel that enforces and witnesses, +whose evidence does not depend on who owns the hardware. ## What cead is -A pinned Linux kernel in a confidential microVM. -The model gets a system prompt and a shell, as in any agent harness. -Every command it writes runs as a Linux process under the kernel's own controls: seccomp, Landlock and cgroups. -An eBPF program in the kernel records what each process did, in a place the model's processes cannot reach. - -Most agent harnesses state their limits in prompt text and application code, then say what happened from inside the process that did it. -cead has the kernel enforce the limits and the kernel write the record, so the record does not depend on the model or the harness telling the truth. - -Nor does it depend on the host. -The processor attests what booted, and the machine signs its record with a key the host cannot read. -The host can stop a job, but cannot read it or forge its record. -On hardware without attestation, the same machine runs unattested and says so. - -Harness design is memory-management policy. -The context window is a cache; the model's state lives in the machine, in files, and the model reaches it through the shell. -A script that stands up a service, runs forty commands and prints `ok` has advanced the task by forty commands and cost the context window one line. -All forty ran under kernel policy and were recorded, whether or not the model mentioned them. +- **A machine for the model.** + A pinned Linux kernel in a microVM; the model drives it through a shell. +- **The kernel enforces.** + Each command runs as a Linux process under seccomp, Landlock and cgroups. +- **The kernel records.** + eBPF writes what each process did, out of the model's reach. + Most harnesses report from the process that acted; here the model's processes never touch the record. +- **The host cannot forge it.** + On attested hardware, the processor attests what booted. + The machine signs its records with a key the host cannot read. + The host can stop a job or drop its records; it cannot read the job or forge them. + Without attestation hardware, the same machine runs unattested and says so. +- **Harness design is memory-management policy.** + The context window is a cache; state lives in files, reached through the shell. + Forty commands in a script that prints `ok`: one line of window, forty enforced and witnessed. Three interfaces; everything between two lines is swappable. | Line | Interface | |---|---| -| VMM ↔ machine | measured boot, content-addressed disks, attestation; devices are untrusted input | +| VMM ↔ machine | measured boot, content-addressed disks, attestation | | kernel ↔ commands | Linux syscall ABI | | commands ↔ model | POSIX sh, GNU flags and error text | -System diagram to come with the first release. - ### Reading - [Recursive Language Models](https://arxiv.org/abs/2512.24601) (Zhang, Kraska, Khattab) @@ -49,53 +46,37 @@ System diagram to come with the first release. - [Robust Composition](http://www.erights.org/talks/thesis/) (Miller) - [Prime Agent](https://www.primeintellect.ai/blog/prime-agent) ([source](https://github.com/PrimeIntellect-ai/prime-agent)) and [Sandboxes](https://www.primeintellect.ai/blog/sandboxes) (Prime Intellect) + ## What cead is not -- Not a container runtime. - cead uses container images and container schedulers, and replaces the container itself with a microVM. -- Not a conversation. +- **Not a container runtime.** + It uses container images and schedulers; a microVM replaces the container. +- **Not a conversation.** Nothing carries between jobs except state in the machine. - A job's context window is the system prompt, the query, and what the model has read since. -- Not a policy. - You bring your own, written in Cedar, and cead compiles it into kernel rules; cead does not decide what a model should be allowed to do. -- Not a new interface for the model. - The model gets a POSIX shell with GNU tools, because that is the interface with the most training data behind it and the one the kernel already enforces. - A bespoke tool schema is out of distribution, has to be taught in every prompt, and needs a translation layer between what the model said and what was enforced. +- **Not a policy.** + You bring your own, in Cedar; cead compiles it into kernel rules. +- **Not a new interface.** + POSIX sh and GNU tools: the most training data, and what the kernel already enforces. + A bespoke tool schema must be taught in every prompt and translated before it can be enforced. ## How to use cead -Install instructions come with the first release. - -A manifest is one file that names a machine: kernel, task image, policy, VMM, and the model: its weights and engine. -Two ways to run it: - -- `cead` boots the machine the manifest describes and opens a shell over it. - Each command in that shell is one operator verb; `run` starts the model. -- `cead run` does one run from your own shell and returns. - argv is the query, stdin is the context, stdout is the answer, and the exit code is the outcome. +A **manifest** is one file that names a machine: kernel, task image, policy, VMM, model (weights, engine). -A query is the length of a commit message; anything longer is a file in the machine for the model to read. +- `cead` opens the console over a manifest and its state; `run` starts a job. +- `cead run "query" < context > answer` does one job and returns; the exit code is the outcome. +- A query is commit-message sized; anything longer is a file for the model to read. What a job does, from manifest to first command: -1. The VMM boots one kernel and attaches two read-only disks: the core (cead's tools, policy and eBPF programs, built by nix) and the task image. -2. init runs as root, before any model process exists. - It loads the eBPF programs into the kernel and compiles the policy into a seccomp filter and a Landlock ruleset. -3. init mounts one filesystem: the task image as root, the core first on PATH, and each descriptor (context on stdin, checkout, scratch, database file). -4. The harness forks the root process, attaches the policy, drops to an unprivileged uid, and execs the shell. - Every child inherits the policy; no process can remove it. -5. The harness renders the system prompt from what it mounted, so it cannot claim what is not there, and sends it with the query to the engine. -6. The model writes its first command. - -Three kinds of file, three fates: - -| File | Consumed by | Becomes | The model's relation to it | -|---|---|---|---| -| eBPF program | init, via `bpf()` | a kernel object | needs CAP_BPF to touch; has none | -| policy | init, via seccomp and Landlock | attributes of every process | no syscall loosens them | -| context, checkout, database | mount and descriptor | files in the view, with rights | reads and writes within them | - -Example run and screen recording to come with the first release. +1. The VMM boots the kernel with two read-only disks: the core (built by nix) and the task image. +2. The machine makes its key and sends its report; nothing runs until the log holds it. +3. init, as root, loads the eBPF programs and compiles the policy into seccomp and Landlock. +4. init mounts the view: the task image as root, the core first on PATH, one descriptor per grant. +5. The harness spawns the root process: policy attached, an unprivileged uid, the shell. + Every child inherits the policy; no syscall loosens it, and no model process holds CAP_BPF. +6. The harness sends the engine the query and a system prompt rendered from what it mounted. +7. The model writes its first command. ## Dependencies @@ -106,91 +87,76 @@ Example run and screen recording to come with the first release. | shell and tools | brush, uutils, SQLite | | policy | Cedar | | VMMs | Cloud Hypervisor (SEV-SNP on KVM); Firecracker and Virtualization.framework, unattested | +| attestation | AMD SEV-SNP, Linux TSM reports (configfs-tsm), virtee/sev | | images and build | OCI images, nix | ## Deployment -The machine runs wherever the cead CLI runs: a laptop or a cloud VM with a hypervisor. -The model runs wherever the manifest's engine is: a hosted API or a local server. -The CLI drives everything below: it reads the manifest, boots, runs, snapshots, forks, and reads the log. - -The machine is the unit of scale. -Work fans out three ways, told apart by who spawns and when: +The machine is the unit of scale. Work fans out three ways: -| Use | Who spawns | When | Mechanism | +| Mechanism | Who spawns | When | What | |---|---|---|---| -| evals | operator | before the job | scale-out: N machines from one manifest | -| reinforcement learning | operator or trainer | mid-job, at a chosen state | fork: K machines from one snapshot, the way a git worktree forks a checkout | -| long or autonomous tasks | the model | whenever it decides | `agent`: a sub-agent process inside the machine | - -- Kubernetes can schedule machines as pods; Firecracker was built for this shape of workload. -- The long-term direction is one box: model, inference engine, kernel and cead. +| scale-out | operator | before a job | N machines from one manifest | +| fork | operator | mid-job | K machines from one snapshot | +| `agent` | the model | whenever it decides | a sub-agent process in the machine | ### Identity -- The machine is the boundary. - Everything a job can touch is inside one disposable microVM, so the questions that usually need users, roles and sessions collapse to one: which machine. -- A manifest answers it by hash. - Two machines with the same manifest are the same experiment. -- Operator and model are told apart by where they stand. - The operator runs the CLI on the host; the model runs inside the machine as an unprivileged user. -- Access is granted; content is discovered. - Every file, socket or database the model can reach was granted to it by cead, and a child process gets no more than its parent held. - What is in them, the model finds for itself. -- Authority is per tool: how far a tool can go beyond what its command line says. - `grep` does only what its arguments say; `python` can do anything the process may. - The class picks the tool's kernel policy and says how to read its trace. -- The host is out of reach, and untrusted. - The grader and long-lived API keys stay on the host; the machine holds only a token scoped to its job, and the log is held outside the machine. - The host is trusted only to keep a job running: it can stop one, but not read it or forge its log. - Trusted-host mode asserts the rest instead of proving it. - -### Hardware - -Cloud Hypervisor boots attested machines on bare-metal AMD EPYC with SEV-SNP, and the same machine unattested on any KVM host. -Firecracker and Virtualization.framework boot it unattested, so the harness runs where developers are. +- **The machine is the boundary.** + Users, roles and sessions collapse to one question: which machine. +- **A manifest answers it by hash.** + Machines from one manifest start identical. +- **Where you stand says who you are.** + The operator runs the CLI on the host; the model is an unprivileged user in the machine. +- **Access is granted; content is discovered.** + cead grants every file, socket and database; a child gets no more than its parent. +- **Authority is per tool.** + `grep` does what its arguments say; `python` can do anything its process may. + The tool's class sets its policy and how to read its trace. +- **Long-lived keys stay on the host.** + The machine holds its boot's signing key and a job-scoped token for the model. + +### Hosts + +- Cloud Hypervisor: attested on bare-metal AMD EPYC with SEV-SNP; unattested on any KVM host. +- Firecracker and Virtualization.framework: unattested. +- The model runs wherever the manifest's engine is: a hosted API or our own. +- A scheduler places machines on hosts; it never sees inside one. ### Network -The model's processes have no network. -The machine reaches the host over vsock only. -The host relays inference, encrypted between the harness and the engine, and the machine's records to the log. -Rules beyond that come with the first release. +- The model's processes have no network. +- The machine reaches the host only over vsock. +- The host relays inference and the machine's records to the log. +- Inference is encrypted end to end to our own engine; a hosted API goes through a gateway on the host. ### Workloads -- Build time. - A task's tools are packed into a read-only OCI image; a SWE-bench instance image works as is. -- Each call. - The harness assembles the context window from the system prompt, the query and the bounded output of every command so far, and sends it to the engine. - It runs the command that comes back and adds the output, cut at a size cap, to the window; the full output goes to a file the model can read piecewise. -- Sub-agents, called programmatically. - `agent` starts a child process with a slice of the parent's context on stdin, a meter under its parent's, the same tools, and its own context window. - It is a command, so the shell composes it: loops, pipes, `&`, `wait`, `kill`. - A child's answer lands in a file or a shell variable and enters a window only when read. -- Forking, of the machine. - A snapshot of a running machine boots another machine that diverges from the same state. -- Ending. - A process ends when the model replies without a command; the reply is its answer on stdout. - Ending kills its running sub-agents, so `wait` first to keep them. - When the root process ends, the job is over and the machine is gone. +- **Build.** + A task's tools are a read-only OCI image. +- **Each call.** + The harness sends the engine the window: system prompt, query, each output so far, cut at a cap. + It runs the command that comes back; output past the cap spills to a file. +- **Sub-agents.** + `agent` spawns a child process: a slice on stdin, a meter under its parent's, its own window. + The shell composes it (`&`, `wait`, `kill`); its answer stays in a file or variable until read. +- **Fork.** + A snapshot boots another machine with a new key. + A fork starts a new job; a recovery continues one whose boot was lost, at most once. +- **Ending.** + A process ends when the model replies without a command; the reply is its stdout. + Ending kills running sub-agents; `wait` first to keep them. + When the root process ends, the job ends and the machine is gone. ### Data -- State is files in the machine, reached through the shell. -- The database is a file. - SQLite is a core tool, so a relational database is a file in the filesystem and a snapshot captures it. -- Postgres is a task tool for tasks that need extensions, concurrency or an existing data directory. - It runs inside the machine, so a snapshot still captures it. -- State leaves the machine on purpose. - A job's answer is stdout; a checkout can be pushed; a snapshot can be exported. - Nothing else leaves. +- State is files in the machine, databases included, reached through the shell; a snapshot captures all of it. +- State leaves only on purpose: the answer on stdout, an exported snapshot or checkout. ### Observability -- eBPF records what the model's processes do: which programs they start, which files they read, and each request to the engine. -- Every action has a cause. - The tracer is keyed by cgroup, so each action is attributed to the command that caused it, however many processes that command spawned. -- The log holds the machine's records, three per call, outside the machine. - The operator reads it from the CLI, live during a job and after. -- Cost per call is a first-release measurement. +- eBPF records which programs start, which files are read, and each request to the engine. +- Keyed by cgroup: each action is traced to the command that caused it, however many processes it spawned. +- The log holds each boot's records, in order: + its report; per call an intent, a decision, and a witness if allowed; its exit. +- The console reads it live, during a job and after.