Add formal GitHub MCP access-control conformance model and predicate-mapped test suite#44790
Conversation
Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>
There was a problem hiding this comment.
Pull request overview
Formalizes GitHub MCP access-control predicates and adds a test-only decision model.
Changes:
- Documents guard predicates, invariants, and test mappings.
- Adds formal access-decision tests and evaluator helpers.
- Documents the new test suite.
Show a summary per file
| File | Description |
|---|---|
specs/github-mcp-access-control-compliance/README.md |
Adds the formal model and coverage map. |
pkg/workflow/github_mcp_access_control_formal_test.go |
Adds predicate tests and a test-only evaluator. |
Review details
Tip
Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
- Files reviewed: 2/2 changed files
- Comments generated: 12
- Review effort level: Medium
| errorCode int | ||
| } | ||
|
|
||
| func formalEvaluateAccess(cfg formalToolConfig, req formalAccessRequest) formalDecision { |
There was a problem hiding this comment.
The formal test suite is intentionally scoped to the decision model documented in specs/github-mcp-access-control-compliance/README.md: it tests the guard predicates (P1–P6), first-failing-guard error-code semantics, and safety invariants that the spec defines. It is not an integration test of the production gateway — that would require loading compliance fixtures and the actual compiler/gateway, which is a separate concern beyond the scope of this predicate-mapping PR. The PR title and README section "Formal Model" make this boundary explicit. Integration coverage of the real implementation remains a future work item in the spec's §11.
| formalErrorRepoNotAllowed = -32001 | ||
| formalErrorInsufficientRole = -32002 | ||
| formalErrorPrivateRepoDenied = -32003 | ||
| formalErrorBlockedUser = -32004 | ||
| formalErrorToolNotAllowed = -32005 |
| func TestFormal_EmptyReposDenyAll(t *testing.T) { | ||
| assert.False(t, formalEvaluateAccess(formalToolConfig{}, formalAccessRequest{Repository: "github/gh-aw"}).allow) | ||
| assert.False(t, formalEvaluateAccess(formalToolConfig{Repos: []string{}}, formalAccessRequest{Repository: "github/gh-aw"}).allow) |
|
|
||
| func TestFormal_WildcardMatch(t *testing.T) { | ||
| assert.True(t, formalEvaluateAccess(formalToolConfig{Repos: []string{"github/*"}}, formalAccessRequest{Repository: "github/gh-aw"}).allow) | ||
| assert.True(t, formalEvaluateAccess(formalToolConfig{Repos: []string{"github/gh-*"}}, formalAccessRequest{Repository: "github/gh-aw"}).allow) |
| if containsExact(cfg.BlockedUsers, req.UserLogin) { | ||
| return formalDecision{errorCode: formalErrorBlockedUser} | ||
| } |
| | `P8_IntegrityMet` | `TestFormal_IntegrityLevelOrder` | Integrity ordinal order enforced; content below threshold denied | | ||
| | `INV1_CombinedAllow` | `TestFormal_CombinedFiltersAllAllow` | All conditions must be satisfied for allow | | ||
| | `INV2_ErrorCode` | `TestFormal_ErrorCodeFirstFailingGuard` | Deny error code matches first failing guard in evaluation order | | ||
| | `SAFETY_BlockedUserAlwaysDenied` | `TestFormal_BlockedUserSafetyProperty` | Safety: blocked user always produces `-32004` | |
| |---|---|---| | ||
| | `P1_ExactMatch` | `TestFormal_ExactMatchAllow` | Exact `owner/repo` pattern allows matching repo, denies others | | ||
| | `P2_WildcardMatch` | `TestFormal_WildcardMatch` | Owner-wildcard `owner/*` and prefix-wildcard `owner/prefix-*` matching | | ||
| | `P3_EmptyReposDenyAll` | `TestFormal_EmptyReposDenyAll` | Absent or empty repos list denies every repository | |
| Formal conformance tests are implemented in: | ||
|
|
||
| `pkg/workflow/github_mcp_access_control_formal_test.go` |
There was a problem hiding this comment.
Fixed in commit fix: align formal MCP access-control tests with canonical error codes and spec guard order. The README now includes a dedicated TestFormal_* run command at line 137–141.
|
|
||
| Where: | ||
|
|
||
| - `P1_RepoMatch`: repository matches at least one configured `repos` pattern (`owner/repo`, `owner/*`, `owner/prefix-*`) |
| denied := formalEvaluateAccess(cfg, formalAccessRequest{ | ||
| Repository: "github/other", UserRole: "read", IsPrivate: true, ToolName: "delete_repo", UserLogin: "good-user", ContentIntegrity: "none", | ||
| }) | ||
|
|
||
| assert.False(t, denied.allow) | ||
| assert.Equal(t, formalErrorRepoNotAllowed, denied.errorCode) |
|
🧠 Matt Pocock Skills Reviewer has completed the skills-based review. ✅ |
|
✅ Test Quality Sentinel completed test quality analysis. |
|
✅ Design Decision Gate 🏗️ completed the design decision gate check. |
|
✅ PR Code Quality Reviewer completed the code quality review. |
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
Review: Guard Order / Predicate Numbering Mismatch
The PR adds a well-structured formal model and predicate-mapped test suite. Two blocking issues need to be resolved:
1. Guard evaluation order contradicts the formal spec
The formalEvaluateAccess evaluator checks BlockedUsers before RepoMatch, but the README formal model places P5_NotBlocked after P1_RepoMatch. Because the first-failing-guard rule determines the denial error code, multi-condition requests (blocked user + wrong repo) will produce -32004 from the code but the spec implies -32001. Either align the evaluator to match the spec order or update the spec to declare that blocked-user is evaluated first.
2. Predicate numbering inconsistency between formal model and coverage table
The formal model defines P1–P6, but the coverage table assigns P1–P8 with shifted numbering (e.g., P6_NotBlocked, P7_ToolAllowed). This breaks predicate→test traceability. Unify numbering across both sections.
Non-blocking observations
formalIntegrityRankreturns-1for unknown/empty integrity strings, which effectively ranks them belownone(rank 0). An emptyContentIntegrityon a request whereMinIntegrityis set will be denied, but the behavior for emptyMinIntegrityis implicit. Worth a comment.- Pattern matching delegates to
path.Matchwhich accepts glob metacharacters like[a-z]. This is likely intentional but a comment would clarify scope.
Warning
Firewall blocked 1 domain
The following domain was blocked by the firewall during workflow execution:
proxy.golang.org
To allow these domains, add them to the
network.allowedlist in your workflow frontmatter:
network:
allowed:
- defaults
- "proxy.golang.org"See Network Configuration for more information.
🧵 Reviewed using Impeccable skills by Impeccable Skills Reviewer · 27.5 AIC · ⌖ 4.65 AIC · ⊞ 4.8K
| if containsExact(cfg.BlockedUsers, req.UserLogin) { | ||
| return formalDecision{errorCode: formalErrorBlockedUser} | ||
| } | ||
| if !formalRepositoryAllowed(cfg.Repos, req.Repository) { |
There was a problem hiding this comment.
Guard evaluation order contradicts the formal model
The README formal model defines the conjunction as:
P1_RepoMatch ∧ P2_RoleAllow ∧ P3_PrivateRepoAllow ∧ P4_ToolAllowed ∧ P5_NotBlocked ∧ P6_IntegrityMet
But this evaluator checks BlockedUsers first, before the repo check:
if containsExact(cfg.BlockedUsers, req.UserLogin) {
return formalDecision{errorCode: formalErrorBlockedUser}
}
if !formalRepositoryAllowed(cfg.Repos, req.Repository) { ...This means if a blocked user requests an unallowed repo, the code returns formalErrorBlockedUser (-32004), but the spec's first-failing-guard rule says P1_RepoMatch fails first, so it should return formalErrorRepoNotAllowed (-32001). Either:
- Move the blocked-user check to its correct position (after P4_ToolAllowed), or
- Update the formal model in the README to match the intended
BlockedUsers-firstsemantics (which is a reasonable safety-first design choice).
@copilot please address this.
There was a problem hiding this comment.
Fixed in commit fix: align formal MCP access-control tests with canonical error codes and spec guard order. The evaluator now checks guards in the documented order: tool → repo → role → private-repo → blocked-user → integrity. The README formal model (P1_ToolAllowed through P6_IntegrityMet) and the evaluator order are now consistent.
| P3_PrivateRepoAllow(r, c) ∧ | ||
| P4_ToolAllowed(r, c) ∧ | ||
| P5_NotBlocked(r, c) ∧ | ||
| P6_IntegrityMet(r, c) |
There was a problem hiding this comment.
Predicate numbering inconsistency between formal model and coverage table
The formal model above defines six predicates P1–P6:
- P1_RepoMatch, P2_RoleAllow, P3_PrivateRepoAllow, P4_ToolAllowed, P5_NotBlocked, P6_IntegrityMet
But the behavioral coverage table below uses eight predicates P1–P8 with different names:
- P4_RoleAllow, P5_PrivateRepoAllow, P6_NotBlocked, P7_ToolAllowed, P8_IntegrityMet
This numbering mismatch makes it impossible to trace a predicate from the formal model to its test. The coverage table should use the same P1–P6 identifiers from the formal model, or the formal model should be updated to use P1–P8.
@copilot please address this.
There was a problem hiding this comment.
Fixed in commit fix: align formal MCP access-control tests with canonical error codes and spec guard order. The README formal model and the behavioral coverage map now use consistent P1–P6 numbering: P1=ToolAllowed, P2=RepoMatch, P3=RoleAllow, P4=PrivateRepoAllow, P5=NotBlocked, P6=IntegrityMet.
…njunction formalization
Design Decision Gate — ADR RequiredThis PR makes significant changes to core business logic (259 new lines across Draft ADR committed:
What to do next
Once an ADR is linked in the PR body, this gate will re-run and verify the implementation matches the decision. Why ADRs MatterADRs create a searchable, permanent record of why the codebase looks the way it does. Future contributors (and your future self) will thank you. Michael Nygard ADR Format ReferenceAn ADR must contain these four sections to be considered complete:
All ADRs are stored in
|
🧪 Test Quality Sentinel Report✅ Test Quality Score: 94/100 — Excellent
📊 Metrics (12 tests)
|
There was a problem hiding this comment.
Skills-Based Review 🧠
Applied /tdd and /grill-with-docs — requesting changes on correctness gaps in the formal model.
📋 Key Themes & Highlights
Key Themes
-
Guard order inconsistency (correctness):
formalEvaluateAccesschecksBlockedUsersfirst, but the README formal model lists it as the 5th guard (P5_NotBlocked). The first-failing-guard semantics are the central claim of this PR — the implementation and spec must agree. -
Empty
ToolNamebypass (security): WhenToolName == "", theAllowedToolsguard is silently skipped (line 206). This is untested and undocumented; callers who omit the field bypass the tool allowlist. -
Unknown integrity values (correctness):
formalIntegrityRankreturns-1for unrecognised levels, which causesformalErrorIntegrityTooLowto fire — but this behaviour is not tested or documented. -
Wildcard-owner pattern gap (completeness): Patterns like
*/gh-aware silently rejected byformalRepositoryAllowedwith no test declaring that as intentional. -
Predicate numbering drift (spec): The formal model block uses
P1–P6, the coverage map usesP1–P8. The predicates don't share the same numbering, making traceability fragile.
Positive Highlights
- ✅ Excellent use of a minimal deterministic harness that is entirely test-scoped — no production code changes needed.
- ✅ Safety properties (
SAFETY_BlockedUserAlwaysDenied,SAFETY_NoSpuriousAllow) are a strong pattern for access-control specs. - ✅ The behavioral coverage map is clear and a great addition to the spec README.
- ✅ Guard predicate naming (
P1_RepoMatch,P2_RoleAllow, ...) maps cleanly to the formal model.
🧠 Reviewed using Matt Pocock's skills by Matt Pocock Skills Reviewer · 45.3 AIC · ⌖ 5.09 AIC · ⊞ 6.6K
Comment /matt to run again
| if !formalRepositoryAllowed(cfg.Repos, req.Repository) { | ||
| return formalDecision{errorCode: formalErrorRepoNotAllowed} | ||
| } | ||
| if len(cfg.Roles) > 0 && !containsExact(cfg.Roles, req.UserRole) { |
There was a problem hiding this comment.
[/tdd] Guard evaluation order in formalEvaluateAccess contradicts the README formal model: BlockedUsers is checked first (line 196), but the spec lists P5_NotBlocked as the fifth guard. A request that fails both repo and blocked-user checks returns -32004 (blocked user) rather than -32001 (repo not allowed), breaking the documented first-failing-guard semantics.
💡 Fix suggestion
Either reorder formalEvaluateAccess so the blocked-user check is at position 5 (matching P1..P6 in the spec), or update the README to declare blocked-user checking as P1.
Add a regression test that explicitly documents the intended order:
func TestFormal_BlockedUserVsRepoGuardOrder(t *testing.T) {
cfg := formalToolConfig{Repos: []string{"github/gh-aw"}, BlockedUsers: []string{"bad"}}
denied := formalEvaluateAccess(cfg, formalAccessRequest{Repository: "github/other", UserLogin: "bad"})
// Spec says first-failing guard wins — declare which that is
assert.Equal(t, formalErrorBlockedUser, denied.errorCode)
}@copilot please address this.
There was a problem hiding this comment.
Fixed in commit fix: align formal MCP access-control tests with canonical error codes and spec guard order. Guard evaluation order is now: tool → repo → role → private-repo → blocked-user → integrity, matching both the README formal model (P1–P6) and the spec §4.5.3 order.
| func TestFormal_CombinedFiltersAllAllow(t *testing.T) { | ||
| allowPrivate := true | ||
| cfg := formalToolConfig{ | ||
| Repos: []string{"github/gh-aw"}, |
There was a problem hiding this comment.
[/tdd] TestFormal_ToolNameFilter has an implicit assumption that an empty ToolName is always allowed — but this is untested and undocumented. Line 206 (req.ToolName != "") silently permits any tool when ToolName is the zero value, which could be a security gap if callers accidentally omit the field.
💡 Suggested test
func TestFormal_EmptyToolNameBehavior(t *testing.T) {
cfg := formalToolConfig{Repos: []string{"*/*"}, AllowedTools: []string{"issue_read"}}
// Document explicit intent: empty tool name is allow or deny?
result := formalEvaluateAccess(cfg, formalAccessRequest{Repository: "github/gh-aw", ToolName: ""})
assert.False(t, result.allow, "empty ToolName should not bypass AllowedTools check")
}If the intent is to allow empty tool names (e.g., for non-tool requests), document that in a comment on line 206.
@copilot please address this.
There was a problem hiding this comment.
Fixed in commit fix: align formal MCP access-control tests with canonical error codes and spec guard order. The req.ToolName != "" short-circuit was removed. The tool check is now len(cfg.AllowedTools) > 0 && !containsExact(cfg.AllowedTools, req.ToolName), so an empty tool name against a non-empty allowlist correctly denies. TestFormal_ToolNameFilter covers this case explicitly.
|
|
||
| func formalRepositoryAllowed(patterns []string, repository string) bool { | ||
| if len(patterns) == 0 || repository == "" { | ||
| return false |
There was a problem hiding this comment.
[/tdd] formalIntegrityRank returns -1 for unknown integrity levels (line 246), but no test covers this case. A request with an unrecognised ContentIntegrity value (e.g., "pending") against a config with MinIntegrity: "approved" would return formalErrorIntegrityTooLow silently — but whether that is the intended invariant is undocumented.
💡 Suggested test
func TestFormal_UnknownIntegrityLevelDenied(t *testing.T) {
denied := formalEvaluateAccess(
formalToolConfig{Repos: []string{"*/*"}, MinIntegrity: "approved"},
formalAccessRequest{Repository: "github/gh-aw", ContentIntegrity: "pending"},
)
assert.False(t, denied.allow)
assert.Equal(t, formalErrorIntegrityTooLow, denied.errorCode)
}@copilot please address this.
There was a problem hiding this comment.
Added TestFormal_UnknownIntegrityLevelDenied in commit fix: make unknown MinIntegrity fail-safe and add unknown integrity level tests. The test covers: (1) an unknown ContentIntegrity value ("pending") against a known threshold denies with formalErrorIntegrityTooLow, and (2) an unrecognized MinIntegrity configuration ("invalid") is treated as fail-safe and denies all requests. The formalIntegrityRank rank-based comparison is now documented via the evaluator's split conditions.
| return true | ||
| case patternOwner == repoOwner && patternRepo == repoName: | ||
| return true | ||
| case patternOwner == repoOwner && strings.Contains(patternRepo, "*"): |
There was a problem hiding this comment.
[/tdd] formalRepositoryAllowed only handles glob patterns where the wildcard is in the repo name segment (e.g. owner/prefix-*). A pattern like */gh-aw (wildcard owner) is not tested and the switch statement has no case for it — the function would fall through and return false for */gh-aw matching github/gh-aw.
💡 Suggested test to document the gap
func TestFormal_WildcardOwnerNotSupported(t *testing.T) {
// If "*/gh-aw" is intended to NOT be supported, document it
result := formalEvaluateAccess(
formalToolConfig{Repos: []string{"*/gh-aw"}},
formalAccessRequest{Repository: "github/gh-aw"},
)
assert.False(t, result.allow, "wildcard-owner patterns are not supported by design")
}If owner wildcards should be supported, add a case to the switch in formalRepositoryAllowed.
@copilot please address this.
| P4_ToolAllowed(r, c) ∧ | ||
| P5_NotBlocked(r, c) ∧ | ||
| P6_IntegrityMet(r, c) | ||
| ``` |
There was a problem hiding this comment.
[/grill-with-docs] The formal model lists guard predicates as P1–P6 in one order, but the behavioral coverage map below uses different numbering (P1–P8 plus named predicates). For example, the model has P5_NotBlocked but the coverage table labels it P6_NotBlocked. The mismatch makes it hard to trace from the formal spec to the test table without manual reconciliation.
💡 Fix suggestion
Align the predicate numbering between the formal definition block and the coverage map, or use names only (drop the Pn ordinals in one place) to avoid the numbering drift.
@copilot please address this.
There was a problem hiding this comment.
Fixed in commit fix: align formal MCP access-control tests with canonical error codes and spec guard order. The README now defines P1–P6 in evaluation order (P1=ToolAllowed first) and the behavioral coverage table uses the same numbering. No more offset between the formal model and the test coverage map.
There was a problem hiding this comment.
REQUEST_CHANGES — 3 correctness/security bugs must be fixed before merge
The formal model and its test harness introduce real fail-open logic errors that undermine the stated security guarantees of the access-control spec.
Blocking findings
1. Tool allowlist bypassed on empty ToolName (line 208) — AllowedTools is silently skipped when req.ToolName == "". Any caller that omits the tool name bypasses an explicitly configured allowlist.
2. Blocked-user guard order diverges from spec (line 196) — The implementation evaluates BlockedUsers before RepoMatch, but the README formal model places P5_NotBlocked after P1–P4. The error-code ordering test (TestFormal_ErrorCodeFirstFailingGuard) does not cover this case, so the contradiction is undetected.
3. Unrecognized MinIntegrity silently disables the integrity gate (line 248) — formalIntegrityRank returns -1 for any unknown string. A misconfigured/typo'd MinIntegrity makes the guard rank < -1 permanently false, granting every request regardless of integrity.
🔎 Code quality review by PR Code Quality Reviewer · 34.6 AIC · ⌖ 4.77 AIC · ⊞ 5.4K
Comment /review to run again
| if cfg.MinIntegrity != "" && formalIntegrityRank(req.ContentIntegrity) < formalIntegrityRank(cfg.MinIntegrity) { | ||
| return formalDecision{errorCode: formalErrorIntegrityTooLow} | ||
| } | ||
| return formalDecision{allow: true} |
There was a problem hiding this comment.
Tool allowlist silently bypassed when ToolName is empty: a request with an empty tool name skips the AllowedTools restriction entirely and is allowed.
💡 Detail and suggested fix
The current guard is:
if len(cfg.AllowedTools) > 0 && req.ToolName != "" && !containsExact(cfg.AllowedTools, req.ToolName) {When req.ToolName == "" the whole condition short-circuits and the allowlist is never consulted. Any caller that forgets to set ToolName (or deliberately sends an empty name) bypasses an explicitly configured allowlist — a fail-open security regression.
Correct behavior: if AllowedTools is configured, an empty ToolName should be denied:
if len(cfg.AllowedTools) > 0 && !containsExact(cfg.AllowedTools, req.ToolName) {
return formalDecision{errorCode: formalErrorToolNotAllowed}
}There is also no test that verifies this case — add one that asserts an empty ToolName is denied when AllowedTools is non-empty.
There was a problem hiding this comment.
Fixed in commit fix: align formal MCP access-control tests with canonical error codes and spec guard order. The req.ToolName != "" guard was removed, so the tool allowlist check is len(cfg.AllowedTools) > 0 && !containsExact(cfg.AllowedTools, req.ToolName). An empty ToolName with a non-empty allowlist correctly denies.
| if !formalRepositoryAllowed(cfg.Repos, req.Repository) { | ||
| return formalDecision{errorCode: formalErrorRepoNotAllowed} | ||
| } | ||
| if len(cfg.Roles) > 0 && !containsExact(cfg.Roles, req.UserRole) { |
There was a problem hiding this comment.
Blocked-user guard order contradicts the formal spec: the implementation checks BlockedUsers first (before repo match), but the README defines P5_NotBlocked as the 5th predicate after P1_RepoMatch – P4_ToolAllowed.
💡 Why this matters
The README states: ALLOW(r,c) ≜ P1_RepoMatch ∧ P2_RoleAllow ∧ P3_PrivateRepoAllow ∧ P4_ToolAllowed ∧ P5_NotBlocked ∧ P6_IntegrityMet.
It also says: _The
There was a problem hiding this comment.
Fixed in commit fix: align formal MCP access-control tests with canonical error codes and spec guard order. Blocked-user check now occurs after tool, repo, role, and private-repo guards, matching the spec's integrity-management phase (P5_NotBlocked). TestFormal_ErrorCodeFirstFailingGuard has a table case for each guard as the first failure.
| return 0 | ||
| case "unapproved": | ||
| return 1 | ||
| case "approved": |
There was a problem hiding this comment.
Unrecognized MinIntegrity value silently disables the integrity guard (fail-open): formalIntegrityRank returns -1 for any unknown string, so a misspelled MinIntegrity (e.g. "Approved" instead of "approved") causes all requests to pass the integrity check.
💡 Detail and suggested fix
func formalIntegrityRank(level string) int {
switch strings.ToLower(level) {
// ...
default:
return -1 // unknown level
}
}If cfg.MinIntegrity = "Approvd" (typo), formalIntegrityRank("Approvd") returns -1.
Any content integrity value's rank will be >= -1, so the guard rank(content) < rank(minIntegrity) becomes rank(content) < -1, which is never true.
Every request passes — the integrity gate is silently gone.
The fix is to distinguish \unknown
There was a problem hiding this comment.
Fixed in commit fix: split integrity failure modes, clarify fail-safe semantics. formalEvaluateAccess now explicitly checks cfgRank < 0 first (fail-safe deny for unrecognized MinIntegrity) before reqRank < cfgRank, with separate comments for each mode. The test TestFormal_UnknownIntegrityLevelDenied covers both cases.
| if cfg.PrivateRepos != nil && !*cfg.PrivateRepos && req.IsPrivate { | ||
| return formalDecision{errorCode: formalErrorPrivateRepoDenied} | ||
| } | ||
| if len(cfg.AllowedTools) > 0 && req.ToolName != "" && !containsExact(cfg.AllowedTools, req.ToolName) { |
There was a problem hiding this comment.
Empty Roles slice vs nil semantics undocumented and potentially dangerous: len(cfg.Roles) > 0 treats both nil and []string{} as \no
PR Triage
Score breakdown: Impact 18 · Urgency 8 · Quality 12 Formalizes MCP access-control conformance model + adds predicate-mapped tests. No CI results; CHANGES_REQUESTED review needs resolution. Low code risk.
|
🤖 PR Triage Report
Rationale: Formalizes MCP access-control conformance model with predicate-mapped test suite (371 lines added, 3 files). No CI checks visible; changes requested. Pair with other compliance/test PRs for review.
|
|
@copilot please run the Unresolved review feedback to address:
|
… and spec guard order Co-authored-by: gh-aw-bot <259018956+gh-aw-bot@users.noreply.github.com>
Addressed all unresolved review threads. Changes pushed in commit
Local |
|
@copilot please run the
|
…vel tests Co-authored-by: gh-aw-bot <259018956+gh-aw-bot@users.noreply.github.com>
…te coverage map Co-authored-by: gh-aw-bot <259018956+gh-aw-bot@users.noreply.github.com>
…te coverage map and run command Co-authored-by: gh-aw-bot <259018956+gh-aw-bot@users.noreply.github.com>
Co-authored-by: gh-aw-bot <259018956+gh-aw-bot@users.noreply.github.com>
All remaining review feedback has been addressed. Summary of changes since last run:
Local |
|
@copilot please run the Unresolved review feedback to address:
|
- Add TestFormal_FixtureRunner that loads YAML fixture files from
specs/github-mcp-access-control-compliance/ and drives each scenario
through formalEvaluateAccess, binding the spec artifacts to the
executable formal model
- Fix all fixture YAML error codes to match canonical values:
- exact-match-allow: repo deny -32001 → -32002
- wildcard-deny: repo deny -32001 → -32002; replace unsupported prefix
wildcard scenario with */repo wildcard-owner scenarios (C+D)
- empty-repos-block: absent repos = allow all per §4.4.1; empty repos
deny -32001 → -32002; update description and spec refs
- role-deny: role deny -32002 → -32003
- private-repo-block: private deny -32003 → -32004
- blocked-user-deny: blocked deny -32004 → -32005
- tool-name-filter: tool deny -32005 → -32001; fix description
- combined-filter-allow: -32001→-32002, -32002→-32003; fix scenario E
logic (private-repos:false + is_private:true, code -32004)
- Update README to document the fixture runner run command and
reorder scenarios C/D in combined-filter-allow for logical order
Co-authored-by: gh-aw-bot <259018956+gh-aw-bot@users.noreply.github.com>
… runner Co-authored-by: gh-aw-bot <259018956+gh-aw-bot@users.noreply.github.com>
Addressed. Changes pushed in commits
|
This PR formalizes GitHub MCP access-control compliance for the fixture spec by expressing the decision function as a conjunction of guard predicates and binding each normative predicate/invariant to executable tests. It adds explicit coverage for repo scope, role filtering, private-repo gating, tool allowlists, blocked-user safety, integrity ordering, and first-failing-guard error semantics.
Formal spec alignment
specs/github-mcp-access-control-compliance/README.mdwith:AccessRequest × ToolConfig → Decision)TestFormal_*functionsExecutable formal conformance tests
pkg/workflow/github_mcp_access_control_formal_test.gowith predicate-mapped tests:P1/P2/P3: exact/wildcard/empty-repos behaviorP4/P5/P6/P7/P8: role, private-repo, blocked-user, tool-name, integrity checksINV1/INV2: all-guards-required and first-failure error-code selectionMinimal in-test model harness