[formal-spec] security-architecture-spec-summary.md — Formal model & test suite — 2026-08-11

[github-actions]

Summary

specs/security-architecture-spec-summary.md (v1.0.1) summarizes the GitHub Agentic Workflows Security Architecture Specification: a 7-layer defense-in-depth model with seven core security guarantees (SG-01..SG-07), a canonical job-pipeline topology, and Section 11 runtime-security requirements (RS-01..RS-15). This run extends the existing formal coverage (SG-01..SG-07, already implemented in pkg/workflow/security_architecture_sg_formal_test.go) by formalizing RS-05a — the workflow_dispatch + aw_context pull-request checkout validation gate — which prior notes flagged as having no dedicated Go test coverage.

Specification

• File: specs/security-architecture-spec-summary.md (cross-references specs/security-architecture-spec.md §11.3)
• Focus area: Runtime Security — workflow_dispatch PR checkout gating (RS-05a)
• Formal notation used: TLA+ / F* / Z3-style guard conjunction

Formal Model

Predicates and invariants (illustrative notation)

\* RS05a_CheckoutGate — Section 11.3 (RS-05a), lines 960-967
\* "For workflow_dispatch triggers where aw_context encodes a pull request
\*  context (item_type == "pull_request"), the implementation MUST enforce
\*  all of the following before executing a PR checkout."
RS05a_CheckoutGate ≜
  ∀ ctx ∈ AwContexts :
    ctx.item_type = "pull_request" ⟹
      PerformCheckout(ctx) ⟹
        RepoScopeOK(ctx) ∧ ActorTrustOK(ctx) ∧ ParseOK(ctx) ∧ ItemNumberPresent(ctx)

\* RS05a_1_RepoScope — line 962
\* "If aw_context.repo is present, compare against context.repo.owner/repo.
\*  A mismatch MUST cause checkout to be skipped with a warning;
\*  cross-repository PR checkout is NOT supported."
RS05a_1_RepoScope ≜
  ∀ ctx ∈ AwContexts :
    (ctx.repo ≠ nil ∧ ctx.repo ≠ CurrentRepoIdentity) ⟹
      ¬PerformCheckout(ctx) ∧ EmittedWarning(ctx)

\* RS05a_2_ActorTrust — line 963
\* "The triggering actor MUST satisfy assertTrustedCheckoutRuntime() —
\*  the runtime repository MUST NOT be a fork, and the actor MUST hold
\*  write-or-higher repository permission (or be a verified bot/app actor)."
RS05a_2_ActorTrust ≜
  ∀ ctx ∈ AwContexts :
    PerformCheckout(ctx) ⟹
      ¬IsFork(RuntimeRepo) ∧ (HasWriteOrHigher(ctx.actor) ∨ IsVerifiedBotOrApp(ctx.actor))

\* RS05a_3_ParseResilience — line 964
\* "Malformed aw_context JSON MUST be caught; the implementation MUST
\*  emit a warning and skip checkout rather than propagating the parse error."
RS05a_3_ParseResilience ≜
  ∀ raw ∈ RawInputs :
    ¬IsValidJSON(raw) ⟹
      ¬ThrowsUncaught(ParseAwContext(raw)) ∧ EmittedWarning(raw) ∧ ¬PerformCheckout(raw)

\* RS05a_4_RefIsolation — line 965
\* "The PR head MUST be fetched exclusively via refs/pull/N/head from the
\*  current repository's origin, using array-based execution (no shell
\*  interpolation)."
RS05a_4_RefIsolation ≜
  ∀ ctx ∈ AwContexts :
    PerformCheckout(ctx) ⟹
      FetchRef(ctx) = "refs/pull/" \o ctx.item_number \o "/head" ∧
      FetchOrigin(ctx) = CurrentRepoOrigin ∧
      ExecutionMode(ctx) = ArrayBased ∧ ¬UsesShellInterpolation(ctx)

