#!/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 VERIFICATION_TEMP_ROOT = ROOT / "target" / "verification" MATERIALIZED_FUSER_MANIFEST = ( ROOT / ".lazaret/vendor/fuser-0.17.0/Cargo.toml" ).resolve() 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", "--filterset", ( "not binary(capability-drop-helper) and not binary(acquisition) " "and not binary(recovery-process) and not binary(runtime-composition) " "and not binary(network-runtime)" ), ) DOCTEST_COMMAND = ( "cargo", "test", "--offline", "--workspace", "--all-features", "--locked", "--doc", ) CAPABILITY_TEST_COMMAND = ( "cargo", "test", "--offline", "-p", "lazaret-linux", "--test", "capability-drop-helper", "--locked", ) ACQUISITION_TEST_COMMAND = ( "cargo", "test", "--offline", "-p", "lazaret-linux", "--test", "acquisition", "--locked", ) RECOVERY_PROCESS_TEST_COMMAND = ( "cargo", "test", "--offline", "-p", "lazaret-host-coordinator", "--test", "recovery-process", "--locked", ) RUNTIME_COMPOSITION_TEST_COMMAND = ( "cargo", "test", "--offline", "-p", "lazaret-host-coordinator", "--test", "runtime-composition", "--locked", ) NETWORK_RUNTIME_TEST_COMMAND = ( "cargo", "test", "--offline", "-p", "lazaret-runtime-supervisor", "--test", "network-runtime", "--locked", ) FUSER_PATCH_TEST_COMMAND = ( "cargo", "test", "--offline", "--locked", "--manifest-path", ".lazaret/vendor/fuser-0.17.0/Cargo.toml", "lock_request_preserves_kind_flags", ) REQUIRED_TOOL_VERSIONS = ( ("rustc", ("--version",), (0,), re.compile(r"^rustc 1\.97\.0 ")), ("cargo", ("--version",), (0,), re.compile(r"^cargo 1\.97\.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_ALLOWANCES = { "crates/lazaret-client/src/terminal.rs": { "signal_scope_restores_mask_and_default_termination" }, "crates/lazaret-linux/src/process.rs": { "append_to", "send_signal", }, "crates/lazaret-linux/src/process/broker.rs": { "acquire", "acquire_with_stdio", "acquire_with_stdio_after_ack", "acquire_captured", "private_role_command", "reap", "reap_status", "fail_running_captured", "acquire_spawned_child", "verify_direct_child_pidfd", "fail_before_pidfd", "fail_after_pidfd_closed", "run_transient", "run_transient_with_stdout", "run_transient_captured", "spawn_bootstrap", "captured_process", }, "crates/lazaret-linux/src/process/recovery.rs": { "recover_process", "current_process_identity", "match_recovery_process", "require_reapable_sigchld", "cleanup_sigchld_probe", "fail_sigchld_probe", }, "crates/lazaret-linux/src/process/launch.rs": { "append_parent_identity", "exec_target", "suspend_current_process", }, "crates/lazaret-host-coordinator/tests/runtime-composition.rs": {"run_benchmark_guest"}, "crates/lazaret-client/tests/state_cli.rs": { "machine_and_human_discovery_are_versioned_and_content_free", "missing_store_succeeds_only_when_the_complete_state_anchor_is_absent", "reset_refuses_an_arbitrary_container_or_host_path_before_state_access", "command", }, "crates/lazaret-linux/tests/acquisition.rs": { "run_acquisition", "successful_acquisition", "acknowledged_transition_precedes_exact_wrapper_release", "failed_acknowledged_transition_refuses_exact_wrapper_release", "lifetime_pipe_descriptor_contract", "run_lifetime_pipe_target", "failed_stages_and_acknowledgments", "launch_wrapper_refuses_former_harness_path", "malformed_barriers_refuse", "sa_nocldwait_refuses", "foreign_non_child_refuses", "concurrent_acquisitions_serialize", }, "crates/lazaret-linux/tests/capability-drop-helper.rs": {"main"}, "crates/lazaret-prepared-lower/tests/prepared_lower.rs": { "retained_fixed_child_bind_mount_is_refused_when_mount_setup_is_available" }, } RUST_FILE_LINE_LIMIT = 1000 RUST_FILE_SIZE_EXCEPTIONS = {} 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,", ) ) PROCESS_TRACE_EXIT_CODES = { "lazaret": 2, "lazaret-escalation-client": 2, "lazaret-git-sentry": 1, "lazaret-host-coordinator": 0, "lazaret-ignored-workspace": 1, "lazaret-launch-wrapper": 0, "lazaret-runtime-supervisor": 0, "lazaret-workspace-benchmark": 1, } 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 temporary_directory(prefix: str) -> tempfile.TemporaryDirectory[str]: VERIFICATION_TEMP_ROOT.mkdir(parents=True, exist_ok=True) return tempfile.TemporaryDirectory(prefix=prefix, dir=VERIFICATION_TEMP_ROOT) 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 run_physical(command: list[str], cwd: Path = ROOT) -> None: print(f"RUN {' '.join(command)}", flush=True) result = subprocess.run(command, cwd=cwd, check=False) if result.returncode == 77: print(f"SKIP {' '.join(command)}: physical prerequisites unavailable") return require(result.returncode == 0, f"physical test exited {result.returncode}") 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", ) observed_allowances = {} for path in workspace_rust_sources(metadata): relative = str(path.relative_to(ROOT)) source = path.read_text(errors="replace") functions = process_lint_allowances(relative, source) if functions: observed_allowances[relative] = functions require( observed_allowances == PROCESS_LINT_ALLOWANCES, "process-safety lint allowances must match exact reviewed functions", ) print("PASS workspace unsafe and process-control lint boundary") def process_lint_allowances(relative: str, source: str) -> set[str]: functions = set() for exemption in LINT_BYPASS.finditer(source): require( re.match(r"#\s*!", exemption.group()) is None, f"whole-file process lint exemption: {relative}", ) following = source[exemption.end() : exemption.end() + 400] function = re.match( r"\s*\)\s*\]\s*(?:#\[[^]]+\]\s*)*(?:pub\s+)?fn\s+([A-Za-z0-9_]+)\s*[<(]", following, ) require(function is not None, f"non-function process lint exemption: {relative}") functions.add(function.group(1)) return functions 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_rust_file_sizes(metadata: dict) -> None: sources = workspace_rust_sources(metadata) relative_sources = {str(path.relative_to(ROOT)): path for path in sources} line_counts = { relative: len(path.read_bytes().splitlines()) for relative, path in relative_sources.items() } for relative, responsibility in RUST_FILE_SIZE_EXCEPTIONS.items(): require( relative == Path(relative).as_posix() and not Path(relative).is_absolute() and relative.endswith(".rs"), f"malformed Rust file size exception path: {relative}", ) require( "\n" not in responsibility and len(responsibility.split()) >= 3, f"malformed Rust file size exception responsibility: {relative}", ) require(relative in relative_sources, f"stale Rust file size exception: {relative}") require( line_counts[relative] > RUST_FILE_LINE_LIMIT, f"stale Rust file size exception below threshold: {relative}", ) oversized = { relative: lines for relative, lines in line_counts.items() if lines > RUST_FILE_LINE_LIMIT and relative not in RUST_FILE_SIZE_EXCEPTIONS } require( not oversized, "Rust files exceed the reviewed responsibility threshold: " + ", ".join(f"{path} ({lines})" for path, lines in sorted(oversized.items())), ) print("PASS tracked Rust file responsibility size boundary") def audit_dependencies(metadata: dict) -> None: policy = load_toml(ROOT / "deny.toml") allowed_licenses = set(policy["licenses"]["allow"]) workspace_members = set(metadata["workspace_members"]) client = next(package for package in metadata["packages"] if package["name"] == "lazaret-client") client_dependencies = {dependency["name"] for dependency in client["dependencies"]} require( client_dependencies.isdisjoint( {"lazaret-host-coordinator", "lazaret-runtime-supervisor"} ), "Lazaret Client depends on Host Coordinator or Runtime Supervisor implementation", ) 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") or is_materialized_fuser(package), f"unapproved dependency source: {package['name']}", ) license_expression = package.get("license") or "" require( license_permitted(license_expression, 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 is_materialized_fuser(package: dict) -> bool: return ( package.get("name") == "fuser" and package.get("version") == "0.17.0" and Path(package.get("manifest_path", "")).resolve() == MATERIALIZED_FUSER_MANIFEST ) def license_permitted(expression: str, allowed: set[str]) -> bool: expression = re.sub(r"\s+WITH\s+[A-Za-z0-9.-]+", "", expression) expression = re.sub(r"\s*/\s*", " OR ", expression) return bool(expression) and any( all( term.strip(" ()") in allowed for term in re.split(r"\s+AND\s+", alternative) ) for alternative in re.split(r"\s+OR\s+", expression) ) def run_models() -> None: tlc = shutil.which("tlc") require(tlc is not None, "TLC must be installed on PATH") with temporary_directory("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) expected_execve = 2 if binary == "lazaret-launch-wrapper" else 1 require( execve_count == expected_execve, 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 temporary_directory("process-syscalls-") as directory: for binary, executable in sorted(binaries.items()): trace_base = Path(directory) / binary command = [ strace, "-ff", "-qq", "-e", "trace=process,wait4,waitid,rt_sigaction", "-o", str(trace_base), "--", str(executable), ] if binary == "lazaret-launch-wrapper": command.append("--trace-self-test") result = subprocess.run( command, 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: expected = PROCESS_TRACE_EXIT_CODES.get(binary) require( returncode == expected, f"{binary}: exercised path exited {returncode}, expected {expected}", ) def refresh_advisories() -> None: run(["cargo", "deny", "fetch"]) run(["cargo", "deny", "--frozen", "check", "advisories"]) def run_rust_tests() -> None: run(list(FUSER_PATCH_TEST_COMMAND)) run(list(NEXTEST_COMMAND)) run(list(ACQUISITION_TEST_COMMAND)) run(list(RECOVERY_PROCESS_TEST_COMMAND)) run(list(CAPABILITY_TEST_COMMAND)) run_physical(list(RUNTIME_COMPOSITION_TEST_COMMAND)) run_physical(list(NETWORK_RUNTIME_TEST_COMMAND)) run(list(DOCTEST_COMMAND)) def run_ignored_workspace_corpus(metadata: dict) -> None: binaries = build_workspace_binaries(metadata) with temporary_directory("ignored-workspace-corpus-") as directory: root = Path(directory) run_physical( [ sys.executable, str(ROOT / "tools/ignored_workspace_verifier.py"), "corpus", "--router", str(binaries["lazaret-ignored-workspace"]), "--git-sentry", str(binaries["lazaret-git-sentry"]), "--work-root", str(root / "work"), "--output", str(root / "result.json"), ] ) 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_ignored_workspace_corpus(metadata) run([sys.executable, "-m", "unittest", "discover", "-s", "tests/tooling"]) audit_workspace_lints(metadata) audit_rust_file_sizes(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())