ms2k/lazaret
SHA256
Watch
0
Code Releases 3 Activity

Confine verification tooling to current repository checks

Browse source
This commit is contained in:
ms2k 2026-07-14 02:17:49 +09:00
commit c738d92f01
21 changed files with 798 additions and 2926 deletions
Download patch file Download diff file Expand all files Collapse all files

76
.clippy.toml
View file

@ -1,44 +1,42 @@
# Generated from support/process-safety.toml; do not edit.
disallowed-types = [
{ path = "std::process::Child", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "std::process::Command", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "tokio::process::Child", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "tokio::process::Command", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "std::process::Child", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "std::process::Command", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "tokio::process::Child", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "tokio::process::Command", reason = "low-level process control requires an explicitly exempted audited boundary" },
]
disallowed-methods = [
{ path = "libc::clone", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "libc::execve", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "libc::execveat", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "libc::fork", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "libc::posix_spawn", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "libc::sigaction", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "libc::signal", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "libc::vfork", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "libc::wait", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "libc::wait4", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "libc::waitid", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "libc::waitpid", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "nix::sys::signal::sigaction", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "nix::sys::wait::wait", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "nix::sys::wait::waitid", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "nix::sys::wait::waitpid", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "nix::unistd::execve", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "nix::unistd::execveat", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "nix::unistd::fork", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "nix::unistd::vfork", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "rustix::process::kill_process", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "rustix::process::kill_process_group", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "rustix::process::pidfd_open", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "rustix::process::pidfd_send_signal", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "rustix::process::waitid", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "rustix::process::waitpid", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "std::process::Child::kill", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "std::process::Child::try_wait", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "std::process::Child::wait", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "std::process::Child::wait_with_output", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "std::process::Command::output", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "std::process::Command::spawn", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "std::process::Command::status", reason = "process control is confined to the reviewed Lazaret spawn/reap broker" },
{ path = "libc::clone", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "libc::execve", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "libc::execveat", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "libc::fork", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "libc::posix_spawn", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "libc::sigaction", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "libc::signal", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "libc::vfork", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "libc::wait", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "libc::wait4", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "libc::waitid", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "libc::waitpid", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "nix::sys::signal::sigaction", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "nix::sys::wait::wait", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "nix::sys::wait::waitid", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "nix::sys::wait::waitpid", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "nix::unistd::execve", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "nix::unistd::execveat", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "nix::unistd::fork", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "nix::unistd::vfork", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "rustix::process::kill_process", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "rustix::process::kill_process_group", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "rustix::process::pidfd_open", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "rustix::process::pidfd_send_signal", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "rustix::process::waitid", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "rustix::process::waitpid", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "std::process::Child::kill", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "std::process::Child::try_wait", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "std::process::Child::wait", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "std::process::Child::wait_with_output", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "std::process::Command::output", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "std::process::Command::spawn", reason = "low-level process control requires an explicitly exempted audited boundary" },
{ path = "std::process::Command::status", reason = "low-level process control requires an explicitly exempted audited boundary" },
]

11
docs/development.md
View file

@ -1,11 +0,0 @@
# Development and verification
The Cargo workspace separates shared production logic from process entry points. `lazaret-core` is the initial library boundary. The `lazaret` Client, `lazaret-host-coordinator`, `lazaret-runtime-supervisor`, `lazaret-network-sidecar`, and `lazaret-escalation-client` executables are thin binary packages; process behavior belongs in libraries so it can be verified without invoking private binary internals.
`support/work-packages.toml` is the dependency authority. `support/model-refinements.toml` assigns every modeled action and configured property to production packages and verification levels. `support/external-tools.toml` fixes the baseline host and tool contracts, including exact kernel qualification records and whether an unavailable capability fails or skips a level. `support/process-safety.toml` pins dependency source identities, features, and reviewed process APIs and registers the compiler and exercised-path syscall checks for the exclusive spawn/reap broker boundary. `docs/implementation-dependencies.md`, `docs/host-support.md`, and `.clippy.toml` are generated registry outputs.
Run `tools/verify-v1`, `tools/verify-v2`, `tools/verify-v3`, `tools/verify-v4`, or `tools/verify-v5`. Each higher level includes the lower levels. V1 is host-local and includes format, Clippy, tests, dependency policy, registry drift, and both TLC models. Physical suites register commands in `support/integration-tests.toml`; an empty level is an explicit skip. A registered scenario may skip only when every missing capability has `policy = "skip"` in the external-tool manifest.
Normal verification is offline: Cargo receives `--offline` and cargo-deny receives `--frozen`. `tools/dev refresh-advisories` is the explicit online operation that updates the local RustSec database and then verifies advisories offline. Every level audits the all-feature dependency source checksums, versions, enabled features, reviewed process APIs, generated compiler policy, and unauthorized lint exemptions. V2 registers optional `strace` cases for exact exercised binary paths; a missing tracer skips those cases, while an observed extra exec, process creation, wait, or `SIGCHLD` mutation fails. Dynamic tracing does not claim coverage of unexercised paths.
Run `tools/dev generate` after changing the work-package, external-tool, or process-safety registry. `tools/dev generate --check` fails when either committed generated view differs.

436
docs/host-support.md
View file

@ -1,436 +0,0 @@
# Host support and process-safety registry
Generated from `support/external-tools.toml` and `support/process-safety.toml`; do not edit this file directly.
## Pidfs host support
- Contract: `pidfs-process-identity-v1`
- Platform floor: `linux-x86_64` kernel `6.9` or newer
- Runtime refusal: `fail-before-generation`
- Unavailable verifier behavior: `skip`
- Smoke claim: `current-boot-smoke-only` cached only by `boot_id`
- Smoke bounds: one attempt per step, `5000` ms per step, `60000` ms total, `5000` ms cleanup
- Positive support: unavailable until IP-03 implements an exact running-build matcher and the smoke runner
The smoke steps are bounded observations and never qualify source or build provenance:
1. `linux-x86_64-kernel-floor`
1. `pidfd-operations`
1. `pidfs-magic`
1. `concurrent-same-process-identity`
1. `last-close-live-reopen-identity`
1. `simultaneous-process-distinct-inode`
1. `stale-handle-cannot-affect-live-peer`
1. `exit-reap-drop-all-later-process-non-reuse`
## Qualified kernel builds
| ID | Kind | Release | Source commit | Build image SHA-256 |
| --- | --- | --- | --- | --- |
| `upstream-linux-6.9.0-x86_64` | upstream | `6.9.0` | `a38297e3fb012ddfa7ce0321a7e5a8daeb1872b6` | `e85edb5da3dc18295f05baeb38ff019a6621c1cac2e6ac81b99e14450c72d7fc` |
## Process-safety audit
Policy `causal-child-acquisition-v1` pins 13 dependency source/version/feature/API-review records, generates compiler-resolved disallowed type/method lints, and registers `process-safety-baseline-exercised-paths` as V2 exercised-path tracing.
The dedicated `lazaret-process-broker` boundary is `unimplemented` and no lint exemption is authorized. Dynamic coverage is `registered-exercised-paths-only`; it does not claim unexercised-path coverage.
## Complete registered data
Every authoritative host-qualification and process-safety field is reproduced below so generated-view drift remains complete.
```json
{
"host_capabilities": [
{
"diagnostic": "Physical and composition suites currently support Linux x86_64.",
"id": "linux-x86_64",
"levels": [
"V2",
"V3",
"V4",
"V5"
],
"policy": "skip",
"probe": "linux-x86_64"
},
{
"diagnostic": "Linux x86-64 kernel 6.9 or newer is required; Linux 6.8 is unsupported for pidfs process identity.",
"id": "kernel",
"levels": [
"V2",
"V3",
"V4",
"V5"
],
"minimum": "6.9",
"policy": "skip",
"probe": "kernel-at-least"
},
{
"contract": "pidfs-process-identity-v1",
"diagnostic": "PidfsHostSupportProbe execution is owned by IP-03; this scaffold cannot claim host support from a version string or manifest record.",
"id": "pidfs-host-support",
"levels": [
"V2",
"V3",
"V4",
"V5"
],
"policy": "skip",
"probe": "registered-host-support"
}
],
"host_probe": [
{
"attempts_per_step": 1,
"cache_key": "boot_id",
"cleanup_timeout_ms": 5000,
"id": "pidfs-host-support-probe-v1",
"owner": "IP-03",
"result_claim": "bounded-current-boot-observations",
"step_timeout_ms": 5000,
"steps": [
"linux-x86_64-kernel-floor",
"pidfd-operations",
"pidfs-magic",
"concurrent-same-process-identity",
"last-close-live-reopen-identity",
"simultaneous-process-distinct-inode",
"stale-handle-cannot-affect-live-peer",
"exit-reap-drop-all-later-process-non-reuse"
],
"total_timeout_ms": 60000
}
],
"kernel_qualification": [
{
"acquisition_result_sha256": "867492f65ffd473733544626c032957143f40d040e1a4e8e1e82bf9e4bca6cc3",
"architecture": "x86_64",
"build_config_sha256": "7db4d48deb650052df60273c7f2c2d228c981db4d6f76b8eb929a9e120d7283a",
"build_image_sha256": "e85edb5da3dc18295f05baeb38ff019a6621c1cac2e6ac81b99e14450c72d7fc",
"id": "upstream-linux-6.9.0-x86_64",
"kind": "upstream",
"pidfs_inode_semantics": "boot-monotonic-u64",
"probe_binary_sha256": "040a84f2b06ae73671c262016c649fe21e3fb21fad89cea3d6d76f8d7436648f",
"release": "6.9.0",
"reuse_result_sha256": "b8491adc9c0fd4509ec94a99d03835842f7f92ca6d5baad8f6589a7f3c49517f",
"source_archive_sha256": "24fa01fb989c7a3e28453f117799168713766e119c5381dac30115f18f268149",
"source_commit": "a38297e3fb012ddfa7ce0321a7e5a8daeb1872b6",
"source_ref": "v6.9",
"source_signer_fingerprint": "647F28654894E3BD457199BE38DBBDC86092693E",
"status": "qualified"
}
],
"pidfs_host_support": {
"bounded_claim": "current-boot-smoke-only",
"diagnostic_kernel": "LZ-HOST-PIDFS-KERNEL: PidfsProcessIdentityV1 requires Linux x86-64 kernel 6.9 or newer; Linux 6.8 is unsupported even with a partial pidfs backport.",
"diagnostic_platform": "LZ-HOST-PIDFS-PLATFORM: PidfsProcessIdentityV1 requires Linux x86-64.",
"diagnostic_qualification": "LZ-HOST-PIDFS-QUALIFICATION: the running kernel build has no exact qualified source/build record.",
"diagnostic_smoke": "LZ-HOST-PIDFS-SMOKE: the bounded per-boot pidfs support smoke failed; no runtime resource or durable generation may be created.",
"id": "pidfs-process-identity-v1",
"minimum_kernel": "6.9",
"platform": "linux-x86_64",
"probe": "pidfs-host-support-probe-v1",
"qualification_ids": [
"upstream-linux-6.9.0-x86_64"
],
"runtime_failure_policy": "fail-before-generation",
"verifier_unavailable_policy": "skip"
},
"process_safety": {
"policy": {
"broker_crate": "lazaret-process-broker",
"broker_state": "unimplemented",
"completion_owner": "IP-03",
"disallowed_methods": [
"libc::clone",
"libc::execve",
"libc::execveat",
"libc::fork",
"libc::posix_spawn",
"libc::sigaction",
"libc::signal",
"libc::vfork",
"libc::wait",
"libc::wait4",
"libc::waitid",
"libc::waitpid",
"nix::sys::signal::sigaction",
"nix::sys::wait::wait",
"nix::sys::wait::waitid",
"nix::sys::wait::waitpid",
"nix::unistd::execve",
"nix::unistd::execveat",
"nix::unistd::fork",
"nix::unistd::vfork",
"rustix::process::kill_process",
"rustix::process::kill_process_group",
"rustix::process::pidfd_open",
"rustix::process::pidfd_send_signal",
"rustix::process::waitid",
"rustix::process::waitpid",
"std::process::Child::kill",
"std::process::Child::try_wait",
"std::process::Child::wait",
"std::process::Child::wait_with_output",
"std::process::Command::output",
"std::process::Command::spawn",
"std::process::Command::status"
],
"disallowed_types": [
"std::process::Child",
"std::process::Command",
"tokio::process::Child",
"tokio::process::Command"
],
"dynamic_coverage": "registered-exercised-paths-only",
"dynamic_scenario": "process-safety-baseline-exercised-paths",
"forbidden_syscall_patterns": [
"^clone3?\\(",
"^execveat\\(",
"^fork\\(",
"^vfork\\(",
"^wait4\\(",
"^waitid\\(",
"^rt_sigaction\\(SIGCHLD,"
],
"id": "causal-child-acquisition-v1",
"lint_allow_paths": [],
"lint_config": ".clippy.toml",
"production_roots": [
"crates"
],
"trace_expression": "process,wait4,waitid,rt_sigaction"
},
"runtime_dependency": [
{
"checksum": "0fa961b519f0b462e3a3b4a34b64d119eeaca1d59af726fe450bbba07a9fc0a1",
"features": [],
"name": "cobs",
"reviewed_process_apis": [],
"version": "0.3.0"
},
{
"checksum": "ef1a6892d9eef45c8fa6b9e0086428a2cca8491aca8f787c534a3d6d0bcb3ced",
"features": [
"alloc"
],
"name": "embedded-io",
"reviewed_process_apis": [],
"version": "0.4.0"
},
{
"checksum": "edd0f118536f44f5ccd48bcb8b111bdc3de888b58c74639dfb034a357d0f206d",
"features": [
"alloc"
],
"name": "embedded-io",
"reviewed_process_apis": [],
"version": "0.6.1"
},
{
"checksum": "6764c3b5dd454e283a30e6dfe78e9b31096d9e32036b5d1eaac7a6119ccb9a24",
"features": [
"alloc",
"use-std"
],
"name": "postcard",
"reviewed_process_apis": [],
"version": "1.1.3"
},
{
"checksum": "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934",
"features": [
"default",
"proc-macro"
],
"name": "proc-macro2",
"reviewed_process_apis": [],
"version": "1.0.106"
},
{
"checksum": "dfbc457d0c7a0759a614551b11a6409e5951f6c7537be1f1b7682b9ae9230368",
"features": [
"default",
"proc-macro"
],
"name": "quote",
"reviewed_process_apis": [],
"version": "1.0.46"
},
{
"checksum": "9a8e94ea7f378bd32cbbd37198a4a91436180c5bb472411e48b5ec2e2124ae9e",
"features": [
"alloc",
"default",
"derive",
"serde_derive",
"std"
],
"name": "serde",
"reviewed_process_apis": [],
"version": "1.0.228"
},
{
"checksum": "41d385c7d4ca58e59fc732af25c3983b67ac852c1a25000afe1175de458b67ad",
"features": [
"alloc",
"result",
"std"
],
"name": "serde_core",
"reviewed_process_apis": [],
"version": "1.0.228"
},
{
"checksum": "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79",
"features": [
"default"
],
"name": "serde_derive",
"reviewed_process_apis": [],
"version": "1.0.228"
},
{
"checksum": "1b9ae57f904213ebb649ce6895b8a66c66f0203b9319718f69a5612a065b1422",
"features": [
"clone-impls",
"default",
"derive",
"parsing",
"printing",
"proc-macro"
],
"name": "syn",
"reviewed_process_apis": [],
"version": "2.0.118"
},
{
"checksum": "4288b5bcbc7920c07a1149a35cf9590a2aa808e0bc1eafaade0b80947865fbc4",
"features": [],
"name": "thiserror",
"reviewed_process_apis": [],
"version": "2.0.18"
},
{
"checksum": "ebc4ee7f67670e9b64d05fa4253e753e016c6c95ff35b89b7941d6b856dec1d5",
"features": [],
"name": "thiserror-impl",
"reviewed_process_apis": [],
"version": "2.0.18"
},
{
"checksum": "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75",
"features": [],
"name": "unicode-ident",
"reviewed_process_apis": [],
"version": "1.0.24"
}
],
"schema": 2,
"trace_case": [
{
"args": [],
"binary": "lazaret",
"expected_exit_code": 0,
"initial_execve_count": 1
},
{
"args": [],
"binary": "lazaret-escalation-client",
"expected_exit_code": 0,
"initial_execve_count": 1
},
{
"args": [],
"binary": "lazaret-host-coordinator",
"expected_exit_code": 0,
"initial_execve_count": 1
},
{
"args": [],
"binary": "lazaret-network-sidecar",
"expected_exit_code": 0,
"initial_execve_count": 1
},
{
"args": [],
"binary": "lazaret-runtime-supervisor",
"expected_exit_code": 0,
"initial_execve_count": 1
}
]
},
"process_trace_capability": {
"args": [
"--version"
],
"diagnostic": "Install strace 6.x or newer to run the registered final-binary exercised-path syscall cases.",
"id": "strace",
"levels": [
"V2",
"V3",
"V4",
"V5"
],
"policy": "skip",
"program": "strace",
"version_pattern": "^strace -- version [6-9]\\.|^strace -- version [1-9][0-9]\\."
},
"process_trace_scenario": {
"capabilities": [
"linux-x86_64",
"strace"
],
"command": [
"tools/dev",
"process-audit",
"--dynamic"
],
"level": "V2",
"name": "process-safety-baseline-exercised-paths"
},
"workspace_lints": {
"clippy": {
"all": {
"level": "deny",
"priority": -1
},
"disallowed_methods": "deny",
"disallowed_types": "deny",
"pedantic": {
"level": "deny",
"priority": -1
}
},
"rust": {
"unsafe_code": "forbid",
"unused": {
"level": "deny",
"priority": -1
}
}
},
"workspace_member_lints": {
"crates/lazaret-client": {
"workspace": true
},
"crates/lazaret-core": {
"workspace": true
},
"crates/lazaret-escalation-client": {
"workspace": true
},
"crates/lazaret-host-coordinator": {
"workspace": true
},
"crates/lazaret-network-sidecar": {
"workspace": true
},
"crates/lazaret-runtime-supervisor": {
"workspace": true
}
}
}
```

