571 lines
19 KiB
Python
571 lines
19 KiB
Python
#!/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)
|
|
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())
|