diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 40ad08a7..87f382b7 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -38,10 +38,13 @@ jobs: key: isabelle-linux-x86-64-2025-2-a20a507bc7c1270d - name: Install proof sandbox run: | - if ! command -v bwrap >/dev/null 2>&1; then + if ! command -v bwrap >/dev/null 2>&1 || ! command -v fc-list >/dev/null 2>&1 || [ -z "$(fc-list --format='%{file}\n' | head -n 1)" ]; then sudo apt-get update - sudo apt-get install --no-install-recommends -y bubblewrap + sudo apt-get install --no-install-recommends -y bubblewrap fontconfig fonts-dejavu-core fi + test -d /etc/fonts + test -d /usr/share/fonts + test -n "$(fc-list --format='%{file}\n' | head -n 1)" - name: Acquire pinned Isabelle distribution run: uv run --project implementations/python --frozen python -m tools.isabelle_tool acquire - name: Resolve policy base revision diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index b82ab5a0..0dfc895f 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -58,6 +58,26 @@ The full repository gate is: uv tool run --from 'nox[uv]==2026.4.10' nox -f noxfile.py -s verify ``` +That gate includes a `participant-opacity-proof` lane, which replays the pinned +Isabelle proof offline. The lane runs on Linux x86_64 only. It needs +`bubblewrap` to enforce the offline replay, and a fontconfig setup with at least +one installed font, because Isabelle starts a JVM that will not run without one: + +```shell +sudo apt-get install bubblewrap fontconfig fonts-dejavu-core +``` + +The proof tool checks this fontconfig runtime before entering the sandbox and +reports a missing prerequisite separately from a kernel rejection. Run the +gate on Linux, or rely on continuous integration, when your workstation is +another platform. + +Some Linux security policies also deny unprivileged user or network namespaces. +The proof tool reports that condition as unavailable bubblewrap isolation and +does not retry without the network sandbox. Use an administrator-approved host +policy for bubblewrap or rely on continuous integration; do not disable the +offline boundary to make the lane pass. + Run the change-aware local gate while iterating: ```shell diff --git a/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md b/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md new file mode 100644 index 00000000..2c1b0e6e --- /dev/null +++ b/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md @@ -0,0 +1,52 @@ +# Issue 1109 / ASR-535 Isabelle Sandbox Portability + +Date: 2026-08-11 + +Issue: #1109. Requirement: ASR-535. Related: #963. + +## Reproduced gap + +The checksum-pinned Isabelle2025-2 distribution was acquired on Ubuntu 24.04 +x86_64 and started inside the repository's bubblewrap network namespace. The +kernel replay stopped before loading the fixed session with `Fontconfig head is +null, check your fonts or fonts configuration`. + +The sandbox already exposes `/etc/fonts` and `/usr/share/fonts`, but creates an +otherwise empty `/usr/share`. On Ubuntu releases where `/etc/fonts/conf.d` +entries resolve into `/usr/share/fontconfig`, the fixed runtime allowlist omits +data required by the pinned prover. Ubuntu 22.04 instead keeps that configuration +under `/etc/fonts`, so `/usr/share/fontconfig` is a distribution-specific, +optional path. A minimal Ubuntu image can also omit the fontconfig runtime +entirely because the canonical workflow installs only bubblewrap. The result is +host-image-dependent proof admission even though theorem sources and the prover +archive are unchanged. + +## Decision + +Install bubblewrap and fontconfig as explicit canonical-runner prerequisites, +require the cross-release `/etc/fonts` and `/usr/share/fonts` directories before +sandbox entry, and add the optional `/usr/share/fontconfig` directory to the +fixed, read-only system-runtime allowlist when the host provides it. +Do not bind the host root, user home, repository workspace, network, ambient +environment, or any mutable proof input. Existing paths remain conditional so +minimal distributions without that directory keep the same command shape. + +The allowlist membership is covered by a focused regression, while the +canonical Ubuntu 22.04 job replays the checksum-pinned archive under bubblewrap +network isolation. Ubuntu 24.04 supplied the reproduced fontconfig layout, but +is not the canonical replay host because its default namespace policy can deny +bubblewrap setup. The proof evidence digest and theorem semantics must remain +unchanged. + +If the host denies bubblewrap namespace setup, the runner must report a stable +sandbox-unavailable error rather than classify pre-prover output as a kernel +rejection. It must not retry with host networking. Ubuntu installations with +restrictive unprivileged-user-namespace policy use an administrator-approved +bubblewrap policy or the canonical CI host. + +## Nonclaims + +This repairs Linux distribution portability for the declared canonical proof +lane. It does not make arbitrary Isabelle installations portable, authorize a +different prover or archive, expand the theorem claim, or replace the existing +checksum, resource, filesystem, and offline-execution controls. diff --git a/docs/requirements/ASR-535/requirement.md b/docs/requirements/ASR-535/requirement.md index b0d084ce..1f2f9fc6 100644 --- a/docs/requirements/ASR-535/requirement.md +++ b/docs/requirements/ASR-535/requirement.md @@ -52,3 +52,5 @@ ADR-081 governs relation discipline and current tests provide bounded evidence, - IMPLEMENTS → PROOF `specs/formal/participant-semantics/isabelle/Participant_Opacity.thy` (Kernel-checked participant-opacity theorem) - TESTS → TEST `implementations/python/tests/test_issue_963_participant_opacity_proof.py` (Issue 963 participant-opacity proof integration tests) - VERIFIES → PROOF `specs/formal/participant-semantics/participant-opacity-proof-evidence.json` (Participant-opacity proof evidence record) +- IMPLEMENTS → GITHUB_ISSUE `1109` (Make the offline Isabelle sandbox portable on Ubuntu) +- DOCUMENTS → DOCUMENTATION `docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md` (Pinned proof-runtime allowlist decision) diff --git a/implementations/python/tests/test_issue_1109_proof_workflow.py b/implementations/python/tests/test_issue_1109_proof_workflow.py new file mode 100644 index 00000000..d14aae55 --- /dev/null +++ b/implementations/python/tests/test_issue_1109_proof_workflow.py @@ -0,0 +1,21 @@ +"""ASR-535 regression guard for the canonical proof sandbox setup.""" + +from pathlib import Path + +import yaml + +REPO_ROOT = Path(__file__).resolve().parents[3] + + +def test_canonical_workflow_installs_the_offline_proof_runtime() -> None: + workflow = yaml.safe_load((REPO_ROOT / ".github" / "workflows" / "ci.yml").read_text(encoding="utf-8")) + steps = workflow["jobs"]["verify"]["steps"] + proof_runtime = next(step["run"] for step in steps if step.get("name") == "Install proof sandbox") + + assert "command -v bwrap" in proof_runtime + assert "command -v fc-list" in proof_runtime + assert "bubblewrap fontconfig fonts-dejavu-core" in proof_runtime + assert "test -d /etc/fonts" in proof_runtime + assert "test -d /usr/share/fonts" in proof_runtime + assert "test -n" in proof_runtime + assert "fc-list --format=" in proof_runtime diff --git a/implementations/python/tests/test_issue_963_participant_opacity_proof.py b/implementations/python/tests/test_issue_963_participant_opacity_proof.py index f6946830..ce066d89 100644 --- a/implementations/python/tests/test_issue_963_participant_opacity_proof.py +++ b/implementations/python/tests/test_issue_963_participant_opacity_proof.py @@ -7,6 +7,7 @@ import json from copy import deepcopy from pathlib import Path +from types import SimpleNamespace from urllib.error import URLError import pytest @@ -31,8 +32,12 @@ ) from tools.isabelle_tool import ( ISABELLE_PROCESS_ADDRESS_SPACE_LIMIT_MIB, + ISABELLE_REQUIRED_FONTCONFIG_PATHS, + ISABELLE_SYSTEM_RUNTIME_PATHS, + _bubblewrap_setup_failed, _proof_process_limits, _proof_sandbox_command, + _require_fontconfig_runtime, ) REPO_ROOT = Path(__file__).resolve().parents[3] @@ -123,6 +128,118 @@ def test_proof_sandbox_exposes_only_fixed_inputs_runtime_and_private_state() -> assert command[-2:] == ["-D", "/workspace/session"] +def test_proof_sandbox_allowlists_fontconfig_symlink_targets() -> None: + assert Path("/etc/fonts") in ISABELLE_SYSTEM_RUNTIME_PATHS + assert Path("/usr/share/fontconfig") in ISABELLE_SYSTEM_RUNTIME_PATHS + assert Path("/usr/share/fonts") in ISABELLE_SYSTEM_RUNTIME_PATHS + assert set(ISABELLE_REQUIRED_FONTCONFIG_PATHS) <= set(ISABELLE_SYSTEM_RUNTIME_PATHS) + assert Path("/usr/share/fontconfig") not in ISABELLE_REQUIRED_FONTCONFIG_PATHS + + +def test_proof_runtime_requires_complete_fontconfig_data(tmp_path: Path) -> None: + existing = tuple(tmp_path / name for name in ("etc-fonts", "share-fontconfig", "share-fonts")) + for path in existing: + path.mkdir() + + _require_fontconfig_runtime(existing, font_query=lambda: True) + + existing[-1].rmdir() + with pytest.raises(isabelle_tool.IsabelleToolError, match="fontconfig runtime is required"): + _require_fontconfig_runtime(existing, font_query=lambda: True) + + +def test_proof_runtime_requires_a_discoverable_font(tmp_path: Path) -> None: + existing = tuple(tmp_path / name for name in ("etc-fonts", "share-fonts")) + for path in existing: + path.mkdir() + + with pytest.raises(isabelle_tool.IsabelleToolError, match="fontconfig runtime is required"): + _require_fontconfig_runtime(existing, font_query=lambda: False) + + +def test_fontconfig_query_requires_a_successful_nonempty_listing( + monkeypatch: pytest.MonkeyPatch, + tmp_path: Path, +) -> None: + font_list = tmp_path / "fc-list" + font_list.write_text("stub", encoding="ascii") + font_list.chmod(0o755) + + monkeypatch.setattr( + isabelle_tool.subprocess, + "run", + lambda *_args, **_kwargs: SimpleNamespace(returncode=0, stdout=b"/usr/share/fonts/example.ttf\n"), + ) + assert isabelle_tool._fontconfig_has_fonts(font_list) is True + + monkeypatch.setattr( + isabelle_tool.subprocess, + "run", + lambda *_args, **_kwargs: SimpleNamespace(returncode=0, stdout=b""), + ) + assert isabelle_tool._fontconfig_has_fonts(font_list) is False + + +def test_proof_replay_checks_fontconfig_before_session_entry( + monkeypatch: pytest.MonkeyPatch, + tmp_path: Path, +) -> None: + original_is_file = Path.is_file + + def reject_missing_fontconfig() -> None: + raise isabelle_tool.IsabelleToolError("fontconfig test sentinel") + + monkeypatch.setattr(isabelle_tool, "require_isabelle", lambda _repo_root: tmp_path) + monkeypatch.setattr( + Path, + "is_file", + lambda path: path == Path("/usr/bin/bwrap") or original_is_file(path), + ) + monkeypatch.setattr( + isabelle_tool, + "_require_fontconfig_runtime", + reject_missing_fontconfig, + ) + + with pytest.raises(isabelle_tool.IsabelleToolError, match="fontconfig test sentinel"): + isabelle_tool.run_isabelle_build(tmp_path) + + +def test_proof_replay_distinguishes_sandbox_setup_from_kernel_rejection( + monkeypatch: pytest.MonkeyPatch, + tmp_path: Path, +) -> None: + session_root = tmp_path / isabelle_tool.ISABELLE_SESSION_RELATIVE_PATH + session_root.mkdir(parents=True) + original_is_file = Path.is_file + + monkeypatch.setattr(isabelle_tool, "require_isabelle", lambda _repo_root: tmp_path / "isabelle") + monkeypatch.setattr( + Path, + "is_file", + lambda path: path == Path("/usr/bin/bwrap") or original_is_file(path), + ) + monkeypatch.setattr(isabelle_tool, "_require_fontconfig_runtime", lambda: None) + + def completed_with(output: bytes): + def fake_run(*_args: object, stdout: object, **_kwargs: object) -> SimpleNamespace: + stdout.write(output) + return SimpleNamespace(returncode=1) + + return fake_run + + assert _bubblewrap_setup_failed(" bwrap: loopback setup denied\n") is True + assert _bubblewrap_setup_failed("*** Isabelle theorem failure\n") is False + + monkeypatch.setattr(isabelle_tool.subprocess, "run", completed_with(b"bwrap: network namespace denied\n")) + with pytest.raises(isabelle_tool.IsabelleToolError, match="bubblewrap network isolation is unavailable"): + isabelle_tool.run_isabelle_build(tmp_path) + + monkeypatch.setattr(isabelle_tool.subprocess, "run", completed_with(b"*** Isabelle theorem failure\n")) + with pytest.raises(isabelle_tool.IsabelleToolError, match="Isabelle kernel rejected"): + isabelle_tool.run_isabelle_build(tmp_path) + + def test_proof_process_limit_enforces_per_process_address_space(monkeypatch: pytest.MonkeyPatch) -> None: calls: list[tuple[int, tuple[int, int]]] = [] monkeypatch.setattr(isabelle_tool.resource, "setrlimit", lambda kind, limits: calls.append((kind, limits))) diff --git a/specs/formal/participant-semantics/participant-opacity-proof-evidence.json b/specs/formal/participant-semantics/participant-opacity-proof-evidence.json index fc916be9..c1541725 100644 --- a/specs/formal/participant-semantics/participant-opacity-proof-evidence.json +++ b/specs/formal/participant-semantics/participant-opacity-proof-evidence.json @@ -292,7 +292,7 @@ }, { "path": "tools/isabelle_tool.py", - "digest": "sha256:5100ea993e91b07bb3ac764642fd6ca110e477882b35aba5c49403f314133c85" + "digest": "sha256:64a6c3190e2116f760de09969f978240ab3582173cc3765b03fb596cf52cd7c1" } ] }, diff --git a/tools/isabelle_tool.py b/tools/isabelle_tool.py index acc82e0b..ff976a51 100644 --- a/tools/isabelle_tool.py +++ b/tools/isabelle_tool.py @@ -11,6 +11,7 @@ import sys import tarfile import tempfile +from collections.abc import Callable from pathlib import Path from urllib.error import HTTPError, URLError from urllib.request import urlopen @@ -31,6 +32,7 @@ ISABELLE_ARCHIVE_BYTES = 1_228_480_874 ISABELLE_SESSION = "Participant_Opacity" ISABELLE_SESSION_RELATIVE_PATH = Path("specs/formal/participant-semantics/isabelle") +ISABELLE_LOCALE = "C.UTF-8" ISABELLE_BUILD_TIMEOUT_SECONDS = 600 ISABELLE_OUTPUT_LIMIT_BYTES = 64 * 1024 ISABELLE_FILE_LIMIT_BYTES = 4 * 1024 * 1024 * 1024 @@ -45,6 +47,7 @@ Path("/usr/lib"), Path("/usr/lib64"), Path("/usr/share/locale"), + Path("/usr/share/fontconfig"), Path("/usr/share/fonts"), Path("/usr/share/zoneinfo"), Path("/lib"), @@ -53,6 +56,12 @@ Path("/etc/ld.so.cache"), Path("/var/cache/fontconfig"), ) +ISABELLE_REQUIRED_FONTCONFIG_PATHS = ( + Path("/etc/fonts"), + Path("/usr/share/fonts"), +) +ISABELLE_FONTCONFIG_LIST = Path("/usr/bin/fc-list") +ISABELLE_FONTCONFIG_QUERY_TIMEOUT_SECONDS = 10 _DOWNLOAD_CHUNK_BYTES = 1024 * 1024 @@ -210,7 +219,7 @@ def expected_isabelle_result() -> dict[str, object]: "result": "kernel-checked", "network": "blocked-by-bubblewrap-network-namespace", "filesystem": "allowlisted-runtime-session-and-private-state-only", - "locale": "C.UTF-8", + "locale": ISABELLE_LOCALE, "platform_boundary": "linux-x86_64", } encoded = json.dumps(result, ensure_ascii=False, separators=(",", ":"), sort_keys=True).encode("utf-8") @@ -287,10 +296,10 @@ def _proof_sandbox_command( "/state/isabelle-user", "--setenv", "LANG", - "C.UTF-8", + ISABELLE_LOCALE, "--setenv", "LC_ALL", - "C.UTF-8", + ISABELLE_LOCALE, "--setenv", "TZ", "UTC", @@ -307,6 +316,43 @@ def _proof_sandbox_command( return command +def _fontconfig_has_fonts(font_list: Path = ISABELLE_FONTCONFIG_LIST) -> bool: + """Return whether the fixed host fontconfig tool finds an installed font.""" + + if not font_list.is_file() or not os.access(font_list, os.X_OK): + return False + try: + completed = subprocess.run( + [str(font_list), "--format=%{file}\\n"], + stdin=subprocess.DEVNULL, + stdout=subprocess.PIPE, + stderr=subprocess.DEVNULL, + check=False, + timeout=ISABELLE_FONTCONFIG_QUERY_TIMEOUT_SECONDS, + env={"LANG": ISABELLE_LOCALE, "LC_ALL": ISABELLE_LOCALE}, + ) + except (OSError, subprocess.TimeoutExpired): + return False + return completed.returncode == 0 and bool(completed.stdout.strip()) + + +def _require_fontconfig_runtime( + paths: tuple[Path, ...] = ISABELLE_REQUIRED_FONTCONFIG_PATHS, + *, + font_query: Callable[[], bool] = _fontconfig_has_fonts, +) -> None: + """Fail before sandbox entry when the pinned prover's font runtime is absent.""" + + if any(not path.is_dir() for path in paths) or not font_query(): + raise IsabelleToolError("fontconfig runtime is required for offline proof replay") + + +def _bubblewrap_setup_failed(output: str) -> bool: + """Return whether bubblewrap failed before the fixed prover could start.""" + + return output.lstrip().startswith("bwrap:") + + def run_isabelle_build(repo_root: Path = REPO_ROOT) -> dict[str, object]: """Kernel-check the fixed session in a network-isolated, bounded process.""" @@ -314,6 +360,7 @@ def run_isabelle_build(repo_root: Path = REPO_ROOT) -> dict[str, object]: bwrap = Path("/usr/bin/bwrap") if not bwrap.is_file(): raise IsabelleToolError("bubblewrap is required to enforce offline proof replay") + _require_fontconfig_runtime() session_root = (repo_root / ISABELLE_SESSION_RELATIVE_PATH).resolve() if not session_root.is_dir() or repo_root.resolve() not in session_root.parents: raise IsabelleToolError("the fixed Isabelle session root is unavailable") @@ -354,6 +401,8 @@ def run_isabelle_build(repo_root: Path = REPO_ROOT) -> dict[str, object]: raise IsabelleToolError("Isabelle proof replay exceeded its wall-time bound") from exc output = _read_bounded_output(output_path) if completed.returncode != 0: + if _bubblewrap_setup_failed(output): + raise IsabelleToolError("bubblewrap network isolation is unavailable for offline proof replay") failure_tail = output.strip()[-4096:] detail = f":\n{failure_tail}" if failure_tail else "" raise IsabelleToolError(f"Isabelle kernel rejected the fixed proof session{detail}")