159
docs/implementation-dependencies.md
View file

@ -1,159 +0,0 @@
# Implementation dependencies
Generated from `support/work-packages.toml`; do not edit this file directly.
| Package | Deliverable | Depends on | Verification |
| --- | --- | --- | --- |
| `IP-00` | Repository scaffold and verification | — | V1, V2, V3, V4, V5 |
| `IP-01` | Typed schema and protocol records | `IP-00` | V1 |
| `IP-02` | Trusted-host configuration | `IP-00`, `IP-01` | V1, V2 |
| `IP-03` | Linux primitives | `IP-00`, `IP-01` | V1, V2 |
| `IP-04` | Ignored-workspace contract | `IP-00` | V1, V2, V5 |
| `IP-10` | Domain Store | `IP-01`, `IP-02`, `IP-03` | V1, V2, V4 |
| `IP-11` | Storage Catalog | `IP-01`, `IP-02`, `IP-03` | V1, V2, V4 |
| `IP-12` | OCI transport and layer preparer | `IP-02`, `IP-03`, `IP-11` | V1, V2, V4 |
| `IP-13` | State Anchor | `IP-02`, `IP-03`, `IP-10`, `IP-11`, `IP-12` | V1, V2, V4 |
| `IP-14` | Derived network policy | `IP-01`, `IP-02` | V1 |
| `IP-15` | Protocol cryptography and codecs | `IP-01`, `IP-02`, `IP-03` | V1, V2 |
| `IP-16` | OCI specification and runsc command builder | `IP-01`, `IP-02`, `IP-03` | V1 |
| `IP-20` | Ignored-workspace router and Git Sentry | `IP-02`, `IP-03`, `IP-04`, `IP-10` | V1, V2, V4, V5 |
| `IP-21` | Runtime Supervisor and runsc ownership | `IP-03`, `IP-13`, `IP-16` | V2, V3, V4 |
| `IP-22` | Network installation and connectivity helper | `IP-03`, `IP-10`, `IP-14`, `IP-21` | V2, V3, V4 |
| `IP-23` | Host-private control face | `IP-02`, `IP-10`, `IP-15` | V1, V2 |
| `IP-24` | Escalation mailbox and execution | `IP-03`, `IP-10`, `IP-15`, `IP-23` | V1, V2, V3, V4 |
| `IP-30` | Core Host Coordinator lifecycle | `IP-10`, `IP-11`, `IP-12`, `IP-13`, `IP-14`, `IP-15`, `IP-16`, `IP-21`, `IP-22`, `IP-23` | V1, V2, V3 |
| `IP-31` | Non-interactive Client CLI | `IP-02`, `IP-16`, `IP-23`, `IP-30` | V1, V3 |
| `IP-40` | Minimal non-interactive runtime slice | `IP-30`, `IP-31` | V3 |
| `IP-32` | Recovery and prepared-artifact GC | `IP-30`, `IP-40` | V1, V2, V4 |
| `IP-33` | Session Terminal engine | `IP-10`, `IP-21`, `IP-23`, `IP-30`, `IP-40` | V1, V2, V4 |
| `IP-34` | Interactive Client CLI | `IP-31`, `IP-33` | V1, V3 |
| `IP-35` | State inspection and reset | `IP-10`, `IP-13`, `IP-20`, `IP-32` | V1, V2, V4 |
| `IP-41` | Workspace, Git, and persistence slice | `IP-20`, `IP-32`, `IP-40` | V3, V5 |
| `IP-42` | Interactive and multi-session slice | `IP-33`, `IP-34`, `IP-40` | V3 |
| `IP-43` | Host-escalation slice | `IP-24`, `IP-34`, `IP-42` | V3 |
| `IP-44` | Durability and hostile-failure gate | `IP-32`, `IP-35`, `IP-40`, `IP-41`, `IP-42`, `IP-43` | V4 |
| `IP-45` | Release qualification | `IP-44` | V5 |
```mermaid
graph TD
IP_00["IP-00 Repository scaffold and verification"]
IP_01["IP-01 Typed schema and protocol records"]
IP_02["IP-02 Trusted-host configuration"]
IP_03["IP-03 Linux primitives"]
IP_04["IP-04 Ignored-workspace contract"]
IP_10["IP-10 Domain Store"]
IP_11["IP-11 Storage Catalog"]
IP_12["IP-12 OCI transport and layer preparer"]
IP_13["IP-13 State Anchor"]
IP_14["IP-14 Derived network policy"]
IP_15["IP-15 Protocol cryptography and codecs"]
IP_16["IP-16 OCI specification and runsc command builder"]
IP_20["IP-20 Ignored-workspace router and Git Sentry"]
IP_21["IP-21 Runtime Supervisor and runsc ownership"]
IP_22["IP-22 Network installation and connectivity helper"]
IP_23["IP-23 Host-private control face"]
IP_24["IP-24 Escalation mailbox and execution"]
IP_30["IP-30 Core Host Coordinator lifecycle"]
IP_31["IP-31 Non-interactive Client CLI"]
IP_40["IP-40 Minimal non-interactive runtime slice"]
IP_32["IP-32 Recovery and prepared-artifact GC"]
IP_33["IP-33 Session Terminal engine"]
IP_34["IP-34 Interactive Client CLI"]
IP_35["IP-35 State inspection and reset"]
IP_41["IP-41 Workspace, Git, and persistence slice"]
IP_42["IP-42 Interactive and multi-session slice"]
IP_43["IP-43 Host-escalation slice"]
IP_44["IP-44 Durability and hostile-failure gate"]
IP_45["IP-45 Release qualification"]
IP_00 --> IP_01
IP_00 --> IP_02
IP_01 --> IP_02
IP_00 --> IP_03
IP_01 --> IP_03
IP_00 --> IP_04
IP_01 --> IP_10
IP_02 --> IP_10
IP_03 --> IP_10
IP_01 --> IP_11
IP_02 --> IP_11
IP_03 --> IP_11
IP_02 --> IP_12
IP_03 --> IP_12
IP_11 --> IP_12
IP_02 --> IP_13
IP_03 --> IP_13
IP_10 --> IP_13
IP_11 --> IP_13
IP_12 --> IP_13
IP_01 --> IP_14
IP_02 --> IP_14
IP_01 --> IP_15
IP_02 --> IP_15
IP_03 --> IP_15
IP_01 --> IP_16
IP_02 --> IP_16
IP_03 --> IP_16
IP_02 --> IP_20
IP_03 --> IP_20
IP_04 --> IP_20
IP_10 --> IP_20
IP_03 --> IP_21
IP_13 --> IP_21
IP_16 --> IP_21
IP_03 --> IP_22
IP_10 --> IP_22
IP_14 --> IP_22
IP_21 --> IP_22
IP_02 --> IP_23
IP_10 --> IP_23
IP_15 --> IP_23
IP_03 --> IP_24
IP_10 --> IP_24
IP_15 --> IP_24
IP_23 --> IP_24
IP_10 --> IP_30
IP_11 --> IP_30
IP_12 --> IP_30
IP_13 --> IP_30
IP_14 --> IP_30
IP_15 --> IP_30
IP_16 --> IP_30
IP_21 --> IP_30
IP_22 --> IP_30
IP_23 --> IP_30
IP_02 --> IP_31
IP_16 --> IP_31
IP_23 --> IP_31
IP_30 --> IP_31
IP_30 --> IP_40
IP_31 --> IP_40
IP_30 --> IP_32
IP_40 --> IP_32
IP_10 --> IP_33
IP_21 --> IP_33
IP_23 --> IP_33
IP_30 --> IP_33
IP_40 --> IP_33
IP_31 --> IP_34
IP_33 --> IP_34
IP_10 --> IP_35
IP_13 --> IP_35
IP_20 --> IP_35
IP_32 --> IP_35
IP_20 --> IP_41
IP_32 --> IP_41
IP_40 --> IP_41
IP_33 --> IP_42
IP_34 --> IP_42
IP_40 --> IP_42
IP_24 --> IP_43
IP_34 --> IP_43
IP_42 --> IP_43
IP_32 --> IP_44
IP_35 --> IP_44
IP_40 --> IP_44
IP_41 --> IP_44
IP_42 --> IP_44
IP_43 --> IP_44
IP_44 --> IP_45
```

