Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
69 changes: 69 additions & 0 deletions .github/workflows/macos-visibility-research.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,69 @@
name: macOS visibility research

on:
pull_request:
paths:
- '.github/workflows/macos-visibility-research.yml'
- 'experimental/127-macos-contract/**'
- 'experimental/127-macos-visibility/**'
workflow_dispatch:

permissions:
contents: read

jobs:
synthetic-visibility:
name: macOS fileport and visibility fixtures (${{ matrix.runner }})
timeout-minutes: 15
strategy:
fail-fast: false
matrix:
runner: [macos-15, macos-15-intel]
runs-on: ${{ matrix.runner }}
steps:
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
with:
persist-credentials: false
- name: Record toolchain
run: |
sw_vers -productVersion
/usr/bin/clang --version | head -n 1
/usr/sbin/lsof -v 2>&1 | grep -E '^ *revision:' || true
python3 -V
if test -x /usr/bin/sandbox-exec; then echo 'sandbox-exec present'; else echo 'sandbox-exec absent'; fi
- name: Deterministic evaluator and actor tests
env:
RESEARCH_TMP_ROOT: ${{ runner.temp }}
run: |
if python3 -I -B -W error::ResourceWarning experimental/127-macos-visibility/test_visibility.py > "$RUNNER_TEMP/visibility-tests.log" 2>&1; then
echo 'visibility tests passed'
else
echo 'visibility tests failed; raw diagnostics kept private'
exit 1
fi
if python3 -I -B -W error::ResourceWarning experimental/127-macos-contract/test_inherit.py > "$RUNNER_TEMP/inherit-tests.log" 2>&1; then
echo 'inherit tests passed'
else
echo 'inherit tests failed; raw diagnostics kept private'
exit 1
fi
# Prints only the allowlisted public summary. The raw result (paths,
# PIDs, service names, stderr) stays in RUNNER_TEMP and is not uploaded.
# A not_executed scenario, failed control or failed cleanup exits
# nonzero: there is no green result for an unmeasured scope.
- name: Measure fileport, hidden-sharer and sandbox visibility fixtures
run: |
root="$(mktemp -d "$RUNNER_TEMP/codex-127v-XXXXXX")"
chmod 700 "$root"
python3 -I -B experimental/127-macos-visibility/visibility.py \
--scratch-root "$root" --result "$RUNNER_TEMP/visibility.json" 2> "$RUNNER_TEMP/visibility.stderr"
- name: Record bounded evidence summary
if: ${{ !cancelled() }}
run: |
raw="$RUNNER_TEMP/visibility.json"
if [ ! -f "$raw" ]; then
echo '{"present": false}'
exit 0
fi
shasum -a 256 "$raw" | cut -d ' ' -f 1
python3 -I -B experimental/127-macos-visibility/visibility.py --summarize "$raw"
105 changes: 105 additions & 0 deletions experimental/127-macos-visibility/HANDOFF.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,105 @@
# Handoff: proposed follow-ups outside this directory

Sections 1 and 2 propose follow-ups outside this directory. The research CI
in section 3 is integrated; product policy changes remain proposals only.
`docs/macos-owner-contract.md`, `experimental/127-macos-contract/` and
`experimental/127-macos-prerequisites/` were read and left unchanged. Nothing
here reproduces a real Codex process or a wrong signal to a real PID.

## 1. `docs/macos-owner-contract.md` (proposal)

Section 4, gap table:

