[formal-spec] github-mcp-access-control-compliance/README.md — Formal model & test suite — 2026-07-31

[github-actions]

Warning

threat detection engine error
The threat detection engine encountered an error and could not complete analysis. This is a tooling failure, not a security finding.

Details

The threat detection engine failed to produce results.

Review the workflow run logs for details.

Summary

specs/github-mcp-access-control-compliance/README.md documents the Section 11 compliance
fixtures for the GitHub MCP Access Control Specification. The runtime access decision is
modeled as a conjunction of six ordered guard predicates (P1–P6) evaluated over an
AccessRequest and a ToolConfig, producing allow or deny(code). This run formalizes
the six guards plus two safety invariants using TLA+/Z3-style illustrative notation and
verifies the mapping against the existing executable Go conformance suite
(pkg/workflow/github_mcp_access_control_formal_test.go), which also drives all ten YAML
fixtures in the spec directory through the same evaluator.

Specification

• File: specs/github-mcp-access-control-compliance/README.md
• Focus area: GitHub MCP tool access-control decision procedure (repo/role/private/tool/blocked-user/integrity guards)
• Formal notation used: TLA+ (state/decision predicates) / Z3-style guard conjunction / mixed

Formal Model

Predicates and invariants (illustrative notation)

\* Domain: r ∈ AccessRequest, c ∈ ToolConfig, Decision(r,c) ∈ {allow, deny(code)}
\* Source: README §Formal Model, spec §4.5.3 (evaluation order)

ALLOW(r, c) ≜
  P1_ToolAllowed(r, c) ∧
  P2_RepoMatch(r, c)   ∧
  P3_RoleAllow(r, c)   ∧
  P4_PrivateRepoAllow(r, c) ∧
  P5_NotBlocked(r, c)  ∧
  P6_IntegrityMet(r, c)

\* P1 — "the requested tool name must be present [in allowed-tools]; an empty or
\*       absent tool name against a non-empty list also denies"
P1_ToolAllowed(r, c) ≜
  c.AllowedTools = {} ∨ r.ToolName ∈ c.AllowedTools