196
support/external-tools.toml
View file

@ -1,196 +0,0 @@
schema = 2
levels = ["V1", "V2", "V3", "V4", "V5"]
[pidfs_host_support]
id = "pidfs-process-identity-v1"
platform = "linux-x86_64"
minimum_kernel = "6.9"
probe = "pidfs-host-support-probe-v1"
qualification_ids = ["upstream-linux-6.9.0-x86_64"]
runtime_failure_policy = "fail-before-generation"
verifier_unavailable_policy = "skip"
bounded_claim = "current-boot-smoke-only"
diagnostic_platform = "LZ-HOST-PIDFS-PLATFORM: PidfsProcessIdentityV1 requires Linux x86-64."
diagnostic_kernel = "LZ-HOST-PIDFS-KERNEL: PidfsProcessIdentityV1 requires Linux x86-64 kernel 6.9 or newer; Linux 6.8 is unsupported even with a partial pidfs backport."
diagnostic_qualification = "LZ-HOST-PIDFS-QUALIFICATION: the running kernel build has no exact qualified source/build record."
diagnostic_smoke = "LZ-HOST-PIDFS-SMOKE: the bounded per-boot pidfs support smoke failed; no runtime resource or durable generation may be created."
[[host_probe]]
id = "pidfs-host-support-probe-v1"
owner = "IP-03"
cache_key = "boot_id"
result_claim = "bounded-current-boot-observations"
attempts_per_step = 1
step_timeout_ms = 5000
total_timeout_ms = 60000
cleanup_timeout_ms = 5000
steps = [
"linux-x86_64-kernel-floor",
"pidfd-operations",
"pidfs-magic",
"concurrent-same-process-identity",
"last-close-live-reopen-identity",
"simultaneous-process-distinct-inode",
"stale-handle-cannot-affect-live-peer",
"exit-reap-drop-all-later-process-non-reuse",
]
[[kernel_qualification]]
id = "upstream-linux-6.9.0-x86_64"
kind = "upstream"
architecture = "x86_64"
release = "6.9.0"
source_ref = "v6.9"
source_commit = "a38297e3fb012ddfa7ce0321a7e5a8daeb1872b6"
source_archive_sha256 = "24fa01fb989c7a3e28453f117799168713766e119c5381dac30115f18f268149"
source_signer_fingerprint = "647F28654894E3BD457199BE38DBBDC86092693E"
build_config_sha256 = "7db4d48deb650052df60273c7f2c2d228c981db4d6f76b8eb929a9e120d7283a"
build_image_sha256 = "e85edb5da3dc18295f05baeb38ff019a6621c1cac2e6ac81b99e14450c72d7fc"
probe_binary_sha256 = "040a84f2b06ae73671c262016c649fe21e3fb21fad89cea3d6d76f8d7436648f"
reuse_result_sha256 = "b8491adc9c0fd4509ec94a99d03835842f7f92ca6d5baad8f6589a7f3c49517f"
acquisition_result_sha256 = "867492f65ffd473733544626c032957143f40d040e1a4e8e1e82bf9e4bca6cc3"
pidfs_inode_semantics = "boot-monotonic-u64"
status = "qualified"
[[command]]
id = "python"
program = "python3"
args = ["--version"]
version_pattern = '^Python 3\.(1[1-9]|[2-9][0-9])\.'
policy = "fail"
levels = ["V1", "V2", "V3", "V4", "V5"]
diagnostic = "Python 3.11 or newer is required for repository verification."
[[command]]
id = "rustc"
program = "rustc"
args = ["--version"]
version_pattern = '^rustc 1\.90\.0 '
policy = "fail"
levels = ["V1", "V2", "V3", "V4", "V5"]
diagnostic = "Install the pinned Rust toolchain from rust-toolchain.toml."
[[command]]
id = "cargo"
program = "cargo"
args = ["--version"]
version_pattern = '^cargo 1\.90\.0 '
policy = "fail"
levels = ["V1", "V2", "V3", "V4", "V5"]
diagnostic = "Install the pinned Rust toolchain from rust-toolchain.toml."
[[command]]
id = "cargo-deny"
program = "cargo-deny"
args = ["--version"]
version_pattern = '^cargo-deny 0\.20\.2$'
policy = "fail"
levels = ["V1", "V2", "V3", "V4", "V5"]
diagnostic = "Install cargo-deny 0.20.2 with its locked dependency graph."
[[command]]
id = "git"
program = "git"
args = ["--version"]
version_pattern = '^git version 2\.'
policy = "fail"
levels = ["V1", "V2", "V3", "V4", "V5"]
diagnostic = "Git 2.x is required for generated-file drift checks."
[[command]]
id = "tlc"
program = "tlc"
args = ["-h"]
version_pattern = 'Version 2\.19 '
accepted_exit_codes = [0, 1]
policy = "fail"
levels = ["V1", "V2", "V3", "V4", "V5"]
diagnostic = "Install the TLC 2.19 launcher on PATH."
[[command]]
id = "runsc"
program = "runsc"
args = ["--version"]
version_pattern = '^runsc version release-20260622\.0\nspec: 1\.2\.1$'
policy = "skip"
levels = ["V3", "V4", "V5"]
diagnostic = "The selected composition is qualified on runsc release-20260622.0."
[[command]]
id = "fuse-overlayfs"
program = "fuse-overlayfs"
args = ["--version"]
version_pattern = '^fusermount3 version: 3\.18\.2\nfuse-overlayfs: version 1\.16\nFUSE library version 3\.18\.2\nusing FUSE kernel interface version 7\.45$'
policy = "skip"
levels = ["V2", "V3", "V4", "V5"]
diagnostic = "Install the qualified fuse-overlayfs 1.16 and FUSE 3.18.2 stack."
[[command]]
id = "slirp4netns"
program = "slirp4netns"
args = ["--version"]
version_pattern = '^slirp4netns version 1\.3\.1\ncommit: .+\nlibslirp: 4\.9\.1\nSLIRP_CONFIG_VERSION_MAX: 6\nlibseccomp: 2\.6\.0$'
policy = "skip"
levels = ["V2", "V3", "V4", "V5"]
diagnostic = "Install the qualified slirp4netns 1.3.1 and libslirp 4.9.1 stack."
[[command]]
id = "strace"
program = "strace"
args = ["--version"]
version_pattern = '^strace -- version [6-9]\.|^strace -- version [1-9][0-9]\.'
policy = "skip"
levels = ["V2", "V3", "V4", "V5"]
diagnostic = "Install strace 6.x or newer to run the registered final-binary exercised-path syscall cases."
[[feature]]
id = "linux-x86_64"
probe = "linux-x86_64"
policy = "skip"
levels = ["V2", "V3", "V4", "V5"]
diagnostic = "Physical and composition suites currently support Linux x86_64."
[[feature]]
id = "kernel"
probe = "kernel-at-least"
minimum = "6.9"
policy = "skip"
levels = ["V2", "V3", "V4", "V5"]
diagnostic = "Linux x86-64 kernel 6.9 or newer is required; Linux 6.8 is unsupported for pidfs process identity."
[[feature]]
id = "pidfs-host-support"
probe = "registered-host-support"
contract = "pidfs-process-identity-v1"
policy = "skip"
levels = ["V2", "V3", "V4", "V5"]
diagnostic = "PidfsHostSupportProbe execution is owned by IP-03; this scaffold cannot claim host support from a version string or manifest record."
[[feature]]
id = "user-namespaces"
probe = "user-namespace"
program = "unshare"
sysctl_path = "/proc/sys/user/max_user_namespaces"
policy = "skip"
levels = ["V2", "V3", "V4", "V5"]
diagnostic = "Enable functional unprivileged user namespace creation for physical runtime tests."
[[feature]]
id = "subordinate-ids"
probe = "subordinate-ids"
minimum_count = 65536
uidmap_program = "newuidmap"
gidmap_program = "newgidmap"
unshare_program = "unshare"
policy = "skip"
levels = ["V2", "V3", "V4", "V5"]
diagnostic = "Configure usable 65,536-ID subordinate UID/GID ranges and mapping helpers for the current user."
[[feature]]
id = "fuse-device"
probe = "open-character-device"
path = "/dev/fuse"
access = "read-write"
policy = "skip"
levels = ["V2", "V3", "V4", "V5"]
diagnostic = "Expose an openable read-write /dev/fuse device to run physical filesystem suites."

8
support/integration-tests.toml
View file

@ -1,8 +0,0 @@
schema = 1
levels = ["V2", "V3", "V4", "V5"]
[[scenarios]]
name = "process-safety-baseline-exercised-paths"
level = "V2"
command = ["tools/dev", "process-audit", "--dynamic"]
capabilities = ["linux-x86_64", "strace"]

165
support/model-refinements.toml
View file