\* RS05a_5_ItemNumberRequired — line 967
\* "The implementation MUST NOT perform checkout when aw_context.item_number
\*  is absent or falsy."
RS05a_5_ItemNumberRequired ≜
  ∀ ctx ∈ AwContexts :
    (ctx.item_number = nil ∨ IsFalsy(ctx.item_number)) ⟹ ¬PerformCheckout(ctx)

val assertTrustedCheckoutRuntime :
  ctx:AwContext →
  Tot bool
  (requires True)
  (ensures fun ok →
    ok = true ⟹ (not (IsFork RuntimeRepo)) /\
                (HasWriteOrHigher ctx.actor \/ IsVerifiedBotOrApp ctx.actor))

val parseAwContextSafely :
  raw:string →
  Tot (result AwContext CheckoutError)
  (requires True)
  (ensures fun r →
    (not (IsValidJSON raw) ⟹ Error? r /\ PerformCheckout? r == false) ∧
    (IsValidJSON raw ⟹ Ok? r))

; RS05a_RepoIdentityBound — repo-scope comparison is a pure equality guard,
; never a partial/prefix match (prevents subdomain/owner-prefix spoofing)
(declare-const ctx_repo String)
(declare-const current_repo String)
(declare-const checkout_allowed Bool)
(assert (=> (and (not (= ctx_repo "")) (not (= ctx_repo current_repo)))
            (not checkout_allowed)))
(check-sat) ; sat — mismatch always forces checkout_allowed = false

Behavioral Coverage Map

Predicate / Invariant	Test Function	Description
RS05a_CheckoutGate	TestFormalRS05a_CheckoutGateConjunctionAllPass	All four RS-05a sub-conditions must hold simultaneously to permit checkout
RS05a_1_RepoScope	TestFormalRS05a_RepoScopeMismatchBlocksCheckout	Cross-repo aw_context.repo mismatch skips checkout and emits a warning
RS05a_1_RepoScope	TestFormalRS05a_RepoScopeAbsentAllowsCheckoutContinuation	Absent aw_context.repo field does not itself block checkout (falls through to other gates)
RS05a_2_ActorTrust	TestFormalRS05a_ActorTrustForkRejected	Runtime repository being a fork always blocks checkout regardless of actor permission
RS05a_2_ActorTrust	TestFormalRS05a_ActorTrustInsufficientPermissionRejected	Non-write, non-bot/app actor is rejected even on a non-fork repository
RS05a_2_ActorTrust	TestFormalRS05a_ActorTrustVerifiedBotAllowed	A verified bot/app actor satisfies the trust gate without explicit write permission
RS05a_3_ParseResilience	TestFormalRS05a_MalformedJSONSkipsCheckoutWithoutPanic	Malformed aw_context JSON is caught, produces a warning, and never propagates a raw parse error
RS05a_4_RefIsolation	TestFormalRS05a_RefIsolationUsesPullHeadRef	Fetched ref is exactly refs/pull/<N>/head against the current repo's origin
RS05a_4_RefIsolation	TestFormalRS05a_RefIsolationRejectsShellInterpolation	Execution mode must be array-based; shell-interpolated fetch commands are rejected
RS05a_5_ItemNumberRequired	TestFormalRS05a_MissingItemNumberBlocksCheckout	Absent or falsy item_number unconditionally blocks checkout
RS05a_5_ItemNumberRequired	TestFormalRS05a_ZeroItemNumberTreatedAsFalsy	item_number == "0" / empty string is treated as falsy (edge case)
RS05a_CheckoutGate	TestFormalRS05a_NonPullRequestItemTypeBypassesGate	Non-pull_request item_type values are outside RS-05a's scope entirely (edge case)

Generated Test Suite

📄 `pkg/workflow/security_architecture_rs05a_formal_test.go`