| Row | Proposed status |
| --- | --- |
| Inherited FD / Mach fileport passing | Measured (same-user synthetic, macOS 27.0.1 arm64, APFS). Lock held while the description is only in a queued Mach message, with no opener in `lsof` and no fileport in `PROC_PIDLISTFILEPORTS`. A fileport in a task's port space is printed as FD `fp.` with the description's flags. The receiver that never called `flock` becomes the sole holder with the bit. See `experimental/127-macos-visibility/README.md`. |
| Inherited FD / shared description with a hidden sharer | Measured as a model (#139 M2 style omission). With `SCM_RIGHTS` (either sharer hidden) and with fork (child hidden), the filter returns `not_excluded` for the visible sharer, which really shares the locked description. The lock stays held after that sharer releases. Recorded as `release_incomplete_due_to_hidden_reference`: one sharer's release does not release the lock. It is not a non-holder misidentified as the holder. |
| Permission / same-user target under `sandbox-exec` | Measured for `(allow default)` and one deny-default profile: target fully visible to an unsandboxed observer. Hardened runtime and App Sandbox not covered. |
| Permission / observer running sandboxed | Measured for five profiles, against a positive control with a full contract. `(deny process-info-pidfdinfo)` and a deny-default profile give exit 1, empty stdout and empty stderr, identical to "no openers". Detected here only by cross-checks (held probe, canary holder). Selective omission of some targets not covered and not detected by these checks. |

Section 2, counterexample rows to add:

| Counterexample | What the observer sees | Source |
| --- | --- | --- |
| Description in flight in a Mach message (fileport) | Held probe, no opener, no fileport listed anywhere | `127-macos-visibility` |
| Description held only as a fileport in a task's port space | `lsof` FD `fp.` with `FWASLOCKED`; no numeric descriptor | `127-macos-visibility` |
| Fileport converted by a process that never called `flock` | Receiver carries the bit and is the sole holder | `127-macos-visibility` |
| Hidden second sharer of the locked description | Visible sharer is a real sharer, `not_excluded`; its release leaves the lock held | `127-macos-visibility` |
| Restricted observer (sandbox) | Exit 1, empty output, no stderr: indistinguishable from "no openers" | `127-macos-visibility` |

Keep the hidden-sharer row separate from the existing former-holder row: the
former holder is a non-holding process that the filter does not refuse.

Section 1 currently lists "Descriptor passing (`SCM_RIGHTS`, Mach fileports)"
as not excluded by the source reading. That stays true: these fixtures show
the OS mechanism, not that Codex uses it.

## 2. Candidate inputs for option (b), not adopted

These are design candidates for the separately reviewed (b) change. Nothing
is implemented in `src/`. Adopting them, and accepting the residual risks,
remain user decisions.

1. Parse `lsof +fg` strictly. Any non-numeric FD, including `fp.`, makes the
scan `unknown`. It must not be skipped and must not count as a descriptor.
2. A held probe with no visible opener is `unknown`, never "stale" or clean.
3. A visibility canary: a descriptor the observer owns and must see exactly
in the same scan mode. A missing canary is `unknown`. It catches a
restriction of the whole observer. It does not detect selective omission.
4. Residuals that stay documented with (b):
- a former holder that keeps its FD;
- a hidden sharer of one description, including fileport and
`SCM_RIGHTS` receivers that never called `flock`, where one sharer's
release does not release the lock;
- a description in flight;
- clean whole-record or selective omission.

## 3. CI integration

The integrating reviewer added `.github/workflows/macos-visibility-research.yml`
from the handoff proposal. Hosted macOS 15 ARM/Intel jobs have passed; consult
the PR checks for the result at each revision.

- Runners: `macos-15` and `macos-15-intel`, with read-only `contents`
permission and checkout pinned to the same SHA as the existing macOS
workflow.
- Steps: the deterministic tests of this directory and of
`127-macos-contract`, then one measurement run.
- Summary: the SHA-256 of the raw result plus `visibility.py --summarize`
output.
- Privacy: the measurement prints an allowlisted public summary. Actor and
test diagnostics stay private; test steps print fixed pass/fail status.
Raw results and logs are not uploaded.

The original proposal was checked with `git apply --check` and YAML parsing.
The integrated workflow also hides raw test/measurement stderr. `--summarize`
was run locally against a result; hosted execution is recorded separately.

A `not_executed` scenario, a failed control, an incomplete wait or a failed
cleanup exits nonzero. There is no green result for an unmeasured scope. If a
hosted runner cannot run something, the public summary names the
`not_executed` kind or the failure kind, and the unmeasured scope must be
reported from that.

Hosted-runner limits to preserve:

- `bootstrap_check_in` with a dynamic name worked in an interactive user
session here. A hosted runner's launchd domain may refuse it. The receiver
then emits `failed`, and the run fails visibly.
- `sandbox-exec` may be unusable inside the runner's own confinement. The
sandbox scenarios are then `not_executed`, which keeps `ok` false.
- A loaded runner can push an `lsof` call over its 5 s bound. This happened
once locally (run 5). It is recorded as incomplete, never stopped, and
fails the run.
- The expected tables were measured only on macOS 27 / lsof 4.91. Kernel 24.x
may differ. A mismatch there is data, not a test bug.

## 4. Policy decisions left to the user

- Whether the hidden-sharer release and in-flight fileport shapes are
acceptable residuals for (b), or move macOS toward (c).
- Whether (b) should adopt the canary and the held-without-opener rule as
candidates, knowing they do not detect selective omission.

The research CI is already included. `not_executed` remains a failure; any
future change to that requirement needs a separate review.
Loading
Loading