@ -1,165 +0,0 @@
schema = 1
[[model]]
name = "Lazaret"
module = "docs/protocol/Lazaret.tla"
config = "docs/protocol/Lazaret.cfg"
action_aggregates = ["Next", "DomainServiceProgress", "RuntimePhysicalInterleaving", "RequestProgress"]
[[model]]
name = "PreparedLower"
module = "docs/protocol/PreparedLower.tla"
config = "docs/protocol/PreparedLower.cfg"
action_aggregates = ["Next"]
[[coverage]]
model = "Lazaret"
kind = "action"
symbols = ["StartNewDomain", "StartReadySession", "WaitForDomain", "RestartWaitingDomain", "AdvanceWaitingSession", "RejectConfigurationMismatch", "RegisterSession", "DisconnectSession"]
owners = ["IP-30", "IP-31"]
levels = ["V1", "V3"]
verifier = "Deterministic lifecycle adapters and the IP-40 cold-start slice"
[[coverage]]
model = "Lazaret"
kind = "action"
symbols = ["CreateTrustAnchor"]
owners = ["IP-23", "IP-30"]
levels = ["V2", "V3"]
verifier = "Credential/control physical tests and generation publication"
[[coverage]]
model = "Lazaret"
kind = "action"
symbols = ["StartRuntimeSupervisor", "LeasePreparedLower", "MountStateAnchor", "StartSidecar", "StartConnectivityHelper", "MarkNetworkReady", "ArmRuntimeCausalEdge", "StartSandbox", "PublishDomain"]
owners = ["IP-10", "IP-11", "IP-12", "IP-13", "IP-14", "IP-15", "IP-16", "IP-21", "IP-22", "IP-23", "IP-30"]
levels = ["V1", "V2", "V3"]
verifier = "Component tests, the IP-21 composition harness, and IP-40"
[[coverage]]
model = "Lazaret"
kind = "action"
symbols = ["BeginTeardown", "StopSandbox", "StopSidecar", "UnmountStateAnchor", "ReleasePreparedLowerLease", "GracefulSupervisorExit", "FinishTeardown"]
owners = ["IP-10", "IP-11", "IP-12", "IP-13", "IP-21", "IP-22", "IP-30"]
levels = ["V1", "V2", "V3"]
verifier = "Lifecycle adapters and IP-40 normal teardown"
[[coverage]]
model = "Lazaret"
kind = "action"
symbols = ["FailDomain", "HostCoordinatorTerminateUnresponsiveRuntime", "LeaseTeardownStopSandbox", "LeaseTeardownStopSidecar", "LeaseTeardownUnmountStateAnchor", "LeaseTeardownSupervisorExit", "ExternalReapStoppedSupervisorAfterHcLoss", "BootstrapRecoveryCoordinator", "BeginRecovery", "RecoverSandbox", "RecoverSidecar", "RecoverStateAnchor", "RecoverPreparedLowerLease", "FinishRecovery"]
owners = ["IP-21", "IP-22", "IP-32"]
levels = ["V2", "V4"]
verifier = "Causal-loss tests and the recovery failpoint matrix"
[[coverage]]
model = "Lazaret"
kind = "action"
symbols = ["HardLoseHostCoordinator", "HardLoseRuntimeSupervisor", "HardLoseAttachedRunsc", "HardLoseConnectivityHelper", "StopHostCoordinatorProcess", "ResumeHostCoordinatorProcess", "StopRuntimeSupervisorProcess", "ResumeRuntimeSupervisorProcess", "StopAttachedRunscProcess", "ResumeAttachedRunscProcess", "ObservePathMismatch", "RefusePathMismatchCleanup", "RefusePreparedLowerReclaim"]
owners = ["IP-11", "IP-12", "IP-13", "IP-21", "IP-22", "IP-32"]
levels = ["V2", "V4"]
verifier = "Physical mismatch, stop, loss, and hostile-failure cases"
[[coverage]]
model = "Lazaret"
kind = "action"
symbols = ["ReceiveEscalation", "AutoApprove", "QueuePrompt", "BeginPrompt", "DeveloperApprove", "DeveloperDeny", "StartHostExecution", "CompleteHostExecution", "TimeoutRequest", "CancelRequest", "FailHostExecution", "DeliverResult"]
owners = ["IP-15", "IP-24", "IP-33", "IP-34"]
levels = ["V1", "V2", "V3", "V4"]
verifier = "Protocol tests, the IP-43 slice, and hostile-loss cases"
[[coverage]]
model = "Lazaret"
kind = "invariant"
symbols = ["TypeOK", "DomainGenerationBounds", "RuntimeRoleIdentitySeparation", "GenerationScopedIdentitiesDistinct"]
owners = ["IP-01", "IP-10", "IP-14", "IP-15", "IP-30"]
levels = ["V1"]
verifier = "IP-01 strict schema-codec, malformed-version, record-invariant, and nominal identity tests plus later lifecycle state assertions"
[[coverage]]
model = "Lazaret"
kind = "invariant"
symbols = ["ConfigurationConfinement", "SandboxNamespaceIsolation", "OrderedNetworkStartup", "NetworkReadyBeforePublish"]
owners = ["IP-02", "IP-14", "IP-16", "IP-20", "IP-21", "IP-22", "IP-30"]
levels = ["V1", "V2", "V3"]
verifier = "Builders/codecs, physical isolation, and IP-40/IP-41"
[[coverage]]
model = "Lazaret"
kind = "invariant"
symbols = ["PublishedDomainsReady", "DomainLockLifetime", "RuntimeCausalEdgeArmedBeforeSandbox", "RuntimeCausalEdgeOwnerPresent", "SandboxRunningImpliesCoordinatorPresent", "PublishedRuntimeAuthorityPresent", "SupervisorLeaseConsistency", "RuntimeResourceOwnership", "CoordinatorPhysicalConsistency", "HostCoordinatorRequiresDomainOwnership", "NoVanishPresentRuntime", "StateAnchorOwnership", "HelperUnderSupervisor"]
owners = ["IP-10", "IP-13", "IP-21", "IP-22", "IP-30", "IP-32"]
levels = ["V1", "V2", "V3", "V4"]
verifier = "Lifecycle adapters, causal harnesses, and IP-44"
[[coverage]]
model = "Lazaret"
kind = "invariant"
symbols = ["ExclusiveBootstrapOwnership", "TeardownNotJoinable", "RegisteredSessionsConnected", "AttachedSessionsValid", "TerminalIsolation"]
owners = ["IP-23", "IP-30", "IP-31", "IP-33", "IP-34"]
levels = ["V1", "V2", "V3"]
verifier = "Control/session tests and IP-40/IP-42"
[[coverage]]
model = "Lazaret"
kind = "invariant"
symbols = ["AuthenticatedRequestsOnly", "RegisteredSessionIdentityUniqueness", "LiveRequestIdentityAuthorized", "DeveloperApprovalAuthenticated", "HostExecutionAuthorized", "AutoApprovalNoShell", "NoOrphanHostProcess", "ResultDeliveryStateConsistent"]
owners = ["IP-15", "IP-23", "IP-24", "IP-33", "IP-34"]
levels = ["V1", "V2", "V3", "V4"]
verifier = "Protocol tests, IP-43, and hostile-loss cases"
[[coverage]]
model = "Lazaret"
kind = "invariant"
symbols = ["OrderedLeaseTeardown", "DurableIntentBeforeSandboxReady", "DurableDecisionPublicationConsistent", "PathMismatchNotAdopted", "FailedDomainIsolation", "OrderedFailureRecovery", "MultiRoleDurableIntent", "PreparedLowerLeaseBeforeMount"]
owners = ["IP-10", "IP-11", "IP-12", "IP-13", "IP-21", "IP-22", "IP-30", "IP-32"]
levels = ["V1", "V2", "V4"]
verifier = "Transactional and failpoint tests plus IP-44"
[[coverage]]
model = "Lazaret"
kind = "property"
symbols = ["SessionEventuallyResolves", "RequestEventuallyResolves", "PromptEventuallyRestoresTerminal", "EmptyDomainEventuallyStops", "FailedDomainEventuallyRecovers"]
owners = ["IP-24", "IP-30", "IP-31", "IP-32", "IP-33", "IP-34"]
levels = ["V1", "V2", "V3", "V4"]
verifier = "Bounded progress tests, integrated slices, and TLC"
[[coverage]]
model = "Lazaret"
kind = "property"
symbols = ["LeaseLossUnmountRetainsPreparedLowerLease"]
owners = ["IP-10", "IP-11", "IP-13", "IP-21", "IP-30", "IP-32"]
levels = ["V2", "V4"]
verifier = "Lease-loss failpoints and TLC"
[[coverage]]
model = "PreparedLower"
kind = "action"
symbols = ["BeginPrepare", "CreateOwnedStage", "PublishArtifact", "RecoverOwnedStage", "ObserveForeignStage", "RefuseForeignStage"]
owners = ["IP-12", "IP-32"]
levels = ["V1", "V2", "V4"]
verifier = "Preparer publication, ownership, and recovery tests"
[[coverage]]
model = "PreparedLower"
kind = "action"
symbols = ["AcquireLease", "MountStateAnchor", "UnmountStateAnchor", "ReleaseLease"]
owners = ["IP-11", "IP-13", "IP-32"]
levels = ["V1", "V2", "V4"]
verifier = "Catalog and State Anchor lease lifecycle tests"
[[coverage]]
model = "PreparedLower"
kind = "action"
symbols = ["RequestGC", "PublishReplacementDuringGC", "ReclaimArtifact"]
owners = ["IP-11", "IP-12", "IP-32"]
levels = ["V1", "V2", "V4"]
verifier = "Concurrent publication and exact-owned reclamation tests"
[[coverage]]
model = "PreparedLower"
kind = "invariant"
symbols = ["TypeOK", "LeaseBindingConsistent", "MountedGenerationLeased", "LeasedArtifactPublished", "GCExcludesLeases", "ReplacementOnlyDuringGC", "ForeignStagePreserved", "OwnedStageRequiresIntent"]
owners = ["IP-11", "IP-12", "IP-13", "IP-32"]
levels = ["V1", "V2", "V4"]
verifier = "Catalog/preparer concurrency and recovery tests plus TLC"

184
support/process-safety.toml
View file

@ -1,184 +0,0 @@
schema = 2
[policy]
id = "causal-child-acquisition-v1"
broker_crate = "lazaret-process-broker"
broker_state = "unimplemented"
production_roots = ["crates"]
lint_config = ".clippy.toml"
lint_allow_paths = []
dynamic_scenario = "process-safety-baseline-exercised-paths"
dynamic_coverage = "registered-exercised-paths-only"
completion_owner = "IP-03"
trace_expression = "process,wait4,waitid,rt_sigaction"
forbidden_syscall_patterns = [
'^clone3?\(',
'^execveat\(',
'^fork\(',
'^vfork\(',
'^wait4\(',
'^waitid\(',
'^rt_sigaction\(SIGCHLD,',
]
disallowed_types = [
"std::process::Child",
"std::process::Command",
"tokio::process::Child",
"tokio::process::Command",
]
disallowed_methods = [
"libc::clone",
"libc::execve",
"libc::execveat",
"libc::fork",
"libc::posix_spawn",
"libc::sigaction",
"libc::signal",
"libc::vfork",
"libc::wait",
"libc::wait4",
"libc::waitid",
"libc::waitpid",
"nix::sys::signal::sigaction",
"nix::sys::wait::wait",
"nix::sys::wait::waitid",
"nix::sys::wait::waitpid",
"nix::unistd::execve",
"nix::unistd::execveat",
"nix::unistd::fork",
"nix::unistd::vfork",
"rustix::process::kill_process",
"rustix::process::kill_process_group",
"rustix::process::pidfd_open",
"rustix::process::pidfd_send_signal",
"rustix::process::waitid",
"rustix::process::waitpid",
"std::process::Child::kill",
"std::process::Child::try_wait",
"std::process::Child::wait",
"std::process::Child::wait_with_output",
"std::process::Command::output",
"std::process::Command::spawn",
"std::process::Command::status",
]
[[trace_case]]
binary = "lazaret"
args = []
expected_exit_code = 0
initial_execve_count = 1
[[trace_case]]
binary = "lazaret-escalation-client"
args = []
expected_exit_code = 0
initial_execve_count = 1
[[trace_case]]
binary = "lazaret-host-coordinator"
args = []
expected_exit_code = 0
initial_execve_count = 1
[[trace_case]]
binary = "lazaret-network-sidecar"
args = []
expected_exit_code = 0
initial_execve_count = 1
[[trace_case]]
binary = "lazaret-runtime-supervisor"
args = []
expected_exit_code = 0
initial_execve_count = 1
[[runtime_dependency]]
name = "cobs"
version = "0.3.0"
checksum = "0fa961b519f0b462e3a3b4a34b64d119eeaca1d59af726fe450bbba07a9fc0a1"
features = []
reviewed_process_apis = []
[[runtime_dependency]]
name = "embedded-io"
version = "0.4.0"
checksum = "ef1a6892d9eef45c8fa6b9e0086428a2cca8491aca8f787c534a3d6d0bcb3ced"
features = ["alloc"]
reviewed_process_apis = []
[[runtime_dependency]]
name = "embedded-io"
version = "0.6.1"
checksum = "edd0f118536f44f5ccd48bcb8b111bdc3de888b58c74639dfb034a357d0f206d"
features = ["alloc"]
reviewed_process_apis = []
[[runtime_dependency]]
name = "postcard"
version = "1.1.3"
checksum = "6764c3b5dd454e283a30e6dfe78e9b31096d9e32036b5d1eaac7a6119ccb9a24"
features = ["alloc", "use-std"]
reviewed_process_apis = []
[[runtime_dependency]]
name = "proc-macro2"
version = "1.0.106"
checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934"
features = ["default", "proc-macro"]
reviewed_process_apis = []
[[runtime_dependency]]
name = "quote"
version = "1.0.46"
checksum = "dfbc457d0c7a0759a614551b11a6409e5951f6c7537be1f1b7682b9ae9230368"
features = ["default", "proc-macro"]
reviewed_process_apis = []
[[runtime_dependency]]
name = "serde"
version = "1.0.228"
checksum = "9a8e94ea7f378bd32cbbd37198a4a91436180c5bb472411e48b5ec2e2124ae9e"
features = ["alloc", "default", "derive", "serde_derive", "std"]
reviewed_process_apis = []
[[runtime_dependency]]
name = "serde_core"
version = "1.0.228"
checksum = "41d385c7d4ca58e59fc732af25c3983b67ac852c1a25000afe1175de458b67ad"
features = ["alloc", "result", "std"]
reviewed_process_apis = []
[[runtime_dependency]]
name = "serde_derive"
version = "1.0.228"
checksum = "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79"
features = ["default"]
reviewed_process_apis = []
[[runtime_dependency]]
name = "syn"
version = "2.0.118"
checksum = "1b9ae57f904213ebb649ce6895b8a66c66f0203b9319718f69a5612a065b1422"
features = ["clone-impls", "default", "derive", "parsing", "printing", "proc-macro"]
reviewed_process_apis = []
[[runtime_dependency]]
name = "thiserror"
version = "2.0.18"
checksum = "4288b5bcbc7920c07a1149a35cf9590a2aa808e0bc1eafaade0b80947865fbc4"
features = []
reviewed_process_apis = []
[[runtime_dependency]]
name = "thiserror-impl"
version = "2.0.18"
checksum = "ebc4ee7f67670e9b64d05fa4253e753e016c6c95ff35b89b7941d6b856dec1d5"
features = []
reviewed_process_apis = []
[[runtime_dependency]]
name = "unicode-ident"
version = "1.0.24"
checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75"
features = []
reviewed_process_apis = []