// Package workflow_test contains formal-model-derived unit tests for
// specs/security-architecture-spec-summary.md (§ RS-05a, cross-referencing
// specs/security-architecture-spec.md §11.3, lines 960-967).
//
// Formal predicates encoded by this file (see issue body for full TLA+/F*/Z3
// notation):
//
//	RS05a_CheckoutGate          - all four sub-gates must hold before checkout
//	RS05a_1_RepoScope           - aw_context.repo must match current repo identity
//	RS05a_2_ActorTrust          - assertTrustedCheckoutRuntime(): no-fork + write-or-bot
//	RS05a_3_ParseResilience     - malformed aw_context JSON must not panic/propagate
//	RS05a_4_RefIsolation        - refs/pull/N/head fetch, array-based execution only
//	RS05a_5_ItemNumberRequired  - absent/falsy item_number always blocks checkout
//
// No production Go implementation of the RS-05a checkout gate currently
// exists in pkg/workflow/ (the runtime logic lives in shell/JS setup
// scripts). The stub interface below encodes the normative contract so the
// predicates are testable; replace with real implementation bindings once
// a Go-side gate exists.
package workflow_test

import (
	"encoding/json"
	"testing"

	"github.com/stretchr/testify/assert"
	"github.com/stretchr/testify/require"
)

// stub — replace with real implementation
//
// awContext mirrors the fields of the workflow_dispatch aw_context input
// relevant to RS-05a (see actions/setup/js/aw_context.cjs for the real
// runtime shape).
type awContext struct {
	ItemType   string `json:"item_type"`
	ItemNumber string `json:"item_number"`
	Repo       string `json:"repo,omitempty"`
	Actor      string `json:"actor,omitempty"`
}

// stub — replace with real implementation
type checkoutDecision struct {
	Allowed      bool
	WarningEmitted bool
	FetchRef     string
	FetchOrigin  string
	ArrayBased   bool
}

// stub — replace with real implementation
//
// assertTrustedCheckoutRuntime encodes RS05a_2_ActorTrust: the runtime
// repository MUST NOT be a fork, and the actor MUST hold write-or-higher
// permission or be a verified bot/app actor.
func assertTrustedCheckoutRuntime(isFork bool, actorHasWriteOrHigher bool, isVerifiedBotOrApp bool) bool {
	if isFork {
		return false
	}
	return actorHasWriteOrHigher || isVerifiedBotOrApp
}

// stub — replace with real implementation
//
// parseAwContextSafely encodes RS05a_3_ParseResilience: malformed JSON must
// never panic and must be surfaced as a caught, non-fatal error.
func parseAwContextSafely(raw string) (ctx awContext, warning bool, err error) {
	if jsonErr := json.Unmarshal([]byte(raw), &ctx); jsonErr != nil {
		return awContext{}, true, jsonErr
	}
	return ctx, false, nil
}

// stub — replace with real implementation
//
// evaluateRS05aCheckoutGate encodes RS05a_CheckoutGate: the conjunction of
// all sub-gates that must hold before a workflow_dispatch PR checkout may
// proceed.
func evaluateRS05aCheckoutGate(ctx awContext, currentRepo string, isFork bool, actorHasWriteOrHigher bool, isVerifiedBotOrApp bool) checkoutDecision {
	if ctx.ItemType != "pull_request" {
		// Out of RS-05a's scope entirely; no gating applies here.
		return checkoutDecision{Allowed: true}
	}

	// RS05a_5_ItemNumberRequired
	if ctx.ItemNumber == "" || ctx.ItemNumber == "0" {
		return checkoutDecision{Allowed: false}
	}

	// RS05a_1_RepoScope
	if ctx.Repo != "" && ctx.Repo != currentRepo {
		return checkoutDecision{Allowed: false, WarningEmitted: true}
	}

	// RS05a_2_ActorTrust
	if !assertTrustedCheckoutRuntime(isFork, actorHasWriteOrHigher, isVerifiedBotOrApp) {
		return checkoutDecision{Allowed: false}
	}

	// RS05a_4_RefIsolation
	return checkoutDecision{
		Allowed:     true,
		FetchRef:    "refs/pull/" + ctx.ItemNumber + "/head",
		FetchOrigin: currentRepo,
		ArrayBased:  true,
	}
}