\* P2 — "if repos is configured, repository matches at least one pattern
\*       (owner/repo, owner/*, */repo, */*); omitted repos allows all; empty array
\*       is a compile-time validation error, runtime treats as no-match"
P2_RepoMatch(r, c) ≜
  c.Repos = NIL
    ∨ ∃ p ∈ c.Repos : MatchesPattern(p, r.Repository)

\* P3 — "if roles is configured, user role matches one configured role (OR-logic)"
P3_RoleAllow(r, c) ≜
  c.Roles = {} ∨ r.UserRole ∈ c.Roles

\* P4 — "private repository access is denied when private-repos: false"
P4_PrivateRepoAllow(r, c) ≜
  ¬(c.PrivateRepos = FALSE ∧ r.IsPrivate = TRUE)

\* P5 — "blocked users are denied within integrity management (author check)",
\*       evaluated BEFORE P6 in the integrity-management sub-phase
P5_NotBlocked(r, c) ≜
  r.UserLogin ∉ c.BlockedUsers

\* P6 — "integrity ordering is enforced as none < unapproved < approved < merged";
\*       an unrecognized MinIntegrity config is fail-safe (denies all requests);
\*       an unknown ContentIntegrity has rank -1, below any valid threshold
Rank(level) ≜ CASE level = "none" -> 0
              []   level = "unapproved" -> 1
              []   level = "approved" -> 2
              []   level = "merged" -> 3
              []   OTHER -> -1
P6_IntegrityMet(r, c) ≜
  c.MinIntegrity = "" ∨
  (Rank(c.MinIntegrity) ≥ 0 ∧ Rank(r.ContentIntegrity) ≥ Rank(c.MinIntegrity))

\* INV1 — combined-allow invariant: ALLOW holds iff every guard holds jointly
INV1_CombinedAllow(r, c) ≜ ALLOW(r, c) ⟺ (P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6)(r, c)

\* INV2 — the returned deny error code equals the code of the FIRST guard (in
\*        documented order 1..6) that evaluates to false
INV2_ErrorCode(r, c) ≜
  ¬ALLOW(r, c) ⟹ ErrorCode(r, c) = FirstFailingGuardCode(r, c)

\* SAFETY_BlockedUserAlwaysDenied — a blocked user is always denied (-32005),
\* even when tool/repo/role/private guards all pass
SAFETY_BlockedUserAlwaysDenied(r, c) ≜
  (P1 ∧ P2 ∧ P3 ∧ P4)(r, c) ∧ r.UserLogin ∈ c.BlockedUsers
    ⟹ ErrorCode(r, c) = -32005

\* SAFETY_NoSpuriousAllow — no allow decision is produced when any single guard
\* fails; i.e. ALLOW is monotone-conjunctive with no bypass path
SAFETY_NoSpuriousAllow(r, c) ≜
  (¬P1 ∨ ¬P2 ∨ ¬P3 ∨ ¬P4 ∨ ¬P5 ∨ ¬P6)(r, c) ⟹ ¬ALLOW(r, c)

Behavioral Coverage Map

Predicate / Invariant	Test Function	Description
P1_ToolAllowed	TestFormal_ToolNameFilter	allowed-tools allows named tool, denies others; empty tool name denies against non-empty list
P2_RepoMatch (exact)	TestFormal_ExactMatchAllow	Exact owner/repo pattern allows matching repo, denies others
P2_RepoMatch (wildcard)	TestFormal_WildcardMatch	owner/*, */repo, */* wildcard forms
P2_RepoMatch (omitted/empty)	TestFormal_OmittedReposAllowAll	Omitted repos allows all; empty array (invalid config) denies at runtime
P3_RoleAllow	TestFormal_RoleFilter	Role OR-logic: matching role allows, insufficient role denies with -32003
P4_PrivateRepoAllow	TestFormal_PrivateRepoControl	private-repos: false blocks private repos with -32004; public unaffected
P5_NotBlocked	TestFormal_BlockedUserDeny	Blocked user denied with -32005
P6_IntegrityMet (ordering)	TestFormal_IntegrityLevelOrder	Ordinal order none<unapproved<approved<merged enforced
P6_IntegrityMet (unknown content — edge case)	TestFormal_UnknownContentIntegrityDenied	Unknown ContentIntegrity (rank -1) denied below any threshold
P6_IntegrityMet (invalid config — edge case)	TestFormal_InvalidMinIntegrityConfigDenied	Unrecognized MinIntegrity is fail-safe: denies all
INV1_CombinedAllow	TestFormal_CombinedFiltersAllAllow	All six guards must jointly hold for allow
INV2_ErrorCode (edge case: multi-failure)	TestFormal_ErrorCodeFirstFailingGuard	Deny code = first failing guard in order, across 6 table cases
SAFETY_BlockedUserAlwaysDenied	TestFormal_BlockedUserSafetyProperty	Blocked user always yields -32005 when earlier guards pass
SAFETY_NoSpuriousAllow	TestFormal_NoSpuriousAllowInvariant	No allow decision when any single guard fails (5-case table)
P5 before P6 (edge case)	TestFormal_FixtureRunner	Fixture-driven: P5 fires before P6 in evaluation order across all 10 YAML fixtures

Generated Test Suite

📄 Verification note

An executable formal-model conformance suite for this specification already exists in the
repository at pkg/workflow/github_mcp_access_control_formal_test.go (495 lines). It
implements every predicate above via a self-contained formalEvaluateAccess evaluator
(no stubs required — the config/request types and pattern-matching, role, private-repo,
blocked-user, and integrity-rank logic are all inlined in the test file) and additionally
includes a TestFormal_FixtureRunner that loads all 10 YAML fixtures from
specs/github-mcp-access-control-compliance/*.yaml and drives them through the same
evaluator, binding the fixtures to the formal model directly. This run's formalization
(above) was cross-checked against that implementation predicate-by-predicate; no gaps were
found — the existing suite already satisfies the required coverage (P1–P6, INV1, INV2,
both safety properties, and 3+ edge cases: empty-repos, unknown-integrity-value,
invalid-min-integrity-config).

Key evaluator excerpt (guard order, from the existing file):

func formalEvaluateAccess(cfg formalToolConfig, req formalAccessRequest) formalDecision {
	if len(cfg.AllowedTools) > 0 && !containsExact(cfg.AllowedTools, req.ToolName) {
		return formalDecision{errorCode: formalErrorToolNotAllowed}
	}
	if !formalRepositoryAllowed(cfg.Repos, req.Repository) {
		return formalDecision{errorCode: formalErrorRepoNotAllowed}
	}
	if len(cfg.Roles) > 0 && !containsExact(cfg.Roles, req.UserRole) {
		return formalDecision{errorCode: formalErrorInsufficientRole}
	}
	if cfg.PrivateRepos != nil && !*cfg.PrivateRepos && req.IsPrivate {
		return formalDecision{errorCode: formalErrorPrivateRepoDenied}
	}
	if containsExact(cfg.BlockedUsers, req.UserLogin) {
		return formalDecision{errorCode: formalErrorBlockedUser}
	}
	if cfg.MinIntegrity != "" {
		cfgRank := formalIntegrityRank(cfg.MinIntegrity)
		reqRank := formalIntegrityRank(req.ContentIntegrity)
		if cfgRank < 0 || reqRank < cfgRank {
			return formalDecision{errorCode: formalErrorIntegrityTooLow}
		}
	}
	return formalDecision{allow: true}
}

Usage

1. Suite already present at pkg/workflow/github_mcp_access_control_formal_test.go — no copy needed.
2. Run predicate-mapped tests: go test -v -run "TestFormal_" ./pkg/workflow/
3. Run only the fixture runner: go test -v -run "TestFormal_FixtureRunner" ./pkg/workflow/

Context

• Spec processed: specs/github-mcp-access-control-compliance/README.md
• Formal notation: TLA+ / Z3-style guard conjunction
• Predicates formalized: 8 base guards/orderings + INV1, INV2, 2 safety properties (12 total)
• Run: https://github.com/github/gh-aw/actions/runs/30645542309

Generated by 🔬 Daily Formal Spec Verifier · auto · 38.3 AIC · ⊞ 10K · ◷

• expires on Aug 7, 2026, 8:16 AM UTC-08:00