Formalize pull request target checkout policy

Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>
pelikhan · Oct 7, 2026 · Oct 7, 2026 · Oct 7, 2026 · Oct 7, 2026 · Oct 7, 2026
commit 53d82776dc9fa60b55ac03bf26050f3eec9553e8
diff --git a/specs/compiler-threat-detection-changelog.md b/specs/compiler-threat-detection-changelog.md
@@ -16,6 +16,7 @@ This changelog records the version history and the dated mapping audits for `spe
 
 | Version | Change |
 |---|---|
+| 1.0.43 | Clarified CTR-008 for the scoped `pull_request_target` checkout policy: exact literal allowlist matching, warning-only risk acknowledgment, and rejection of configured `fetch` values. |
 | 1.0.42 | Audit-only clarification that same-repository bot PR checkout authorization is a runtime trust control governed by Security Architecture Specification RS-05a, not a new compiler threat rule. |
 | 1.0.41 | Added CTR-031 for strict rejection and non-strict warning of `tools.github.private-to-public-flows`, which can expose private data through public logs or destinations. |
 | 1.0.40 | Added CTR-030 for PR-base provenance of activation sparse checkout before loading imports or skills; preserves non-PR refs and the `GITHUB_TOKEN` same-repo fallback guard. |

diff --git a/specs/compiler-threat-detection-spec.md b/specs/compiler-threat-detection-spec.md
@@ -7,7 +7,7 @@ sidebar:
 
 # GitHub Actions Compiler Threat Detection Specification
 
-**Version**: 1.0.42
+**Version**: 1.0.43
 **Status**: Candidate Recommendation  
 **Latest Version**: https://github.com/github/gh-aw/blob/main/specs/compiler-threat-detection-spec.md  
 **Editors**: GitHub Next (GitHub, Inc.)
@@ -32,6 +32,7 @@ Each version maps to the minimum compatible binary. A version change MUST update
 
 | Versions | Minimum gh-aw | Compatibility |
 |---|---:|---|
+| `1.0.43` | `v0.87.9` | Clarifies CTR-008 trusted `pull_request_target` checkouts: acknowledgment suppresses only the trigger warning, allowlisted checkouts require an exact literal repository/ref pair, and any configured `fetch` is rejected. |
 | `1.0.42` | `v0.87.9` | Audit-only; same-repository bot PR checkout authorization is a runtime trust control governed by the security architecture specification, not a new compiler threat rule. |
 | `1.0.41` | `v0.87.9` | Adds CTR-031; private-to-public flow opt-outs are rejected in strict mode and warned in non-strict mode because they can expose private data through public logs or destinations. |
 | `1.0.40` | `v0.87.9` | Adds CTR-030; activation sparse checkouts use the PR base SHA for pull-request and review events before loading runtime imports or skills. |
@@ -81,7 +82,7 @@ Each rule has a stable `CTR-*` ID, threat class, trigger, compiler action, diagn
 - **CTR-005 Unsafe Output Route**: Reject direct write paths that bypass safe outputs.
 - **CTR-006 Template Injection**: Reject user-controlled expressions directly embedded in shell commands.
 - **CTR-007 Markdown Content Security**: Detect unsafe external markdown, including obfuscation, scripts, and social engineering.
-- **CTR-008 Pull Request Target Safety**: Reject unsafe `pull_request_target` checkout patterns.
+- **CTR-008 Pull Request Target Safety**: For `pull_request_target`, strict mode MUST warn about elevated permissions and secret access unless `on.pull_request_target.acknowledge-risk` is `true`. This acknowledgment suppresses only that warning; it MUST NOT authorize a checkout or suppress checkout diagnostics. An explicit `checkout: false` is accepted. Otherwise, every configured checkout MUST independently use either the supported base-repository/base-ref form or an exact, case-sensitive literal repository/ref pair in `on.pull_request_target.allowed-checkouts`. The allowlist path MUST reject expressions, wildcard refs, `refs/pull/...` refs, wiki checkouts, and omitted external refs. Neither the base-checkout nor allowlist path may accept any non-empty `fetch` value. An omitted checkout configuration is not equivalent to explicit `checkout: false`. In strict mode an unsafe checkout MUST be rejected; in non-strict mode it MUST produce a warning.
 - **CTR-009 Shell Expansion in Safe-Outputs**: Reject dangerous shell expansion in safe-output scripts.
 - **CTR-010 Expression Safety Allowlist**: Reject unauthorized or multiline GitHub Actions expressions.
 - **CTR-011 Network Firewall Configuration**: Reject missing firewall prerequisites and strict-mode wildcard domains.
@@ -153,7 +154,7 @@ Every active rule MUST map to implementation and test coverage. References are p
 | CTR-005 Unsafe Output Route | safe-output compiler/validation; setup safe-output and manifest helpers | safe-output and setup helper tests |
 | CTR-006 Template Injection | template/heredoc validation, `mcp_renderer_guard.go` | template-injection and MCP tests |
 | CTR-007 Markdown Content Security | `markdown_security_scanner.go`, `pull_request_target_validation.go` | corresponding workflow and sanitizer tests |
-| CTR-008 Pull Request Target Safety | `markdown_security_scanner.go`, `pull_request_target_validation.go` | corresponding workflow and sanitizer tests |
+| CTR-008 Pull Request Target Safety | `pkg/workflow/pull_request_target_validation.go` | `pkg/workflow/pull_request_target_validation_test.go`; `specs/workflow-security/PullRequestTargetCheckout.tla` |
 | CTR-009 Shell Expansion in Safe-Outputs | safe-output shell/push validation, expression validation, firewall validation | corresponding workflow tests |
 | CTR-010 Expression Safety Allowlist | safe-output shell/push validation, expression validation, firewall validation | corresponding workflow tests |
 | CTR-011 Network Firewall Configuration | safe-output shell/push validation, expression validation, firewall validation | corresponding workflow tests |
@@ -196,7 +197,7 @@ Each active rule MUST have at least one deterministic test that covers its prima
 | **T-CTR-005** | CTR-005 Unsafe Output Route | Reject direct write paths that bypass safe outputs | Reject direct write paths that bypass safe outputs. | `CTR-005` |
 | **T-CTR-006** | CTR-006 Template Injection | Reject user-controlled expressions directly embedded in shell commands | Reject user-controlled expressions directly embedded in shell commands. | `CTR-006` |
 | **T-CTR-007** | CTR-007 Markdown Content Security | Detect unsafe external markdown, including obfuscation, scripts, and social engineering | Detect unsafe external markdown, including obfuscation, scripts, and social engineering. | `CTR-007` |
-| **T-CTR-008** | CTR-008 Pull Request Target Safety | Reject unsafe `pull_request_target` checkout patterns | Reject unsafe `pull_request_target` checkout patterns. | `CTR-008` |
+| **T-CTR-008** | CTR-008 Pull Request Target Safety | A `pull_request_target` workflow acknowledges trigger risk, configures base or external checkouts, or sets `fetch` | Suppress only the strict trigger warning when acknowledged; accept only explicit disablement, trusted base checkouts, or exact allowlisted literal repository/ref pairs without `fetch`; otherwise reject in strict mode and warn in non-strict mode. | `CTR-008` |
 | **T-CTR-009** | CTR-009 Shell Expansion in Safe-Outputs | Reject dangerous shell expansion in safe-output scripts | Reject dangerous shell expansion in safe-output scripts. | `CTR-009` |
 | **T-CTR-010** | CTR-010 Expression Safety Allowlist | Reject unauthorized or multiline GitHub Actions expressions | Reject unauthorized or multiline GitHub Actions expressions. | `CTR-010` |
 | **T-CTR-011** | CTR-011 Network Firewall Configuration | Reject missing firewall prerequisites and strict-mode wildcard domains | Reject missing firewall prerequisites and strict-mode wildcard domains. | `CTR-011` |

diff --git a/specs/workflow-security/PullRequestTargetCheckout.cfg b/specs/workflow-security/PullRequestTargetCheckout.cfg
@@ -0,0 +1,10 @@
+CONSTANT Fault = "none"
+SPECIFICATION Spec
+INVARIANTS
+    TypeOK
+    NoUntrustedCheckoutAcceptance
+    ExactTrustedCheckoutClasses
+    WarningAcknowledgmentIsScoped
+    CheckoutDiagnosticsAreIndependentOfAcknowledgment
+    OtherTriggersHaveNoDiagnostics
+CHECK_DEADLOCK FALSE
diff --git a/specs/workflow-security/PullRequestTargetCheckout.tla b/specs/workflow-security/PullRequestTargetCheckout.tla
@@ -0,0 +1,81 @@
+------------------------- MODULE PullRequestTargetCheckout -------------------------
+EXTENDS FiniteSets, TLC
+
+CONSTANT Fault
+ASSUME Fault \in {"none", "acknowledgment-bypasses-checkout", "fetch-bypasses-checkout"}
+
+Triggers == {"pull_request_target", "other"}
+Checkouts == {"checkout-disabled", "checkout-omitted", "base",
+              "external-allowlisted-literal", "external-unlisted-literal",
+              "expression", "wildcard", "pull-ref", "external-ref-omitted", "wiki"}
+Fetches == {"none", "ordinary-ref", "pull-ref", "expression", "wildcard"}
+
+VARIABLES trigger, strictMode, acknowledged, checkout, fetch
+vars == <<trigger, strictMode, acknowledged, checkout, fetch>>
+
+CheckoutNotExplicitlyDisabled == checkout # "checkout-disabled"
+ExpectedTrustedCheckout ==
+    checkout = "checkout-disabled" \/
+    (CheckoutNotExplicitlyDisabled /\ fetch = "none" /\
+      checkout \in {"base", "external-allowlisted-literal"})
+
+ObservedTrustedCheckout ==
+    ExpectedTrustedCheckout \/
+    (Fault = "acknowledgment-bypasses-checkout" /\
+      acknowledged /\ CheckoutNotExplicitlyDisabled) \/
+    (Fault = "fetch-bypasses-checkout" /\ CheckoutNotExplicitlyDisabled /\
+      fetch # "none" /\ checkout \in {"base", "external-allowlisted-literal"})
+
+RiskWarning ==
+    trigger = "pull_request_target" /\ strictMode /\ ~acknowledged
+
+CheckoutRejected ==
+    trigger = "pull_request_target" /\ CheckoutNotExplicitlyDisabled /\
+      ~ObservedTrustedCheckout
+
+CheckoutError == CheckoutRejected /\ strictMode
+CheckoutWarning == CheckoutRejected /\ ~strictMode
+
+Init ==
+    /\ trigger \in Triggers
+    /\ strictMode \in BOOLEAN
+    /\ acknowledged \in BOOLEAN
+    /\ checkout \in Checkouts
+    /\ fetch \in Fetches
+
+Next == UNCHANGED vars
+Spec == Init /\ [][Next]_vars
+
+TypeOK ==
+    /\ trigger \in Triggers
+    /\ strictMode \in BOOLEAN
+    /\ acknowledged \in BOOLEAN
+    /\ checkout \in Checkouts
+    /\ fetch \in Fetches
+
+NoUntrustedCheckoutAcceptance ==
+    trigger = "pull_request_target" /\ CheckoutNotExplicitlyDisabled /\
+      ~ExpectedTrustedCheckout => ~ObservedTrustedCheckout
+
+ExactTrustedCheckoutClasses ==
+    ExpectedTrustedCheckout =>
+      checkout = "checkout-disabled" \/
+      (fetch = "none" /\
+        checkout \in {"base", "external-allowlisted-literal"})
+
+WarningAcknowledgmentIsScoped ==
+    RiskWarning =
+      (trigger = "pull_request_target" /\ strictMode /\ ~acknowledged)
+
+CheckoutDiagnosticsAreIndependentOfAcknowledgment ==
+    CheckoutError =
+      (trigger = "pull_request_target" /\ CheckoutNotExplicitlyDisabled /\
+        ~ObservedTrustedCheckout /\ strictMode)
+    /\ CheckoutWarning =
+      (trigger = "pull_request_target" /\ CheckoutNotExplicitlyDisabled /\
+        ~ObservedTrustedCheckout /\ ~strictMode)
+
+OtherTriggersHaveNoDiagnostics ==
+    trigger = "other" => ~RiskWarning /\ ~CheckoutError /\ ~CheckoutWarning
+
+=============================================================================
diff --git a/specs/workflow-security/README.md b/specs/workflow-security/README.md
@@ -40,6 +40,7 @@ sandboxed agent principal, even when GitHub Actions runs both in the same job.
 | Apps and secrets | `live`, `revoked`, `appScope`, `appRepos`, `agentSecrets` | Read-only checkout credentials, authorized engine credentials, and privileged installation tokens have different consumers and lifetimes. |
 | Networking | `ToolCall`, `egress`, `NetworkPolicy` | Authorized GitHub/inference services, blocked destinations, and service-bound engine authentication. |
 | Git | `checkouts`, `cleanup`, `agentBegan`, `privilegedCheckout`, `operations`, `errors` | Per-repository auth, temporary setup credentials, verified cleanup/failure, available blobs/refs, sparse/shallow state, local operations, REST, and privileged push. |
+| `pull_request_target` checkout policy | [`PullRequestTargetCheckout.tla`](PullRequestTargetCheckout.tla) | Strict warning acknowledgment, explicit checkout disablement, trusted base checkout, exact allowlisted external checkout, and fail-closed `fetch` handling. |
 
 The `issue` effect creates at most one validated issue in the main public
 repository. The `pull-request` effect prepares a full checkout in the privileged
@@ -65,13 +66,40 @@ represented by a skipped state-machine slot, not a real runtime job.
 
 Reviewed baseline: `542e937dd8447172c8c484cda3a9a5716ae99245`.
 The authorities are [Security Architecture v1.1.0](../security-architecture-spec.md),
-[Compiler Threat Detection v1.0.42](../compiler-threat-detection-spec.md),
+[Compiler Threat Detection v1.0.43](../compiler-threat-detection-spec.md),
 [Checkout Behavior](../../docs/src/content/docs/specs/checkout-behavior-specification.md),
 and the [Safe Outputs specification](../../docs/src/content/docs/specs/safe-outputs-specification.md).
 Line references describe that baseline; symbols are the more durable mapping.
 The checkout specification's 1.3.1 amendment requires verified cleanup before
 agent execution, including the failure paths found by the corpus trial.
 
+### `pull_request_target` checkout policy
+
+[`PullRequestTargetCheckout.tla`](PullRequestTargetCheckout.tla) is a separate,
+bounded model of compiler rule CTR-008. It exhaustively checks the finite
+combinations of trigger, strict mode, warning acknowledgment, checkout class,
+and fetch class. The successful external allowlist class represents an exact
+literal repository/ref pair; expressions, wildcard/PR refs, wiki checkouts,
+omitted external refs, and unmatched pairs have distinct untrusted classes.
+Any configured `fetch` makes a configured checkout untrusted. A `Fault`
+constant provides negative controls for acknowledgment or fetch bypassing
+checkout authorization.
+
+Run the baseline model with the same pinned TLA+ Tools installation:
+
+```bash
+java -cp /path/to/tla2tools.jar tlc2.TLC \
+  -config specs/workflow-security/PullRequestTargetCheckout.cfg \
+  specs/workflow-security/PullRequestTargetCheckout.tla
+```
+
+The baseline exhausts 400 input combinations. To verify either negative
+control, copy the `.cfg` to a temporary file, set `Fault` to
+`"acknowledgment-bypasses-checkout"` or `"fetch-bypasses-checkout"`, and
+confirm TLC reports `NoUntrustedCheckoutAcceptance`. This model specifies the
+compiler decision boundary; it does not model Git's parser or prove safety of
+the contents at an otherwise trusted mutable ref.
+
 | Predicate | Required safety condition | Architecture / threat rule | Compiler/runtime evidence |
 |---|---|---|---|
 | `TypeOK` | Every modeled job, token, checkout, channel, and request has a valid shape. | Compiler typed configuration and runtime request contracts | [`WorkflowData`](../../pkg/workflow/workflow_data.go), [`Job`](../../pkg/workflow/jobs.go), [`safe_output_validator`](../../actions/setup/js/safe_output_validator.cjs). |