func TestFormalRS05a_CheckoutGateConjunctionAllPass(t *testing.T) {
	ctx := awContext{ItemType: "pull_request", ItemNumber: "42", Repo: "github/gh-aw"}
	decision := evaluateRS05aCheckoutGate(ctx, "github/gh-aw", false, true, false)
	require.True(t, decision.Allowed, "RS05a_CheckoutGate: checkout MUST be allowed when all four sub-gates (repo scope, actor trust, parse resilience, item number) hold")
	assert.Equal(t, "refs/pull/42/head", decision.FetchRef, "RS05a_4_RefIsolation: fetch ref MUST be refs/pull/<N>/head when checkout is allowed")
}

func TestFormalRS05a_RepoScopeMismatchBlocksCheckout(t *testing.T) {
	ctx := awContext{ItemType: "pull_request", ItemNumber: "7", Repo: "other-org/other-repo"}
	decision := evaluateRS05aCheckoutGate(ctx, "github/gh-aw", false, true, false)
	assert.False(t, decision.Allowed, "RS05a_1_RepoScope: a mismatched aw_context.repo MUST cause checkout to be skipped; cross-repository PR checkout is NOT supported")
	assert.True(t, decision.WarningEmitted, "RS05a_1_RepoScope: a repo mismatch MUST emit a warning")
}

func TestFormalRS05a_RepoScopeAbsentAllowsCheckoutContinuation(t *testing.T) {
	ctx := awContext{ItemType: "pull_request", ItemNumber: "7"}
	decision := evaluateRS05aCheckoutGate(ctx, "github/gh-aw", false, true, false)
	assert.True(t, decision.Allowed, "RS05a_1_RepoScope: an absent aw_context.repo field MUST NOT itself block checkout; only an explicit mismatch does")
}

func TestFormalRS05a_ActorTrustForkRejected(t *testing.T) {
	ctx := awContext{ItemType: "pull_request", ItemNumber: "7", Repo: "github/gh-aw"}
	decision := evaluateRS05aCheckoutGate(ctx, "github/gh-aw", true /* isFork */, true, false)
	assert.False(t, decision.Allowed, "RS05a_2_ActorTrust: a forked runtime repository MUST block checkout even with a write-permission actor")
}

func TestFormalRS05a_ActorTrustInsufficientPermissionRejected(t *testing.T) {
	ctx := awContext{ItemType: "pull_request", ItemNumber: "7", Repo: "github/gh-aw"}
	decision := evaluateRS05aCheckoutGate(ctx, "github/gh-aw", false, false /* no write */, false /* not bot */)
	assert.False(t, decision.Allowed, "RS05a_2_ActorTrust: an actor without write-or-higher permission and not a verified bot/app MUST be rejected")
}

func TestFormalRS05a_ActorTrustVerifiedBotAllowed(t *testing.T) {
	ctx := awContext{ItemType: "pull_request", ItemNumber: "7", Repo: "github/gh-aw"}
	decision := evaluateRS05aCheckoutGate(ctx, "github/gh-aw", false, false, true /* verified bot */)
	assert.True(t, decision.Allowed, "RS05a_2_ActorTrust: a verified bot/app actor MUST satisfy the trust gate even without explicit write permission")
}

func TestFormalRS05a_MalformedJSONSkipsCheckoutWithoutPanic(t *testing.T) {
	malformed := `{"item_type": "pull_request", "item_number": ` // truncated JSON
	require.NotPanics(t, func() {
		_, warning, err := parseAwContextSafely(malformed)
		assert.Error(t, err, "RS05a_3_ParseResilience: malformed aw_context JSON MUST be caught as a non-fatal error")
		assert.True(t, warning, "RS05a_3_ParseResilience: a parse failure MUST emit a warning rather than propagating the raw error")
	}, "RS05a_3_ParseResilience: parsing malformed aw_context JSON MUST NOT panic")
}

