#!/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", "--filterset", "not binary(capability-drop-helper) and not binary(acquisition)", ) 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", ) 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_ALLOWANCES = { "crates/lazaret-linux/src/process.rs": { "append_to", "send_signal", "acquire", "private_role_command", "require_reapable_sigchld", "cleanup_sigchld_probe", "fail_sigchld_probe", "reap", "acquire_spawned_child", "verify_direct_child_pidfd", "fail_before_pidfd", "fail_after_pidfd_closed", "recover_process", "current_process_identity", "append_parent_identity", "exec_target", }, "crates/lazaret-linux/tests/acquisition.rs": { "run_acquisition", "successful_acquisition", "failed_stages_and_acknowledgments", "production_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"}, } 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", ) 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_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 "" 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 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 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) 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 tempfile.TemporaryDirectory(prefix="lazaret-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: 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(ACQUISITION_TEST_COMMAND)) run(list(CAPABILITY_TEST_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())