diff --git a/CODE.md b/CODE.md index 8b45aa9..f4412a5 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, 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? -- 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. +- 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 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. # Vocabulary @@ -33,42 +33,52 @@ 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. | | -| 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. | | +| 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, 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. | | -| 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**. | | +| 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. | | +| 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. | | -| 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. | | -| 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. | | -| observer | eBPF keyed by cgroup, outside the model's reach. | | -| 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. | | -| ring | A privilege layer: model processes; harness and observer; host. | | +| 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 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` | +| 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 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, 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 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, `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 (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** 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. | | +| 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 @@ -100,13 +110,13 @@ 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, 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. # 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 349fd84..2ac215f 100644 --- a/README.md +++ b/README.md @@ -6,90 +6,77 @@ cead (Irish: permission; "kyad")

-cead is an agent harness built as a microVM: a userspace whose user is a model. -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 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. - -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. - -Three contracts; everything between two lines is swappable. - -| Line | Contract | +- **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 | |---|---| -| backend ↔ guest | boot protocol and virtio | +| 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) - [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://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) + ## 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. - 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. -- 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 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. +- **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 declaration is one file that names a machine: kernel, task image, policy, backend, and model endpoint. -Two ways to run it: +A **manifest** is one file that names a machine: kernel, task image, policy, VMM, model (weights, engine). -- `cead` boots the machine the declaration 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. +- `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. -A query is the length of a commit message; anything longer is a file in the machine for the model to read. +What a job does, from manifest to first command: -What a run does, from declaration 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. -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 model endpoint. -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 @@ -99,86 +86,77 @@ 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 | 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 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 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 run | scale-out: N machines from one declaration | -| 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 | - -- 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 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. -- 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. - API keys, the grader and the log stay on the host. - -### Hardware - -Two backends boot the same guest and leave the same evidence: Firecracker on Linux, Virtualization.framework on macOS. -The host needs a hypervisor and nothing else. +- **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, through a proxy, for inference and for 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 step. - 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. -- 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. - 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. -- Finish. - `finish` ends a process with its answer; when the root process finishes, the run 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 run'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 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 operator reads it from the CLI, live during a run and after. -- Cost per command 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. diff --git a/spec/cead.cfg b/spec/cead.cfg new file mode 100644 index 0000000..7e085b5 --- /dev/null +++ b/spec/cead.cfg @@ -0,0 +1,38 @@ +CONSTANTS + 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 + +INVARIANTS + TypeOK + IntentFirst + DenyNeverRuns + OnlyMachine + ExecutedOnce + Unambiguous + FinishHonest + Complete + ReportFirst + Rooted + OneOutcome + OnProcessors + WithinMeter + Attenuated + KillReach + +PROPERTIES + LogOnlyGrows + BootEnds + +CHECK_DEADLOCK FALSE diff --git a/spec/cead.tla b/spec/cead.tla new file mode 100644 index 0000000..0f14130 --- /dev/null +++ b/spec/cead.tla @@ -0,0 +1,495 @@ +-------------------------------- MODULE cead -------------------------------- +(***************************************************************************) +(* cead as a system. *) +(* 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. *) +(* 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. *) +(* 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, 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 + 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, 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", "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 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", "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 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 processes + transit, \* every record sent: each can be lost, delayed, reordered, duplicated + log \* held outside the machine: a set of records + +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, 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. +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.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" + +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 *) + +Init == + /\ machine = [b \in Boots |-> "off"] + /\ 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 |-> <<>>] + /\ job = [b \in Boots |-> b] + /\ snapshots = {} + /\ transit = {} + /\ log = {} + +\* 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] + /\ 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), 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. +BootFrom(b, s, o) == + /\ b # Root + /\ machine[b] = "off" + /\ o = "recovery" => Unknown(s.boot) + /\ 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 runs. +\* Nothing runs on a boot the log has not heard of. +Start(b) == + /\ machine[b] = "booting" + /\ Logged(b, 1) + /\ machine' = [machine EXCEPT ![b] = "up"] + /\ pending' = [pending EXCEPT ![b] = NoRecord] + /\ UNCHANGED <> + +\* 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" + /\ \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], 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. +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 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") + +\* The log has the exit record: the machine is gone. +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(b) == + /\ machine[b] \in {"booting", "up", "exiting"} + /\ machine' = [machine EXCEPT ![b] = "evicted"] + /\ pending' = [pending EXCEPT ![b] = NoRecord] + /\ 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 *) +(* 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 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. +Arrive(r) == + /\ IF r.type = "report" + THEN /\ r.key = "processor" + /\ r.body = "recovery" => + /\ ~LoggedType(r.from, 0, "exit") + /\ ~Recovered(r.from) + 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 + \/ \E b \in Boots, s \in snapshots, o \in {"fork", "recovery"} : BootFrom(b, s, o) + \/ \E b \in Boots : + \/ 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)) + +----------------------------------------------------------------------------- +(* Properties *) + +TypeOK == + /\ 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..MaxId, 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 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 b \in Boots : \A k \in 1..Len(executed[b]) : + Decision(executed[b][k].cmd) = "allow" + +\* 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] = "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)) + +\* 7. Each call is executed at most once on a boot. +ExecutedOnce == + \A b \in Boots : \A j, k \in 1..Len(executed[b]) : + j # k => executed[b][j].id # executed[b][k].id + +\* 8. No boot signs two different records for one place in its hash chain, +\* so each chain gives one order. +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 root process ended its turn: +\* it was not cut off. +FinishHonest == + \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. +Complete == + \A x \in log : + (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 == \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. +Rooted == + \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.from, 0, "exit") + /\ \A x, y \in Boots : + (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