175
support/work-packages.toml
View file

@ -1,175 +0,0 @@
schema = 1
[[package]]
id = "IP-00"
title = "Repository scaffold and verification"
depends_on = []
levels = ["V1", "V2", "V3", "V4", "V5"]
[[package]]
id = "IP-01"
title = "Typed schema and protocol records"
depends_on = ["IP-00"]
levels = ["V1"]
[[package]]
id = "IP-02"
title = "Trusted-host configuration"
depends_on = ["IP-00", "IP-01"]
levels = ["V1", "V2"]
[[package]]
id = "IP-03"
title = "Linux primitives"
depends_on = ["IP-00", "IP-01"]
levels = ["V1", "V2"]
[[package]]
id = "IP-04"
title = "Ignored-workspace contract"
depends_on = ["IP-00"]
levels = ["V1", "V2", "V5"]
[[package]]
id = "IP-10"
title = "Domain Store"
depends_on = ["IP-01", "IP-02", "IP-03"]
levels = ["V1", "V2", "V4"]
[[package]]
id = "IP-11"
title = "Storage Catalog"
depends_on = ["IP-01", "IP-02", "IP-03"]
levels = ["V1", "V2", "V4"]
[[package]]
id = "IP-12"
title = "OCI transport and layer preparer"
depends_on = ["IP-02", "IP-03", "IP-11"]
levels = ["V1", "V2", "V4"]
[[package]]
id = "IP-13"
title = "State Anchor"
depends_on = ["IP-02", "IP-03", "IP-10", "IP-11", "IP-12"]
levels = ["V1", "V2", "V4"]
[[package]]
id = "IP-14"
title = "Derived network policy"
depends_on = ["IP-01", "IP-02"]
levels = ["V1"]
[[package]]
id = "IP-15"
title = "Protocol cryptography and codecs"
depends_on = ["IP-01", "IP-02", "IP-03"]
levels = ["V1", "V2"]
[[package]]
id = "IP-16"
title = "OCI specification and runsc command builder"
depends_on = ["IP-01", "IP-02", "IP-03"]
levels = ["V1"]
[[package]]
id = "IP-20"
title = "Ignored-workspace router and Git Sentry"
depends_on = ["IP-02", "IP-03", "IP-04", "IP-10"]
levels = ["V1", "V2", "V4", "V5"]
[[package]]
id = "IP-21"
title = "Runtime Supervisor and runsc ownership"
depends_on = ["IP-03", "IP-13", "IP-16"]
levels = ["V2", "V3", "V4"]
[[package]]
id = "IP-22"
title = "Network installation and connectivity helper"
depends_on = ["IP-03", "IP-10", "IP-14", "IP-21"]
levels = ["V2", "V3", "V4"]
[[package]]
id = "IP-23"
title = "Host-private control face"
depends_on = ["IP-02", "IP-10", "IP-15"]
levels = ["V1", "V2"]
[[package]]
id = "IP-24"
title = "Escalation mailbox and execution"
depends_on = ["IP-03", "IP-10", "IP-15", "IP-23"]
levels = ["V1", "V2", "V3", "V4"]
[[package]]
id = "IP-30"
title = "Core Host Coordinator lifecycle"
depends_on = ["IP-10", "IP-11", "IP-12", "IP-13", "IP-14", "IP-15", "IP-16", "IP-21", "IP-22", "IP-23"]
levels = ["V1", "V2", "V3"]
[[package]]
id = "IP-31"
title = "Non-interactive Client CLI"
depends_on = ["IP-02", "IP-16", "IP-23", "IP-30"]
levels = ["V1", "V3"]
[[package]]
id = "IP-32"
title = "Recovery and prepared-artifact GC"
depends_on = ["IP-30", "IP-40"]
levels = ["V1", "V2", "V4"]
[[package]]
id = "IP-33"
title = "Session Terminal engine"
depends_on = ["IP-10", "IP-21", "IP-23", "IP-30", "IP-40"]
levels = ["V1", "V2", "V4"]
[[package]]
id = "IP-34"
title = "Interactive Client CLI"
depends_on = ["IP-31", "IP-33"]
levels = ["V1", "V3"]
[[package]]
id = "IP-35"
title = "State inspection and reset"
depends_on = ["IP-10", "IP-13", "IP-20", "IP-32"]
levels = ["V1", "V2", "V4"]
[[package]]
id = "IP-40"
title = "Minimal non-interactive runtime slice"
depends_on = ["IP-30", "IP-31"]
levels = ["V3"]
[[package]]
id = "IP-41"
title = "Workspace, Git, and persistence slice"
depends_on = ["IP-20", "IP-32", "IP-40"]
levels = ["V3", "V5"]
[[package]]
id = "IP-42"
title = "Interactive and multi-session slice"
depends_on = ["IP-33", "IP-34", "IP-40"]
levels = ["V3"]
[[package]]
id = "IP-43"
title = "Host-escalation slice"
depends_on = ["IP-24", "IP-34", "IP-42"]
levels = ["V3"]
[[package]]
id = "IP-44"
title = "Durability and hostile-failure gate"
depends_on = ["IP-32", "IP-35", "IP-40", "IP-41", "IP-42", "IP-43"]
levels = ["V4"]
[[package]]
id = "IP-45"
title = "Release qualification"
depends_on = ["IP-44"]
levels = ["V5"]

7
tests/fixtures/README.md vendored
View file

@ -1,7 +0,0 @@
# Fixture conventions
Fixtures are immutable inputs grouped by the verifier that owns their format. Use descriptive lowercase directory names and commit expected outputs beside inputs when exact bytes matter. A fixture directory must contain a `fixture.toml` with `schema`, `case`, and `expected` fields; paths in that file are relative to its directory.
Positive and negative cases remain separate. Negative cases name the rejected condition and assert the stable error category, not incidental wording. Physical and failure fixtures also record the verification level, durable checkpoint, and exact identity fields under test. Generated, downloaded, host-specific, credential-bearing, and mutable runtime data are not fixtures.
Tests must copy writable inputs to a test-owned temporary directory and remove it on success or failure. Retained corpus updates are reviewed as input changes; tests never rewrite committed expected output.

342
tests/tooling/test_devtool.py
View file