func TestFormalRS05a_RefIsolationUsesPullHeadRef(t *testing.T) {
	ctx := awContext{ItemType: "pull_request", ItemNumber: "1234", Repo: "github/gh-aw"}
	decision := evaluateRS05aCheckoutGate(ctx, "github/gh-aw", false, true, false)
	require.True(t, decision.Allowed, "precondition: checkout must be allowed to inspect the fetch ref")
	assert.Equal(t, "refs/pull/1234/head", decision.FetchRef, "RS05a_4_RefIsolation: the PR head MUST be fetched exclusively via refs/pull/N/head")
	assert.Equal(t, "github/gh-aw", decision.FetchOrigin, "RS05a_4_RefIsolation: the fetch origin MUST be the current repository")
}

func TestFormalRS05a_RefIsolationRejectsShellInterpolation(t *testing.T) {
	ctx := awContext{ItemType: "pull_request", ItemNumber: "55", Repo: "github/gh-aw"}
	decision := evaluateRS05aCheckoutGate(ctx, "github/gh-aw", false, true, false)
	require.True(t, decision.Allowed, "precondition: checkout must be allowed to inspect execution mode")
	assert.True(t, decision.ArrayBased, "RS05a_4_RefIsolation: fetch execution MUST be array-based with no shell interpolation")
}

func TestFormalRS05a_MissingItemNumberBlocksCheckout(t *testing.T) {
	ctx := awContext{ItemType: "pull_request", ItemNumber: "", Repo: "github/gh-aw"}
	decision := evaluateRS05aCheckoutGate(ctx, "github/gh-aw", false, true, false)
	assert.False(t, decision.Allowed, "RS05a_5_ItemNumberRequired: checkout MUST NOT be performed when aw_context.item_number is absent")
}

func TestFormalRS05a_ZeroItemNumberTreatedAsFalsy(t *testing.T) {
	ctx := awContext{ItemType: "pull_request", ItemNumber: "0", Repo: "github/gh-aw"}
	decision := evaluateRS05aCheckoutGate(ctx, "github/gh-aw", false, true, false)
	assert.False(t, decision.Allowed, "RS05a_5_ItemNumberRequired: an item_number of \"0\" MUST be treated as falsy and block checkout")
}

func TestFormalRS05a_NonPullRequestItemTypeBypassesGate(t *testing.T) {
	ctx := awContext{ItemType: "issue", ItemNumber: "9", Repo: "other-org/other-repo"}
	decision := evaluateRS05aCheckoutGate(ctx, "github/gh-aw", true, false, false)
	assert.True(t, decision.Allowed, "RS05a_CheckoutGate: non-pull_request item_type values are outside RS-05a's scope and MUST NOT be gated by this rule")
}

Usage

1. Copy the test file to pkg/workflow/security_architecture_rs05a_formal_test.go.
2. Replace the // stub awContext, checkoutDecision, assertTrustedCheckoutRuntime, parseAwContextSafely, and evaluateRS05aCheckoutGate definitions with bindings to the real Go-side implementation once RS-05a gating is ported from the shell/JS setup scripts, or wire the stub logic directly against actions/setup/js/aw_context.cjs behavior via a JS-test bridge if the gate remains JS-only.
3. Run: go test ./pkg/workflow/... -run 'TestFormalRS05a'

Context

• Spec processed: specs/security-architecture-spec-summary.md
• Formal notation: TLA+ / F* / Z3-style guard conjunction
• Run: https://github.com/github/gh-aw/actions/runs/31508370270

Generated by 🔬 Daily Formal Spec Verifier · auto · 51.7 AIC · ⌖ 3.62 AIC · ⊞ 9.9K · ◷

• expires on Aug 18, 2026, 7:49 AM UTC-08:00