@ -1,342 +0,0 @@
import copy
import contextlib
import importlib.util
import io
from pathlib import Path
import subprocess
import tempfile
import unittest
from unittest import mock
ROOT = Path(__file__).resolve().parents[2]
SPEC = importlib.util.spec_from_file_location("lazaret_dev", ROOT / "tools/lazaret_dev.py")
DEV = importlib.util.module_from_spec(SPEC)
SPEC.loader.exec_module(DEV)
class RegistryTests(unittest.TestCase):
def setUp(self):
self.packages = DEV.load_toml(ROOT / "support/work-packages.toml")
self.refinements = DEV.load_toml(ROOT / "support/model-refinements.toml")
self.external = DEV.load_toml(ROOT / "support/external-tools.toml")
self.integrations = DEV.load_toml(ROOT / "support/integration-tests.toml")
self.process_safety = DEV.load_toml(ROOT / "support/process-safety.toml")
def test_committed_registries_are_complete(self):
packages = DEV.validate_packages(self.packages)
DEV.validate_refinements(self.refinements, {package["id"] for package in packages})
DEV.validate_external_tools(self.external)
capability_ids = {item["id"] for kind in ("command", "feature") for item in self.external[kind]}
DEV.validate_integrations(self.integrations, capability_ids)
DEV.validate_process_safety(self.process_safety, self.integrations)
def test_dependency_cycle_is_rejected(self):
packages = copy.deepcopy(self.packages)
packages["package"][0]["depends_on"] = ["IP-01"]
with self.assertRaisesRegex(DEV.RegistryError, "cycle"):
DEV.validate_packages(packages)
def test_unknown_model_symbol_is_rejected(self):
refinements = copy.deepcopy(self.refinements)
refinements["coverage"][0]["symbols"].append("UnknownAction")
package_ids = {package["id"] for package in DEV.validate_packages(self.packages)}
with self.assertRaisesRegex(DEV.RegistryError, "coverage mismatch"):
DEV.validate_refinements(refinements, package_ids)
def test_unknown_probe_policy_is_rejected(self):
external = copy.deepcopy(self.external)
external["command"][0]["policy"] = "ignore"
with self.assertRaisesRegex(DEV.RegistryError, "fail or skip"):
DEV.validate_external_tools(external)
def test_command_fields_are_strict(self):
mutations = (
lambda command: command.pop("program"),
lambda command: command.update(args=[1]),
lambda command: command.update(unexpected=True),
)
for mutation in mutations:
with self.subTest(mutation=mutation):
external = copy.deepcopy(self.external)
mutation(external["command"][0])
with self.assertRaises(DEV.RegistryError):
DEV.validate_external_tools(external)
def test_each_probe_rejects_missing_fields(self):
for index, feature in enumerate(self.external["feature"]):
with self.subTest(probe=feature["probe"]):
external = copy.deepcopy(self.external)
removable = next((field for field in feature if field not in {"id", "probe", "policy", "levels", "diagnostic"}), "diagnostic")
external["feature"][index].pop(removable)
with self.assertRaises(DEV.RegistryError):
DEV.validate_external_tools(external)
def test_each_probe_rejects_malformed_fields(self):
invalid = {
"linux-x86_64": {"id": 1},
"kernel-at-least": {"minimum": 6.8},
"registered-host-support": {"contract": "unknown"},
"user-namespace": {"program": 1},
"subordinate-ids": {"minimum_count": "65536"},
"open-character-device": {"access": "read-only"},
}
for index, feature in enumerate(self.external["feature"]):
with self.subTest(probe=feature["probe"]):
external = copy.deepcopy(self.external)
external["feature"][index].update(invalid[feature["probe"]])
with self.assertRaises(DEV.RegistryError):
DEV.validate_external_tools(external)
def test_each_probe_rejects_extraneous_fields(self):
for index, feature in enumerate(self.external["feature"]):
with self.subTest(probe=feature["probe"]):
external = copy.deepcopy(self.external)
external["feature"][index]["unexpected"] = True
with self.assertRaisesRegex(DEV.RegistryError, "unexpected fields"):
DEV.validate_external_tools(external)
def test_supported_platform_probe_is_mandatory(self):
for capability in ("linux-x86_64", "kernel", "pidfs-host-support", "user-namespaces"):
with self.subTest(capability=capability):
external = copy.deepcopy(self.external)
external["feature"] = [feature for feature in external["feature"] if feature["id"] != capability]
with self.assertRaisesRegex(DEV.RegistryError, "external manifest missing"):
DEV.validate_external_tools(external)
def test_pidfs_contract_fields_are_strict(self):
mutations = (
lambda external: external["pidfs_host_support"].pop("diagnostic_smoke"),
lambda external: external["pidfs_host_support"].update(minimum_kernel=6.9),
lambda external: external["pidfs_host_support"].update(unexpected=True),
lambda external: external["host_probe"][0].update(steps=["kernel-version-only"]),
lambda external: external["host_probe"][0].update(attempts_per_step=True),
lambda external: external["host_probe"][0].update(total_timeout_ms=1000),
lambda external: external["host_probe"][0].update(step_timeout_ms=4000),
lambda external: external["kernel_qualification"][0].pop("source_commit"),
lambda external: external["kernel_qualification"][0].update(build_image_sha256="bad"),
lambda external: external["kernel_qualification"][0].update(build_image_sha256=1),
lambda external: external["kernel_qualification"][0].update(id=[]),
lambda external: external["kernel_qualification"][0].update(unexpected=True),
)
for mutation in mutations:
with self.subTest(mutation=mutation):
external = copy.deepcopy(self.external)
mutation(external)
with self.assertRaises(DEV.RegistryError):
DEV.validate_external_tools(external)
def test_linux_68_is_refused_and_69_meets_only_the_floor(self):
kernel = next(feature for feature in self.external["feature"] if feature["id"] == "kernel")
with mock.patch.object(DEV.platform, "system", return_value="Linux"), mock.patch.object(
DEV.platform, "release", return_value="6.8.99"
):
self.assertEqual(DEV.probe_feature(kernel), (False, "6.8.99"))
with mock.patch.object(DEV.platform, "system", return_value="Linux"), mock.patch.object(
DEV.platform, "release", return_value="6.9.0"
):
self.assertEqual(DEV.probe_feature(kernel), (True, "6.9.0"))
with mock.patch.object(DEV.platform, "system", return_value="Linux"), mock.patch.object(
DEV.platform, "release", return_value="6.12.38+deb13-amd64"
):
self.assertEqual(DEV.probe_feature(kernel), (True, "6.12.38+deb13-amd64"))
pidfs = next(feature for feature in self.external["feature"] if feature["id"] == "pidfs-host-support")
self.assertEqual(DEV.probe_feature(pidfs), (False, "registered runner pending IP-03"))
def test_pidfs_smoke_failure_is_a_hard_runtime_refusal(self):
contract = self.external["pidfs_host_support"]
self.assertTrue(contract["diagnostic_smoke"].startswith("LZ-HOST-PIDFS-SMOKE:"))
self.assertEqual(contract["runtime_failure_policy"], "fail-before-generation")
def test_mandatory_capabilities_cannot_be_remapped(self):
for capability in ("linux-x86_64", "kernel", "pidfs-host-support", "user-namespaces"):
with self.subTest(capability=capability):
external = copy.deepcopy(self.external)
feature = next(item for item in external["feature"] if item["id"] == capability)
feature.update(policy="fail")
with self.assertRaisesRegex(DEV.RegistryError, "mandatory feature contract drift"):
DEV.validate_external_tools(external)
external = copy.deepcopy(self.external)
pidfs = next(item for item in external["feature"] if item["id"] == "pidfs-host-support")
pidfs.pop("contract")
pidfs["probe"] = "linux-x86_64"
with self.assertRaisesRegex(DEV.RegistryError, "mandatory feature contract drift"):
DEV.validate_external_tools(external)
external = copy.deepcopy(self.external)
rustc = next(item for item in external["command"] if item["id"] == "rustc")
rustc["levels"] = ["V1"]
with self.assertRaisesRegex(DEV.RegistryError, "mandatory command contract drift"):
DEV.validate_external_tools(external)
def test_unqualified_vendor_build_is_rejected(self):
external = copy.deepcopy(self.external)
vendor = copy.deepcopy(external["kernel_qualification"][0])
vendor.update(
id="vendor-linux-6.9.0-x86_64",
kind="vendor",
vendor="Example Vendor",
vendor_patchset_sha256="0" * 64,
status="unqualified",
)
external["kernel_qualification"].append(vendor)
external["pidfs_host_support"]["qualification_ids"].append(vendor["id"])
with self.assertRaisesRegex(DEV.RegistryError, "not qualified"):
DEV.validate_external_tools(external)
def test_qualified_vendor_release_string_is_representable(self):
external = copy.deepcopy(self.external)
vendor = copy.deepcopy(external["kernel_qualification"][0])
vendor.update(
id="vendor-linux-6.12-x86_64",
kind="vendor",
release="6.12.38-1-amd64",
vendor="Example Vendor",
vendor_patchset_sha256="0" * 64,
)
external["kernel_qualification"].append(vendor)
external["pidfs_host_support"]["qualification_ids"].append(vendor["id"])
DEV.validate_external_tools(external)
def test_process_safety_registration_is_strict(self):
mutations = (
lambda process: process["policy"].pop("dynamic_scenario"),
lambda process: process["policy"].update(production_roots=["crates/lazaret-core"]),
lambda process: process["policy"].update(lint_allow_paths=["crates/foreign.rs"]),
lambda process: process["policy"].update(trace_expression="read"),
lambda process: process["policy"].update(forbidden_syscall_patterns=["$^"]),
lambda process: process["policy"].update(unexpected=True),
lambda process: process["runtime_dependency"][0].update(features=["z", "a"]),
lambda process: process["runtime_dependency"][0].update(checksum=1),
lambda process: process["trace_case"][0].update(initial_execve_count=True),
)
for mutation in mutations:
with self.subTest(mutation=mutation):
process = copy.deepcopy(self.process_safety)
mutation(process)
with self.assertRaises(DEV.RegistryError):
DEV.validate_process_safety(process, self.integrations)
integrations = copy.deepcopy(self.integrations)
integrations["scenarios"] = []
with self.assertRaisesRegex(DEV.RegistryError, "dynamic syscall scenario"):
DEV.validate_process_safety(self.process_safety, integrations)
def test_process_lint_exemption_is_detected(self):
self.assertTrue(DEV.has_process_lint_exemption("#![allow(clippy::disallowed_types)]\n"))
self.assertTrue(DEV.has_process_lint_exemption("#[expect(clippy::{disallowed_methods})]\n"))
def test_workspace_process_lints_are_mandatory(self):
workspace = DEV.load_toml(ROOT / "Cargo.toml")
DEV.validate_workspace_process_lints(workspace)
for group, lint in (("rust", "unsafe_code"), ("clippy", "disallowed_methods"), ("clippy", "disallowed_types")):
with self.subTest(lint=lint):
changed = copy.deepcopy(workspace)
changed["workspace"]["lints"][group].pop(lint)
with self.assertRaises(DEV.RegistryError):
DEV.validate_workspace_process_lints(changed)
def test_every_workspace_member_inherits_process_lints(self):
workspace = DEV.load_toml(ROOT / "Cargo.toml")["workspace"]
for member in workspace["members"]:
with self.subTest(member=member):
manifest = DEV.load_toml(ROOT / member / "Cargo.toml")
DEV.validate_member_process_lints(manifest, member)
changed = copy.deepcopy(manifest)
changed["lints"] = {"workspace": False}
with self.assertRaises(DEV.RegistryError):
DEV.validate_member_process_lints(changed, member)
def test_compiler_resolves_grouped_process_import_alias(self):
with tempfile.TemporaryDirectory() as directory:
root = Path(directory)
(root / "src").mkdir()
(root / "Cargo.toml").write_text(
'[package]\nname = "lint-probe"\nversion = "0.0.0"\nedition = "2024"\n'
"[lints.clippy]\ndisallowed_types = \"deny\"\n"
)
(root / ".clippy.toml").write_text(DEV.clippy_config_view(self.process_safety))
(root / "src/main.rs").write_text(
'use std::{process::Command as C};\nfn main() { let _ = C::new("true"); }\n'
)
result = subprocess.run(
["cargo", "clippy", "--offline", "--", "-D", "warnings"],
cwd=root,
text=True,
stdout=subprocess.PIPE,
stderr=subprocess.STDOUT,
check=False,
)
self.assertNotEqual(result.returncode, 0)
self.assertIn("disallowed type", result.stdout)
def test_process_syscall_trace_refuses_bypass(self):
policy = self.process_safety["policy"]
trace_case = self.process_safety["trace_case"][0]
DEV.validate_process_trace(['execve("/tmp/lazaret", ["lazaret"], 0x0) = 0'], policy, trace_case)
for syscall in ("clone", "execveat", "wait4", "waitid"):
with self.subTest(syscall=syscall), self.assertRaisesRegex(DEV.RegistryError, "forbidden"):
DEV.validate_process_trace(
['execve("/tmp/lazaret", ["lazaret"], 0x0) = 0', f"{syscall}(0) = 1"],
policy,
trace_case,
)
with self.assertRaisesRegex(DEV.RegistryError, "SIGCHLD"):
DEV.validate_process_trace(
['execve("/tmp/lazaret", ["lazaret"], 0x0) = 0', "rt_sigaction(SIGCHLD, {}, NULL, 8) = 0"],
policy,
trace_case,
)
with self.assertRaisesRegex(DEV.RegistryError, "execve surface count"):
DEV.validate_process_trace(
['execve("/tmp/lazaret", [], 0x0) = 0', 'execve("/tmp/other", [], 0x0) = 0'],
policy,
trace_case,
)
def test_generated_host_view_covers_authoritative_fields(self):
baseline = DEV.host_contract_view(self.external, self.integrations, self.process_safety)
external = copy.deepcopy(self.external)
external["kernel_qualification"][0]["probe_binary_sha256"] = "0" * 64
self.assertNotEqual(DEV.host_contract_view(external, self.integrations, self.process_safety), baseline)
process = copy.deepcopy(self.process_safety)
process["runtime_dependency"][0]["features"] = ["changed"]
self.assertNotEqual(DEV.host_contract_view(self.external, self.integrations, process), baseline)
def test_integration_manifest_rejects_top_level_extras(self):
integrations = copy.deepcopy(self.integrations)
integrations["unexpected"] = True
capability_ids = {item["id"] for kind in ("command", "feature") for item in self.external[kind]}
with self.assertRaisesRegex(DEV.RegistryError, "unexpected fields"):
DEV.validate_integrations(integrations, capability_ids)
def test_missing_skip_capability_skips_scenario(self):
integrations = {
"scenarios": [{"name": "fuse", "level": "V2", "command": ["false"], "capabilities": ["fuse-device"]}]
}
with mock.patch.object(DEV, "probe", return_value=(set(), {"fuse-device"})):
with contextlib.redirect_stdout(io.StringIO()) as output:
DEV.run_integrations("V2", self.external, integrations)
self.assertIn("SKIP fuse", output.getvalue())
def test_missing_fail_capability_rejects_scenario(self):
integrations = {
"scenarios": [{"name": "compiler", "level": "V2", "command": ["false"], "capabilities": ["rustc"]}]
}
with mock.patch.object(DEV, "probe", return_value=(set(), set())):
with self.assertRaisesRegex(DEV.RegistryError, "undeclared capability failure"):
DEV.run_integrations("V2", self.external, integrations)
def test_subordinate_range_accepts_name_or_numeric_uid(self):
with tempfile.TemporaryDirectory() as directory:
path = Path(directory) / "subids"
path.write_text("developer:not-a-number:65536\n1000:524288:65536\n")
self.assertEqual(DEV.subordinate_id_range(path, {"developer", "1000"}, 65536), 524288)
def test_subordinate_range_rejects_short_or_malformed_rows(self):
with tempfile.TemporaryDirectory() as directory:
path = Path(directory) / "subids"
path.write_text("developer:524288:65535\ndeveloper:bad:65536\ndeveloper:0:65536\n")
self.assertIsNone(DEV.subordinate_id_range(path, {"developer", "1000"}, 65536))
if __name__ == "__main__":
unittest.main()

275
tests/tooling/test_verify.py Normal file
View file

@ -0,0 +1,275 @@
from __future__ import annotations
import copy
import importlib.machinery
import importlib.util
from pathlib import Path
import tempfile
import unittest
from unittest import mock
ROOT = Path(__file__).resolve().parents[2]
LOADER = importlib.machinery.SourceFileLoader(
"lazaret_verify", str(ROOT / "tools/lazaret_verify.py")
)
SPEC = importlib.util.spec_from_loader(LOADER.name, LOADER)
VERIFY = importlib.util.module_from_spec(SPEC)
LOADER.exec_module(VERIFY)
class VerificationTests(unittest.TestCase):
def test_current_workspace_lints_pass(self) -> None:
VERIFY.audit_workspace_lints(VERIFY.workspace_metadata())
def test_workspace_unsafe_policy_is_required(self) -> None:
workspace = VERIFY.load_toml(ROOT / "Cargo.toml")
workspace["workspace"]["lints"]["rust"]["unsafe_code"] = "deny"
original = VERIFY.load_toml
VERIFY.load_toml = lambda path: workspace if path == ROOT / "Cargo.toml" else original(path)
try:
with self.assertRaisesRegex(VERIFY.VerificationError, "forbid unsafe"):
VERIFY.audit_workspace_lints(VERIFY.workspace_metadata())
finally:
VERIFY.load_toml = original
def test_clippy_process_policy_is_exact(self) -> None:
config = VERIFY.load_toml(ROOT / ".clippy.toml")
config["disallowed-methods"] = config["disallowed-methods"][:-1]
original = VERIFY.load_toml
VERIFY.load_toml = lambda path: config if path == ROOT / ".clippy.toml" else original(path)
try:
with self.assertRaisesRegex(VERIFY.VerificationError, "reviewed boundary"):
VERIFY.audit_workspace_lints(VERIFY.workspace_metadata())
finally:
VERIFY.load_toml = original
def test_member_lint_inheritance_is_required(self) -> None:
metadata = VERIFY.workspace_metadata()
member = next(
package
for package in metadata["packages"]
if package["id"] in set(metadata["workspace_members"])
)
original = VERIFY.load_toml
def without_inheritance(path: Path) -> dict:
data = original(path)
if path == Path(member["manifest_path"]):
data = copy.deepcopy(data)
data.pop("lints")
return data
VERIFY.load_toml = without_inheritance
try:
with self.assertRaisesRegex(VERIFY.VerificationError, "inherit workspace lints"):
VERIFY.audit_workspace_lints(metadata)
finally:
VERIFY.load_toml = original
def test_lint_bypass_pattern_covers_restricted_lints(self) -> None:
forbidden = (
"#[allow(disallowed_methods)]",
"#![expect(clippy::disallowed_types)]",
"#[allow(warnings)]",
"#[allow(clippy::all)]",
"#[allow(clippy::style)]",
"#[expect(clippy::restriction)]",
"#![allow(clippy :: all)]",
"#[expect(clippy :: style)]",
)
for source in forbidden:
with self.subTest(source=source):
self.assertIsNotNone(VERIFY.LINT_BYPASS.search(source))
self.assertIsNone(VERIFY.LINT_BYPASS.search("#[allow(dead_code)]"))
def test_workspace_source_discovery_is_not_confined_to_crates(self) -> None:
with tempfile.TemporaryDirectory(dir=ROOT) as directory:
package_root = Path(directory)
source = package_root / "outside.rs"
source.write_text("fn main() {}")
metadata = {
"workspace_members": ["outside"],
"packages": [
{
"id": "outside",
"manifest_path": str(package_root / "Cargo.toml"),
}
],
"target_directory": str(ROOT / "target"),
}
self.assertEqual(VERIFY.workspace_rust_sources(metadata), [source])
def test_workspace_source_discovery_rejects_overlapping_target_directory(self) -> None:
with tempfile.TemporaryDirectory(dir=ROOT) as directory:
package_root = Path(directory)
metadata = {
"workspace_members": ["outside"],
"packages": [
{
"id": "outside",
"manifest_path": str(package_root / "Cargo.toml"),
}
],
"target_directory": str(ROOT),
}
with self.assertRaisesRegex(VERIFY.VerificationError, "must not contain"):
VERIFY.workspace_rust_sources(metadata)
metadata["target_directory"] = str(package_root)
with self.assertRaisesRegex(VERIFY.VerificationError, "must not contain"):
VERIFY.workspace_rust_sources(metadata)
def test_process_trace_requires_exactly_one_exec(self) -> None:
VERIFY.validate_process_trace("example", ['execve("example", [], []) = 0'])
with self.assertRaisesRegex(VERIFY.VerificationError, "execve surface count 0"):
VERIFY.validate_process_trace("example", [])
with self.assertRaisesRegex(VERIFY.VerificationError, "execve surface count 2"):
VERIFY.validate_process_trace("example", ["execve(a)", "execve(b)"])
def test_process_trace_rejects_each_forbidden_surface(self) -> None:
forbidden = (
"clone(child_stack=NULL) = 1",
"clone3(NULL, 0) = 1",
"execveat(3, \"child\", [], [], 0) = 0",
"fork() = 1",
"vfork() = 1",
"wait4(1, NULL, 0, NULL) = 1",
"waitid(P_PIDFD, 3, {}, WEXITED, NULL) = 0",
"rt_sigaction(SIGCHLD, {}, NULL, 8) = 0",
)
for syscall in forbidden:
with self.subTest(syscall=syscall):
with self.assertRaisesRegex(VERIFY.VerificationError, "forbidden process syscall"):
VERIFY.validate_process_trace("example", ["execve(example)", syscall])
def test_process_syscall_audit_requires_strace(self) -> None:
with mock.patch.object(VERIFY.shutil, "which", return_value=None):
with self.assertRaisesRegex(VERIFY.VerificationError, "strace must be installed"):
VERIFY.audit_process_syscalls({})
def test_process_syscall_audit_rejects_failed_binary(self) -> None:
with self.assertRaisesRegex(VERIFY.VerificationError, "exercised path exited 1"):
VERIFY.validate_trace_exit("example", 1)
def test_workspace_binary_discovery_covers_every_current_target(self) -> None:
self.assertEqual(
set(VERIFY.workspace_binary_targets(VERIFY.workspace_metadata())),
{
"lazaret",
"lazaret-escalation-client",
"lazaret-host-coordinator",
"lazaret-network-sidecar",
"lazaret-runtime-supervisor",
},
)
def test_workspace_binary_names_must_be_unique(self) -> None:
metadata = {
"workspace_members": ["one", "two"],
"packages": [
{"id": "one", "targets": [{"name": "same", "kind": ["bin"]}]},
{"id": "two", "targets": [{"name": "same", "kind": ["bin"]}]},
],
}
with self.assertRaisesRegex(VERIFY.VerificationError, "must be unique"):
VERIFY.workspace_binary_targets(metadata)
def test_binary_artifacts_use_cargo_reported_path(self) -> None:
metadata = {
"workspace_members": ["one"],
"packages": [
{"id": "one", "targets": [{"name": "example", "kind": ["bin"]}]}
],
}
executable = "/tmp/custom-cargo-target/debug/example"
message = (
'{"reason":"compiler-artifact","package_id":"one",'
f'"target":{{"name":"example","kind":["bin"]}},"executable":"{executable}"}}'
)
self.assertEqual(
VERIFY.binary_artifacts(metadata, message),
{"example": Path(executable)},
)
def test_tool_versions_are_exactly_pinned(self) -> None:
expected = {
"rustc": r"^rustc 1\.90\.0 ",
"cargo": r"^cargo 1\.90\.0 ",
"cargo-nextest": r"^cargo-nextest 0\.9\.140 ",
"cargo-deny": r"^cargo-deny 0\.20\.2$",
"tlc": r"Version 2\.19 ",
"uv": r"^uv 0\.11\.28(?: .*)?$",
}
self.assertEqual(
{program: pattern.pattern for program, _, _, pattern in VERIFY.REQUIRED_TOOL_VERSIONS},
expected,
)
def test_entrypoint_uses_dependency_free_offline_uv(self) -> None:
entrypoint = (ROOT / "tools/verify").read_text()
self.assertIn(
"uv run --python '>=3.11' --no-project --offline "
"--no-python-downloads --no-cache python3",
entrypoint,
)
self.assertIn('lazaret_verify.py" "$@"', entrypoint)
def test_workspace_tests_use_nextest_and_cargo_retains_doctests(self) -> None:
source = (ROOT / "tools/lazaret_verify.py").read_text()
expected = [
[
"cargo",
"nextest",
"run",
"--offline",
"--workspace",
"--all-features",
"--locked",
],
[
"cargo",
"test",
"--offline",
"--workspace",
"--all-features",
"--locked",
"--doc",
],
]
commands = []
original_run = VERIFY.run
VERIFY.run = lambda command, cwd=VERIFY.ROOT: commands.append(command)
try:
VERIFY.run_rust_tests()
finally:
VERIFY.run = original_run
self.assertEqual(commands, expected)
self.assertIn("exact cargo-nextest 0.9.140", source)
self.assertIn("exact uv 0.11.28", source)
self.assertIn("Python 3.11 or newer", source)
def test_advisory_refresh_checks_versions_before_mutation(self) -> None:
events = []
original_versions = VERIFY.check_tool_versions
original_refresh = VERIFY.refresh_advisories
VERIFY.check_tool_versions = lambda: events.append("versions")
VERIFY.refresh_advisories = lambda: events.append("refresh")
try:
with mock.patch.object(VERIFY.sys, "argv", ["tools/verify", "--refresh-advisories"]):
self.assertEqual(VERIFY.main(), 0)
finally:
VERIFY.check_tool_versions = original_versions
VERIFY.refresh_advisories = original_refresh
self.assertEqual(events, ["versions", "refresh"])
def test_model_paths_are_current_and_complete(self) -> None:
self.assertEqual(
{module.name for module, _ in VERIFY.MODEL_CONFIGURATIONS},
{"Lazaret.tla", "PreparedLower.tla"},
)
for module, config in VERIFY.MODEL_CONFIGURATIONS:
self.assertTrue(module.is_file())
self.assertTrue(config.is_file())
if __name__ == "__main__":
unittest.main()

3
tools/dev
View file

@ -1,3 +0,0 @@
#!/usr/bin/env bash
set -euo pipefail
exec python3 "$(dirname "$0")/lazaret_dev.py" "$@"

1186
tools/lazaret_dev.py
View file

File diff suppressed because it is too large Load diff

483
tools/lazaret_verify.py Normal file
View file

@ -0,0 +1,483 @@
#!/usr/bin/env python3
"""Run Lazaret's repository-owned verification and focused host audits."""
from __future__ import annotations
import argparse
import json
from pathlib import Path
import re
import shutil
import subprocess
import sys
import tempfile
import tomllib
ROOT = Path(__file__).resolve().parent.parent
MODEL_CONFIGURATIONS = (
(ROOT / "docs/protocol/Lazaret.tla", ROOT / "docs/protocol/Lazaret.cfg"),
(ROOT / "docs/protocol/PreparedLower.tla", ROOT / "docs/protocol/PreparedLower.cfg"),
)
NEXTEST_COMMAND = (
"cargo",
"nextest",
"run",
"--offline",
"--workspace",
"--all-features",
"--locked",
)
DOCTEST_COMMAND = (
"cargo",
"test",
"--offline",
"--workspace",
"--all-features",
"--locked",
"--doc",
)
REQUIRED_TOOL_VERSIONS = (
("rustc", ("--version",), (0,), re.compile(r"^rustc 1\.90\.0 ")),
("cargo", ("--version",), (0,), re.compile(r"^cargo 1\.90\.0 ")),
(
"cargo-nextest",
("--version",),
(0,),
re.compile(r"^cargo-nextest 0\.9\.140 "),
),
("cargo-deny", ("--version",), (0,), re.compile(r"^cargo-deny 0\.20\.2$")),
("tlc", ("-h",), (0, 1), re.compile(r"Version 2\.19 ")),
("uv", ("--version",), (0,), re.compile(r"^uv 0\.11\.28(?: .*)?$")),
)
REQUIRED_DISALLOWED_TYPES = {
"std::process::Child",
"std::process::Command",
"tokio::process::Child",
"tokio::process::Command",
}
REQUIRED_DISALLOWED_METHODS = {
"libc::clone",
"libc::execve",
"libc::execveat",
"libc::fork",
"libc::posix_spawn",
"libc::sigaction",
"libc::signal",
"libc::vfork",
"libc::wait",
"libc::wait4",
"libc::waitid",
"libc::waitpid",
"nix::sys::signal::sigaction",
"nix::sys::wait::wait",
"nix::sys::wait::waitid",
"nix::sys::wait::waitpid",
"nix::unistd::execve",
"nix::unistd::execveat",
"nix::unistd::fork",
"nix::unistd::vfork",
"rustix::process::kill_process",
"rustix::process::kill_process_group",
"rustix::process::pidfd_open",
"rustix::process::pidfd_send_signal",
"rustix::process::waitid",
"rustix::process::waitpid",
"std::process::Child::kill",
"std::process::Child::try_wait",
"std::process::Child::wait",
"std::process::Child::wait_with_output",
"std::process::Command::output",
"std::process::Command::spawn",
"std::process::Command::status",
}
PROCESS_LINT_EXEMPTIONS = frozenset()
FORBIDDEN_PROCESS_SYSCALLS = tuple(
re.compile(pattern)
for pattern in (
r"^clone3?\(",
r"^execveat\(",
r"^fork\(",
r"^vfork\(",
r"^wait4\(",
r"^waitid\(",
r"^rt_sigaction\(SIGCHLD,",
)
)
LINT_BYPASS = re.compile(
r"#\s*!?\s*\[[^]]*(?:allow|expect)\s*\([^]]*"
r"(?:warnings|clippy\s*::\s*(?:all|style|restriction)|disallowed_methods|disallowed_types)"
)
class VerificationError(RuntimeError):
pass
def require(condition: bool, message: str) -> None:
if not condition:
raise VerificationError(message)
def load_toml(path: Path) -> dict:
with path.open("rb") as source:
return tomllib.load(source)
def run(command: list[str], cwd: Path = ROOT) -> None:
print(f"RUN {' '.join(command)}", flush=True)
subprocess.run(command, cwd=cwd, check=True)
def check_tool_versions() -> None:
require(sys.version_info >= (3, 11), "Python 3.11 or newer is required")
for program, args, accepted_exit_codes, pattern in REQUIRED_TOOL_VERSIONS:
executable = shutil.which(program)
require(executable is not None, f"{program} must be installed on PATH")
result = subprocess.run(
[executable, *args],
text=True,
stdout=subprocess.PIPE,
stderr=subprocess.STDOUT,
check=False,
)
output = result.stdout.strip()
require(
result.returncode in accepted_exit_codes and pattern.search(output) is not None,
f"unsupported {program} version: {output or 'no version output'}",
)
print("PASS pinned verification tool versions")
def workspace_metadata() -> dict:
result = subprocess.run(
[
"cargo",
"metadata",
"--locked",
"--offline",
"--all-features",
"--format-version",
"1",
],
cwd=ROOT,
text=True,
stdout=subprocess.PIPE,
check=True,
)
return json.loads(result.stdout)
def audit_workspace_lints(metadata: dict) -> None:
workspace = load_toml(ROOT / "Cargo.toml")
rust_lints = workspace.get("workspace", {}).get("lints", {}).get("rust", {})
clippy_lints = workspace.get("workspace", {}).get("lints", {}).get("clippy", {})
require(rust_lints.get("unsafe_code") == "forbid", "workspace must forbid unsafe Rust")
require(
clippy_lints.get("disallowed_methods") == "deny",
"workspace must deny Clippy disallowed methods",
)
require(
clippy_lints.get("disallowed_types") == "deny",
"workspace must deny Clippy disallowed types",
)
clippy_config = load_toml(ROOT / ".clippy.toml")
disallowed_types = {entry.get("path") for entry in clippy_config.get("disallowed-types", [])}
disallowed_methods = {
entry.get("path") for entry in clippy_config.get("disallowed-methods", [])
}
require(
disallowed_types == REQUIRED_DISALLOWED_TYPES,
"Clippy disallowed process types must match the reviewed boundary",
)
require(
disallowed_methods == REQUIRED_DISALLOWED_METHODS,
"Clippy disallowed process methods must match the reviewed boundary",
)
packages = {package["id"]: package for package in metadata["packages"]}
for package_id in metadata["workspace_members"]:
package = packages[package_id]
manifest = load_toml(Path(package["manifest_path"]))
require(
manifest.get("lints") == {"workspace": True},
f"{package['name']}: package must inherit workspace lints without override",
)
for path in workspace_rust_sources(metadata):
relative = str(path.relative_to(ROOT))
require(
LINT_BYPASS.search(path.read_text(errors="replace")) is None
or relative in PROCESS_LINT_EXEMPTIONS,
f"process-safety lint exemption is forbidden: {relative}",
)
print("PASS workspace unsafe and process-control lint boundary")
def workspace_rust_sources(metadata: dict) -> list[Path]:
packages = {package["id"]: package for package in metadata["packages"]}
target_directory = Path(metadata["target_directory"]).resolve()
sources = set()
for package_id in metadata["workspace_members"]:
package_root = Path(packages[package_id]["manifest_path"]).resolve().parent
require(
package_root.is_relative_to(ROOT),
f"workspace package is outside the repository: {package_root}",
)
require(
not package_root.is_relative_to(target_directory),
"Cargo target directory must not contain a workspace package",
)
sources.update(
path.resolve()
for path in package_root.rglob("*.rs")
if not path.resolve().is_relative_to(target_directory)
)
return sorted(sources)
def audit_dependencies(metadata: dict) -> None:
policy = load_toml(ROOT / "deny.toml")
allowed_licenses = set(policy["licenses"]["allow"])
workspace_members = set(metadata["workspace_members"])
for package in metadata["packages"]:
if package["id"] not in workspace_members:
source = package.get("source") or ""
require(
source.startswith("registry+https://github.com/rust-lang/crates.io-index"),
f"unapproved dependency source: {package['name']}",
)
license_expression = package.get("license") or ""
licenses = set(re.findall(r"[A-Za-z0-9.-]+", license_expression)) - {
"AND",
"OR",
"WITH",
}
require(
bool(licenses) and licenses <= allowed_licenses,
f"unapproved dependency license: {package['name']} {license_expression}",
)
for dependency in package["dependencies"]:
dependency_source = dependency.get("source")
if dependency_source is None:
dependency_path = dependency.get("path")
require(
dependency_path is not None
and Path(dependency_path).resolve().is_relative_to(ROOT),
f"external path dependency: {package['name']} -> {dependency['name']}",
)
else:
require(
dependency_source.startswith(
"registry+https://github.com/rust-lang/crates.io-index"
),
f"unapproved dependency source: {package['name']} -> {dependency['name']}",
)
require(
dependency["req"] != "*",
f"wildcard dependency: {package['name']} -> {dependency['name']}",
)
run(["cargo", "deny", "--frozen", "check", "bans", "licenses", "sources"])
print("PASS dependency source, wildcard, and license audit")
def run_models() -> None:
tlc = shutil.which("tlc")
require(tlc is not None, "TLC must be installed on PATH")
with tempfile.TemporaryDirectory(prefix="lazaret-tlc-") as directory:
workdir = Path(directory)
for module, config in MODEL_CONFIGURATIONS:
require(module.is_file(), f"missing model: {module.relative_to(ROOT)}")
require(config.is_file(), f"missing model config: {config.relative_to(ROOT)}")
metadata = workdir / module.stem
run(
[
tlc,
"-workers",
"1",
"-metadir",
str(metadata),
"-config",
str(config),
str(module),
],
workdir,
)
def workspace_binary_targets(metadata: dict) -> dict[str, str]:
workspace_members = set(metadata["workspace_members"])
targets = [
(target["name"], package["id"])
for package in metadata["packages"]
if package["id"] in workspace_members
for target in package["targets"]
if "bin" in target["kind"]
]
names = [name for name, _ in targets]
require(len(names) == len(set(names)), "workspace binary target names must be unique")
return dict(targets)
def binary_artifacts(metadata: dict, messages: str) -> dict[str, Path]:
expected = workspace_binary_targets(metadata)
artifacts = {}
for line in messages.splitlines():
message = json.loads(line)
if message.get("reason") != "compiler-artifact" or message.get("executable") is None:
continue
target = message["target"]
name = target["name"]
if "bin" not in target["kind"] or expected.get(name) != message["package_id"]:
continue
require(name not in artifacts, f"duplicate executable artifact for {name}")
artifacts[name] = Path(message["executable"])
require(
set(artifacts) == set(expected),
f"binary artifact coverage mismatch; expected={sorted(expected)}, actual={sorted(artifacts)}",
)
return artifacts
def build_workspace_binaries(metadata: dict) -> dict[str, Path]:
command = [
"cargo",
"build",
"--offline",
"--workspace",
"--all-features",
"--bins",
"--locked",
"--message-format=json",
]
print(f"RUN {' '.join(command)}", flush=True)
result = subprocess.run(
command,
cwd=ROOT,
text=True,
stdout=subprocess.PIPE,
check=True,
)
return binary_artifacts(metadata, result.stdout)
def validate_process_trace(binary: str, lines: list[str]) -> None:
execve_count = sum(line.startswith("execve(") for line in lines)
require(execve_count == 1, f"{binary}: unexpected execve surface count {execve_count}")
for line in lines:
matches = [pattern.pattern for pattern in FORBIDDEN_PROCESS_SYSCALLS if pattern.search(line)]
require(not matches, f"{binary}: forbidden process syscall surface {line}: {matches}")
def audit_process_syscalls(metadata: dict) -> None:
strace = shutil.which("strace")
require(strace is not None, "strace must be installed for --process-syscalls")
require(sys.platform == "linux", "--process-syscalls requires Linux")
binaries = build_workspace_binaries(metadata)
require(binaries, "workspace has no binaries to trace")
with tempfile.TemporaryDirectory(prefix="lazaret-process-syscalls-") as directory:
for binary, executable in sorted(binaries.items()):
trace_base = Path(directory) / binary
result = subprocess.run(
[
strace,
"-ff",
"-qq",
"-e",
"trace=process,wait4,waitid,rt_sigaction",
"-o",
str(trace_base),
"--",
str(executable),
],
cwd=ROOT,
check=False,
)
validate_trace_exit(binary, result.returncode)
traces = sorted(Path(directory).glob(f"{binary}.*"))
require(traces, f"{binary}: strace produced no output")
lines = [
line
for trace in traces
for line in trace.read_text(errors="replace").splitlines()
]
validate_process_trace(binary, lines)
print("PASS final-binary exercised-path process-syscall audit")
def validate_trace_exit(binary: str, returncode: int) -> None:
require(returncode == 0, f"{binary}: exercised path exited {returncode}")
def refresh_advisories() -> None:
run(["cargo", "deny", "fetch"])
run(["cargo", "deny", "--frozen", "check", "advisories"])
def run_rust_tests() -> None:
run(list(NEXTEST_COMMAND))
run(list(DOCTEST_COMMAND))
def verify(process_syscalls: bool) -> None:
check_tool_versions()
metadata = workspace_metadata()
run(["cargo", "fmt", "--all", "--", "--check"])
run(
[
"cargo",
"clippy",
"--offline",
"--workspace",
"--all-targets",
"--all-features",
"--locked",
"--",
"-D",
"warnings",
]
)
run_rust_tests()
run([sys.executable, "-m", "unittest", "discover", "-s", "tests/tooling"])
audit_workspace_lints(metadata)
audit_dependencies(metadata)
run_models()
if process_syscalls:
audit_process_syscalls(metadata)
def main() -> int:
parser = argparse.ArgumentParser(
prog="tools/verify",
description=(
"Run formatting, Clippy, cargo-nextest, documentation tests, dependency "
"policy, process-control policy, and both TLA+ models. Cargo operations "
"are offline and locked; tests use exact cargo-nextest 0.9.140 and "
"orchestration uses exact uv 0.11.28 with Python 3.11 or newer."
)
)
actions = parser.add_mutually_exclusive_group()
actions.add_argument(
"--process-syscalls",
action="store_true",
help="also trace every current binary's no-argument path with strace",
)
actions.add_argument(
"--refresh-advisories",
action="store_true",
help="update the RustSec database and check advisories instead of the default suite",
)
args = parser.parse_args()
try:
if args.refresh_advisories:
check_tool_versions()
refresh_advisories()
else:
verify(args.process_syscalls)
except (OSError, subprocess.CalledProcessError, VerificationError) as error:
print(f"ERROR: {error}", file=sys.stderr)
return 1
return 0
if __name__ == "__main__":
sys.exit(main())

3
tools/verify Executable file
View file

@ -0,0 +1,3 @@
#!/usr/bin/env bash
set -euo pipefail
exec uv run --python '>=3.11' --no-project --offline --no-python-downloads --no-cache python3 "$(dirname "$0")/lazaret_verify.py" "$@"

3
tools/verify-v1
View file

@ -1,3 +0,0 @@
#!/usr/bin/env bash
set -euo pipefail
exec "$(dirname "$0")/dev" verify V1

3
tools/verify-v2
View file

@ -1,3 +0,0 @@
#!/usr/bin/env bash
set -euo pipefail
exec "$(dirname "$0")/dev" verify V2

3
tools/verify-v3
View file

@ -1,3 +0,0 @@
#!/usr/bin/env bash
set -euo pipefail
exec "$(dirname "$0")/dev" verify V3

3
tools/verify-v4
View file

@ -1,3 +0,0 @@
#!/usr/bin/env bash
set -euo pipefail
exec "$(dirname "$0")/dev" verify V4

Some files were not shown because too many files have changed in this diff Show more