diff --git a/docs/adr/44790-formalize-github-mcp-access-control-guard-conjunction.md b/docs/adr/44790-formalize-github-mcp-access-control-guard-conjunction.md new file mode 100644 index 00000000000..7c84b02a49d --- /dev/null +++ b/docs/adr/44790-formalize-github-mcp-access-control-guard-conjunction.md @@ -0,0 +1,58 @@ +# ADR-44790: Formalize GitHub MCP Access-Control Decision as a Guard Conjunction + +**Date**: 2026-07-10 +**Status**: Draft +**Deciders**: pelikhan, copilot-swe-agent + +--- + +### Context + +The GitHub MCP access-control compliance suite previously used a fixture-driven approach: each test fixture described an input `ToolConfig` + `AccessRequest` pair and an expected outcome (allow/deny). This left the decision function implicit — there was no single authoritative statement of which predicates must hold for access to be granted, in what order they are evaluated, or which error code is returned when multiple guards fail simultaneously. + +As the number of normative requirements grew (repo scope, role filtering, private-repo gating, tool allowlists, blocked-user safety, and integrity ordering — §§4–10 of the spec), the absence of a formal model made it difficult to reason about completeness of test coverage or to verify that implementations honour the first-failing-guard semantics required by the spec. This PR was the direct consequence of that gap: a formal model was needed to tie predicates to tests in an auditable way. + +### Decision + +We will express the GitHub MCP access-control decision function as a deterministic conjunction of six ordered guard predicates (`P1_RepoMatch ∧ P2_RoleAllow ∧ P3_PrivateRepoAllow ∧ P4_ToolAllowed ∧ P5_NotBlocked ∧ P6_IntegrityMet`), document the conjunction in the compliance spec (`specs/github-mcp-access-control-compliance/README.md`), and bind each predicate to an executable conformance test in a self-contained in-test mini-evaluator (`pkg/workflow/github_mcp_access_control_formal_test.go`). The denial error code is always the code of the first failing guard in evaluation order. + +### Alternatives Considered + +#### Alternative 1: Maintain fixture-only compliance coverage + +Keep the existing fixture-based approach and add more fixtures to cover the new predicates, without introducing a formal model or a standalone evaluator. + +This was rejected because it keeps the decision function implicit. There is no single place where a reader can see all six guards, their evaluation order, and the first-failing-guard rule. New contributors and compliance auditors must reconstruct the model by reading all fixtures. It also makes it impossible to write invariant-style safety properties (e.g., "blocked users are _always_ denied regardless of all other conditions") without either duplication or framework support that the fixture runner does not provide. + +#### Alternative 2: Use a dedicated formal-specification language (TLA+, Alloy, or Coq) + +Express the access-control model in a formal specification language outside the Go test suite, and generate or manually write Go conformance tests that mirror the spec. + +This was rejected because it introduces a toolchain and expertise requirement separate from the existing Go environment. It also creates a two-language synchronisation burden: every change to the spec must be reflected in the Go tests independently. The in-test mini-evaluator approach keeps specification and conformance tests in the same file, in the same language, reviewed and maintained together. + +#### Alternative 3: Extract the evaluator into a shared production package and test against it directly + +Instead of a self-contained in-test evaluator, promote the formal model to a production `pkg/mcp/accesscontrol` package and write the predicate-mapped tests against the real implementation. + +This was considered and deferred rather than rejected. It would eliminate the risk of the test model drifting from the real implementation (see Negative consequences). However, the real access-control logic is currently distributed across multiple locations without a single canonical evaluator, so extracting it first would require a larger refactor outside the scope of this PR. The in-test evaluator was chosen as a first step: it documents the intended semantics precisely enough that the canonical implementation can be validated against it later. + +### Consequences + +#### Positive +- The guard conjunction, evaluation order, and first-failing-guard denial-code rule are now documented in the compliance spec (`README.md`) and enforced by executable tests — a single source of truth for the formal model. +- Each normative predicate (P1–P6) and each safety invariant (INV1, INV2, SAFETY_BlockedUser, SAFETY_NoSpuriousAllow) is mapped to a named `TestFormal_*` function in the behavioral coverage map, making coverage audits straightforward. +- Adding a new access-control dimension requires only: (a) adding a guard predicate to the formal model in README.md, (b) adding a branch to `formalEvaluateAccess`, and (c) writing a corresponding `TestFormal_` function — a clear, low-friction extension path. +- Safety properties that would require many fixtures to express (e.g., "blocked user is always denied regardless of other conditions") are now expressible as single invariant tests. + +#### Negative +- The in-test mini-evaluator (`formalEvaluateAccess`) is a parallel implementation of the production access-control logic. If the real production logic changes without a corresponding update to the formal test model, the tests will still pass while the production behaviour diverges from the spec. +- The formal model uses a fixed evaluation order (BlockedUser checked first, IntegrityMet checked last), which the real implementation must also honour. This is not enforced by a compiler or type system — only by convention and code review. + +#### Neutral +- The `formalEvaluateAccess` function and its supporting types (`formalToolConfig`, `formalAccessRequest`, `formalDecision`) are package-internal to `workflow` tests (build tag `!integration`). They are not exported and do not affect the public API. +- The predicate numbering in the spec (P1–P6) does not match the guard evaluation order in the code (blocked-user check runs before repo-match check). This is by design — the spec numbers reflect conceptual grouping while the code reflects safety-first ordering — but reviewers unfamiliar with the design may find this surprising. +- The `containsExact` helper added in this file shadows or duplicates any similar helper in the `workflow` package. [TODO: verify whether a `containsExact` already exists elsewhere in the package and consolidate if so.] + +--- + +*ADR created by [adr-writer agent]. Review and finalize before changing status from Draft to Accepted.* diff --git a/pkg/workflow/github_mcp_access_control_formal_test.go b/pkg/workflow/github_mcp_access_control_formal_test.go new file mode 100644 index 00000000000..ddd9e012f1d --- /dev/null +++ b/pkg/workflow/github_mcp_access_control_formal_test.go @@ -0,0 +1,495 @@ +//go:build !integration + +package workflow + +import ( + "os" + "path/filepath" + "slices" + "strings" + "testing" + + "github.com/stretchr/testify/assert" + "github.com/stretchr/testify/require" + yamlv3 "gopkg.in/yaml.v3" +) + +// Guard-policy error codes, aligned with pkg/cli/gateway_logs_types.go and the normative +// GitHub MCP access-control specification (Appendix B). +const ( + formalErrorToolNotAllowed = -32001 // tool not in allowed-tools (general access denied) + formalErrorRepoNotAllowed = -32002 // repos guard failed + formalErrorInsufficientRole = -32003 // roles guard failed + formalErrorPrivateRepoDenied = -32004 // private-repos: false guard failed + formalErrorBlockedUser = -32005 // blocked-users guard failed (within integrity management) + formalErrorIntegrityTooLow = -32006 // min-integrity guard failed +) + +type formalToolConfig struct { + Repos []string + Roles []string + PrivateRepos *bool + AllowedTools []string + BlockedUsers []string + MinIntegrity string +} + +type formalAccessRequest struct { + Repository string + UserRole string + IsPrivate bool + ToolName string + UserLogin string + ContentIntegrity string +} + +func TestFormal_ExactMatchAllow(t *testing.T) { + allowed := formalEvaluateAccess(formalToolConfig{Repos: []string{"github/gh-aw"}}, formalAccessRequest{Repository: "github/gh-aw"}) + denied := formalEvaluateAccess(formalToolConfig{Repos: []string{"github/gh-aw"}}, formalAccessRequest{Repository: "github/other"}) + + assert.True(t, allowed.allow) + assert.False(t, denied.allow) + assert.Equal(t, formalErrorRepoNotAllowed, denied.errorCode) +} + +func TestFormal_WildcardMatch(t *testing.T) { + // owner/* — all repos under an owner + assert.True(t, formalEvaluateAccess(formalToolConfig{Repos: []string{"github/*"}}, formalAccessRequest{Repository: "github/gh-aw"}).allow) + assert.False(t, formalEvaluateAccess(formalToolConfig{Repos: []string{"github/*"}}, formalAccessRequest{Repository: "microsoft/vscode"}).allow) + // */repo — exact repo name under any owner + assert.True(t, formalEvaluateAccess(formalToolConfig{Repos: []string{"*/gh-aw"}}, formalAccessRequest{Repository: "github/gh-aw"}).allow) + assert.False(t, formalEvaluateAccess(formalToolConfig{Repos: []string{"*/gh-aw"}}, formalAccessRequest{Repository: "github/other"}).allow) + // */* — full wildcard (equivalent to no repos restriction) + assert.True(t, formalEvaluateAccess(formalToolConfig{Repos: []string{"*/*"}}, formalAccessRequest{Repository: "any/repo"}).allow) +} + +func TestFormal_OmittedReposAllowAll(t *testing.T) { + // P1_RepoMatch: omitted repos field means "no restriction" — all accessible repos are allowed (spec §4.4.1). + assert.True(t, formalEvaluateAccess(formalToolConfig{}, formalAccessRequest{Repository: "github/gh-aw"}).allow) + assert.True(t, formalEvaluateAccess(formalToolConfig{}, formalAccessRequest{Repository: "microsoft/vscode"}).allow) + + // An empty slice is an invalid configuration (rejected at compilation; see TestValidateGitHubGuardPolicy + // in tools_validation_test.go). In the runtime formal model it is treated as no-match. + assert.False(t, formalEvaluateAccess(formalToolConfig{Repos: []string{}}, formalAccessRequest{Repository: "github/gh-aw"}).allow) +} + +func TestFormal_RoleFilter(t *testing.T) { + cfg := formalToolConfig{Repos: []string{"*/*"}, Roles: []string{"write", "admin"}} + assert.True(t, formalEvaluateAccess(cfg, formalAccessRequest{Repository: "github/gh-aw", UserRole: "write"}).allow) + denied := formalEvaluateAccess(cfg, formalAccessRequest{Repository: "github/gh-aw", UserRole: "read"}) + assert.False(t, denied.allow) + assert.Equal(t, formalErrorInsufficientRole, denied.errorCode) +} + +func TestFormal_PrivateRepoControl(t *testing.T) { + allowPrivate := true + denyPrivate := false + + assert.True(t, formalEvaluateAccess(formalToolConfig{Repos: []string{"myorg/*"}, PrivateRepos: &allowPrivate}, formalAccessRequest{Repository: "myorg/private", IsPrivate: true}).allow) + assert.True(t, formalEvaluateAccess(formalToolConfig{Repos: []string{"myorg/*"}, PrivateRepos: &denyPrivate}, formalAccessRequest{Repository: "myorg/public", IsPrivate: false}).allow) + denied := formalEvaluateAccess(formalToolConfig{Repos: []string{"myorg/*"}, PrivateRepos: &denyPrivate}, formalAccessRequest{Repository: "myorg/private", IsPrivate: true}) + assert.False(t, denied.allow) + assert.Equal(t, formalErrorPrivateRepoDenied, denied.errorCode) +} + +func TestFormal_BlockedUserDeny(t *testing.T) { + cfg := formalToolConfig{Repos: []string{"github/gh-aw"}, Roles: []string{"write"}, BlockedUsers: []string{"bad-actor"}} + assert.True(t, formalEvaluateAccess(cfg, formalAccessRequest{ + Repository: "github/gh-aw", UserRole: "write", UserLogin: "good-actor", ContentIntegrity: "approved", + }).allow) + denied := formalEvaluateAccess(cfg, formalAccessRequest{ + Repository: "github/gh-aw", UserRole: "write", UserLogin: "bad-actor", ContentIntegrity: "approved", + }) + assert.False(t, denied.allow) + assert.Equal(t, formalErrorBlockedUser, denied.errorCode) +} + +func TestFormal_ToolNameFilter(t *testing.T) { + cfg := formalToolConfig{Repos: []string{"*/*"}, AllowedTools: []string{"issue_read"}} + assert.True(t, formalEvaluateAccess(cfg, formalAccessRequest{Repository: "github/gh-aw", ToolName: "issue_read"}).allow) + // no AllowedTools configured → any tool is allowed + assert.True(t, formalEvaluateAccess(formalToolConfig{Repos: []string{"*/*"}}, formalAccessRequest{Repository: "github/gh-aw", ToolName: "delete_repo"}).allow) + // tool not in allowlist + denied := formalEvaluateAccess(cfg, formalAccessRequest{Repository: "github/gh-aw", ToolName: "delete_repo"}) + assert.False(t, denied.allow) + assert.Equal(t, formalErrorToolNotAllowed, denied.errorCode) + // empty tool name with a non-empty allowlist must also deny (the tool is not present) + deniedEmpty := formalEvaluateAccess(cfg, formalAccessRequest{Repository: "github/gh-aw", ToolName: ""}) + assert.False(t, deniedEmpty.allow) + assert.Equal(t, formalErrorToolNotAllowed, deniedEmpty.errorCode) +} + +func TestFormal_IntegrityLevelOrder(t *testing.T) { + assert.True(t, formalEvaluateAccess(formalToolConfig{Repos: []string{"*/*"}, MinIntegrity: "approved"}, formalAccessRequest{Repository: "github/gh-aw", ContentIntegrity: "approved"}).allow) + assert.True(t, formalEvaluateAccess(formalToolConfig{Repos: []string{"*/*"}, MinIntegrity: "approved"}, formalAccessRequest{Repository: "github/gh-aw", ContentIntegrity: "merged"}).allow) + denied := formalEvaluateAccess(formalToolConfig{Repos: []string{"*/*"}, MinIntegrity: "approved"}, formalAccessRequest{Repository: "github/gh-aw", ContentIntegrity: "unapproved"}) + assert.False(t, denied.allow) + assert.Equal(t, formalErrorIntegrityTooLow, denied.errorCode) +} + +func TestFormal_UnknownContentIntegrityDenied(t *testing.T) { + // An unknown ContentIntegrity value (rank -1) is below any valid minimum threshold. + denied := formalEvaluateAccess( + formalToolConfig{Repos: []string{"*/*"}, MinIntegrity: "approved"}, + formalAccessRequest{Repository: "github/gh-aw", ContentIntegrity: "unknown-level"}, + ) + assert.False(t, denied.allow) + assert.Equal(t, formalErrorIntegrityTooLow, denied.errorCode) +} + +func TestFormal_InvalidMinIntegrityConfigDenied(t *testing.T) { + // An unrecognized MinIntegrity configuration is fail-safe: denies all requests. + denied := formalEvaluateAccess( + formalToolConfig{Repos: []string{"*/*"}, MinIntegrity: "invalid"}, + formalAccessRequest{Repository: "github/gh-aw", ContentIntegrity: "merged"}, + ) + assert.False(t, denied.allow) + assert.Equal(t, formalErrorIntegrityTooLow, denied.errorCode) +} + +func TestFormal_CombinedFiltersAllAllow(t *testing.T) { + allowPrivate := true + cfg := formalToolConfig{ + Repos: []string{"github/gh-aw"}, + Roles: []string{"write"}, + PrivateRepos: &allowPrivate, + AllowedTools: []string{"issue_read"}, + MinIntegrity: "approved", + } + assert.True(t, formalEvaluateAccess(cfg, formalAccessRequest{ + Repository: "github/gh-aw", UserRole: "write", IsPrivate: true, ToolName: "issue_read", UserLogin: "good-user", ContentIntegrity: "approved", + }).allow) +} + +func TestFormal_ErrorCodeFirstFailingGuard(t *testing.T) { + // INV2: the denial code is selected by the FIRST failing guard in evaluation order: + // tool → repo → role → private-repo → blocked-user → integrity + // + // Each case makes one guard the first failure while one or more later guards also fail, + // ensuring that only the first guard's code is returned. + denyPrivate := false + cfg := formalToolConfig{ + Repos: []string{"github/gh-aw"}, + Roles: []string{"write"}, + PrivateRepos: &denyPrivate, + AllowedTools: []string{"issue_read"}, + BlockedUsers: []string{"bad-actor"}, + MinIntegrity: "approved", + } + + cases := []struct { + name string + req formalAccessRequest + wantCode int + }{ + { + name: "tool guard fails first (repo/role/private/blocked/integrity also fail)", + req: formalAccessRequest{ + Repository: "github/other", UserRole: "read", IsPrivate: true, + ToolName: "delete_repo", UserLogin: "bad-actor", ContentIntegrity: "none", + }, + wantCode: formalErrorToolNotAllowed, + }, + { + name: "repo guard fails first (role/private/blocked/integrity also fail)", + req: formalAccessRequest{ + Repository: "github/other", UserRole: "read", IsPrivate: true, + ToolName: "issue_read", UserLogin: "bad-actor", ContentIntegrity: "none", + }, + wantCode: formalErrorRepoNotAllowed, + }, + { + name: "role guard fails first (private/blocked/integrity also fail)", + req: formalAccessRequest{ + Repository: "github/gh-aw", UserRole: "read", IsPrivate: true, + ToolName: "issue_read", UserLogin: "bad-actor", ContentIntegrity: "none", + }, + wantCode: formalErrorInsufficientRole, + }, + { + name: "private-repo guard fails first (blocked/integrity also fail)", + req: formalAccessRequest{ + Repository: "github/gh-aw", UserRole: "write", IsPrivate: true, + ToolName: "issue_read", UserLogin: "bad-actor", ContentIntegrity: "none", + }, + wantCode: formalErrorPrivateRepoDenied, + }, + { + name: "blocked-user guard fails first within integrity (integrity also fails)", + // PrivateRepos must allow private so private check passes. + // Use a separate cfg that allows private repos so private guard is not the first failure. + req: formalAccessRequest{ + Repository: "github/gh-aw", UserRole: "write", IsPrivate: false, + ToolName: "issue_read", UserLogin: "bad-actor", ContentIntegrity: "none", + }, + wantCode: formalErrorBlockedUser, + }, + { + name: "integrity guard fails (all earlier guards pass)", + req: formalAccessRequest{ + Repository: "github/gh-aw", UserRole: "write", IsPrivate: false, + ToolName: "issue_read", UserLogin: "good-actor", ContentIntegrity: "none", + }, + wantCode: formalErrorIntegrityTooLow, + }, + } + + // The cfg uses denyPrivate=false; IsPrivate=true triggers the private-repo guard, and + // IsPrivate=false bypasses it — so blocked-user and integrity guards can be the first failure. + + for _, tc := range cases { + t.Run(tc.name, func(t *testing.T) { + d := formalEvaluateAccess(cfg, tc.req) + assert.False(t, d.allow) + assert.Equal(t, tc.wantCode, d.errorCode) + }) + } +} + +func TestFormal_BlockedUserSafetyProperty(t *testing.T) { + // SAFETY_BlockedUserAlwaysDenied: a blocked user is always denied, even when all other guards + // (tool, repo, role, private-repo) pass. Blocked-user is the first integrity-management guard. + allowPrivate := true + cfg := formalToolConfig{ + Repos: []string{"*/*"}, + Roles: []string{"admin"}, + PrivateRepos: &allowPrivate, + AllowedTools: []string{"issue_read"}, + BlockedUsers: []string{"blocked"}, + MinIntegrity: "merged", + } + + denied := formalEvaluateAccess(cfg, formalAccessRequest{ + Repository: "any/repo", UserRole: "admin", IsPrivate: false, + ToolName: "issue_read", UserLogin: "blocked", ContentIntegrity: "merged", + }) + + assert.False(t, denied.allow) + assert.Equal(t, formalErrorBlockedUser, denied.errorCode) +} + +func TestFormal_NoSpuriousAllowInvariant(t *testing.T) { + allowPrivate := true + cfg := formalToolConfig{ + Repos: []string{"github/gh-aw"}, + Roles: []string{"write"}, + PrivateRepos: &allowPrivate, + AllowedTools: []string{"issue_read"}, + BlockedUsers: []string{"blocked"}, + MinIntegrity: "approved", + } + + cases := []formalAccessRequest{ + {Repository: "github/other", UserRole: "write", ToolName: "issue_read", ContentIntegrity: "approved"}, + {Repository: "github/gh-aw", UserRole: "read", ToolName: "issue_read", ContentIntegrity: "approved"}, + {Repository: "github/gh-aw", UserRole: "write", ToolName: "delete_repo", ContentIntegrity: "approved"}, + {Repository: "github/gh-aw", UserRole: "write", ToolName: "issue_read", ContentIntegrity: "none"}, + {Repository: "github/gh-aw", UserRole: "write", UserLogin: "blocked", ToolName: "issue_read", ContentIntegrity: "approved"}, + } + + for _, req := range cases { + assert.False(t, formalEvaluateAccess(cfg, req).allow) + } +} + +type formalDecision struct { + allow bool + errorCode int +} + +func formalEvaluateAccess(cfg formalToolConfig, req formalAccessRequest) formalDecision { + // Guard evaluation order (spec §4.5.3): + // 1. Tool selection (allowed-tools) + // 2. Repository access control: repo → role → private-repo visibility + // 3. Integrity management: blocked-user → min-integrity threshold + 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) + // Fail-safe: an unrecognized MinIntegrity configuration value is treated as deny-all. + if cfgRank < 0 { + return formalDecision{errorCode: formalErrorIntegrityTooLow} + } + // Deny if content integrity is below (or unrecognized — rank -1) the configured minimum. + if reqRank < cfgRank { + return formalDecision{errorCode: formalErrorIntegrityTooLow} + } + } + return formalDecision{allow: true} +} + +func formalRepositoryAllowed(patterns []string, repository string) bool { + // nil patterns means the repos field is omitted: all accessible repositories are allowed (spec §4.4.1). + if patterns == nil { + return true + } + // Empty slice is an invalid configuration (rejected at compilation); runtime treats as no-match. + if len(patterns) == 0 { + return false + } + repoOwner, repoName, ok := strings.Cut(repository, "/") + if !ok || repoOwner == "" || repoName == "" { + return false + } + + for _, pattern := range patterns { + patternOwner, patternRepo, ok := strings.Cut(pattern, "/") + if !ok { + continue + } + switch { + case patternOwner == "*" && patternRepo == "*": + return true + case patternOwner == "*" && patternRepo == repoName: + // */repo — matches exact repo name under any owner + return true + case patternOwner == repoOwner && patternRepo == "*": + return true + case patternOwner == repoOwner && patternRepo == repoName: + return true + } + } + return false +} + +func formalIntegrityRank(level string) int { + switch strings.ToLower(level) { + case "none": + return 0 + case "unapproved": + return 1 + case "approved": + return 2 + case "merged": + return 3 + default: + return -1 + } +} + +func containsExact(values []string, needle string) bool { + return slices.Contains(values, needle) +} + +// --------------------------------------------------------------------------- +// Compliance fixture runner +// --------------------------------------------------------------------------- +// fixtureFile mirrors the top-level YAML structure for the compliance fixture files +// located at specs/github-mcp-access-control-compliance/*.yaml. +type fixtureFile struct { + FixtureID string `yaml:"fixture_id"` + Description string `yaml:"description"` + Scenarios []fixtureScenario `yaml:"scenarios"` +} + +type fixtureScenario struct { + ScenarioID string `yaml:"scenario_id"` + Description string `yaml:"description"` + Input fixtureInput `yaml:"input"` + Expected fixtureExpected `yaml:"expected"` +} + +type fixtureInput struct { + ToolConfig fixtureToolConfig `yaml:"tool_config"` + Request fixtureRequest `yaml:"request"` +} + +type fixtureToolConfig struct { + Repos []string `yaml:"repos"` + Roles []string `yaml:"roles"` + PrivateRepos *bool `yaml:"private-repos"` + AllowedTools []string `yaml:"allowed-tools"` + BlockedUsers []string `yaml:"blocked-users"` + MinIntegrity string `yaml:"min-integrity"` +} + +type fixtureRequest struct { + Repository string `yaml:"repository"` + UserRole string `yaml:"user_role"` + IsPrivate bool `yaml:"is_private"` + ToolName string `yaml:"tool_name"` + UserLogin string `yaml:"user_login"` + ContentIntegrity string `yaml:"content_integrity"` +} + +type fixtureExpected struct { + Decision string `yaml:"decision"` + ErrorCode *int `yaml:"error_code"` + Reason string `yaml:"reason"` +} + +// TestFormal_FixtureRunner loads every YAML fixture from +// specs/github-mcp-access-control-compliance/ and verifies each scenario against +// formalEvaluateAccess. This binds the executable formal model to the YAML spec +// artifacts so that a divergence between the fixture and the evaluator is caught +// immediately rather than silently. +func TestFormal_FixtureRunner(t *testing.T) { + fixtureDir := filepath.Join("..", "..", "specs", "github-mcp-access-control-compliance") + entries, err := os.ReadDir(fixtureDir) + require.NoError(t, err, "failed to read compliance fixture directory") + + var totalScenarios int + for _, entry := range entries { + if entry.IsDir() || filepath.Ext(entry.Name()) != ".yaml" { + continue + } + + fixturePath := filepath.Join(fixtureDir, entry.Name()) + data, err := os.ReadFile(fixturePath) + require.NoErrorf(t, err, "failed to read fixture file %s", entry.Name()) + + var ff fixtureFile + require.NoErrorf(t, yamlv3.Unmarshal(data, &ff), "failed to parse fixture file %s", entry.Name()) + + for _, sc := range ff.Scenarios { + totalScenarios++ + t.Run(sc.ScenarioID, func(t *testing.T) { + cfg := formalToolConfig{ + Repos: sc.Input.ToolConfig.Repos, + Roles: sc.Input.ToolConfig.Roles, + PrivateRepos: sc.Input.ToolConfig.PrivateRepos, + AllowedTools: sc.Input.ToolConfig.AllowedTools, + BlockedUsers: sc.Input.ToolConfig.BlockedUsers, + MinIntegrity: sc.Input.ToolConfig.MinIntegrity, + } + req := formalAccessRequest{ + Repository: sc.Input.Request.Repository, + UserRole: sc.Input.Request.UserRole, + IsPrivate: sc.Input.Request.IsPrivate, + ToolName: sc.Input.Request.ToolName, + UserLogin: sc.Input.Request.UserLogin, + ContentIntegrity: sc.Input.Request.ContentIntegrity, + } + + got := formalEvaluateAccess(cfg, req) + + if sc.Expected.Decision == "allow" { + assert.True(t, got.allow, "%s: expected allow, got deny (code %d)", sc.ScenarioID, got.errorCode) + assert.Zero(t, got.errorCode, "%s: allow decision must have zero error code", sc.ScenarioID) + } else { + assert.False(t, got.allow, "%s: expected deny, got allow", sc.ScenarioID) + if sc.Expected.ErrorCode != nil { + assert.Equal(t, *sc.Expected.ErrorCode, got.errorCode, + "%s: wrong error code (decision=%s)", sc.ScenarioID, sc.Expected.Decision) + } + } + }) + } + } + + require.Positive(t, totalScenarios, "fixture runner found no scenarios — check fixture directory path") +} diff --git a/specs/github-mcp-access-control-compliance/README.md b/specs/github-mcp-access-control-compliance/README.md index 2eac652a074..c5b7651b5d0 100644 --- a/specs/github-mcp-access-control-compliance/README.md +++ b/specs/github-mcp-access-control-compliance/README.md @@ -7,13 +7,69 @@ Each fixture describes a test scenario with an input tool configuration and the access-control decision. Fixtures are consumed by the compliance test runner to verify that implementations satisfy the normative requirements in §§4–10 of the specification. +## Formal Model + +Let: + +- `r ∈ AccessRequest` +- `c ∈ ToolConfig` +- `Decision(r, c) ∈ {allow, deny(code)}` + +The runtime decision is a conjunction of six guard predicates evaluated in the documented +order (spec §4.5.3): + +``` +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) +``` + +**Evaluation order** (§4.5.3): +1. **Tool selection** — `allowed-tools` filter determines which tools are available +2. **Repository access control** — repo scope, role, and visibility are evaluated +3. **Integrity management** — blocked-user author check, then min-integrity threshold + +Where: + +- `P1_ToolAllowed`: if `allowed-tools` is configured, the requested tool name must be present; an empty or absent tool name against a non-empty list also denies +- `P2_RepoMatch`: if `repos` is configured, repository matches at least one pattern (`owner/repo`, `owner/*`, `*/repo`, `*/*`); omitted `repos` allows all accessible repositories; empty array is a compile-time validation error (§4.4.1) +- `P3_RoleAllow`: if `roles` is configured, user role matches one configured role (OR-logic) +- `P4_PrivateRepoAllow`: private repository access is denied when `private-repos: false` +- `P5_NotBlocked`: blocked users are denied within integrity management (author check) +- `P6_IntegrityMet`: integrity ordering is enforced as `none < unapproved < approved < merged` + +The denial code is selected by the first failing guard in the evaluation order above. + +## Behavioral Coverage Map + +| Predicate / Invariant | Test Function | Description | +|---|---|---| +| `P1_ToolAllowed` (exact allow) | `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/*` and `*/repo` wildcard patterns; `*/*` full wildcard | +| `P2_RepoMatch` (omitted) | `TestFormal_OmittedReposAllowAll` | Omitted `repos` allows all accessible repositories; empty array is invalid config | +| `P3_RoleAllow` | `TestFormal_RoleFilter` | Role OR-logic: matching role allows, insufficient role denies | +| `P4_PrivateRepoAllow` | `TestFormal_PrivateRepoControl` | `private-repos: false` blocks private repos; public repos unaffected | +| `P5_NotBlocked` | `TestFormal_BlockedUserDeny` | Blocked user denied within integrity management | +| `P6_IntegrityMet` | `TestFormal_IntegrityLevelOrder` | Integrity ordinal order enforced; content below threshold denied | +| `P6_IntegrityMet` (unknown content) | `TestFormal_UnknownContentIntegrityDenied` | Unknown `ContentIntegrity` value (rank -1) is below any valid minimum threshold → denied | +| `P6_IntegrityMet` (invalid config) | `TestFormal_InvalidMinIntegrityConfigDenied` | Unrecognized `MinIntegrity` config is fail-safe: denies all requests | +| `INV1_CombinedAllow` | `TestFormal_CombinedFiltersAllAllow` | All conditions must be satisfied for allow | +| `INV2_ErrorCode` | `TestFormal_ErrorCodeFirstFailingGuard` | Deny error code matches first failing guard; table covers each guard as first failure | +| `SAFETY_BlockedUserAlwaysDenied` | `TestFormal_BlockedUserSafetyProperty` | Safety: blocked user always produces `-32005` when all earlier guards pass | +| `SAFETY_NoSpuriousAllow` | `TestFormal_NoSpuriousAllowInvariant` | Safety: no allow decision when any guard fails | + ## Fixture Files | Filename | Scenario | Spec Coverage | |---|---|---| | `exact-match-allow.yaml` | Exact repository pattern allows matching repo | T-GH-011, T-GH-012 | | `wildcard-deny.yaml` | Owner-wildcard pattern denies non-matching owner | T-GH-013, T-GH-014 | -| `empty-repos-block.yaml` | Absent or empty `repos` list denies all repository access | T-GH-015, T-GH-016 | +| `empty-repos-block.yaml` | Empty `repos` array is rejected at compile time | T-GH-015, T-GH-016 | | `role-deny.yaml` | Role filter denies access when user role is insufficient | T-GH-019, T-GH-020 | | `tool-name-filter.yaml` | `allowed-tools` filter allows or denies by tool name | T-GH-031, T-GH-032, T-GH-033 | | `blocked-user-deny.yaml` | `blocked-users` denies listed actors unconditionally | T-GH-071, T-GH-072 | @@ -35,23 +91,24 @@ input: request: object # Simulated access request (repository, user, content) expected: decision: allow | deny # Required access-control outcome - error_code: integer | null # Expected MCP JSON-RPC error code on deny (e.g., -32001) + error_code: integer | null # Expected MCP JSON-RPC error code on deny (e.g., -32002) reason: string # Expected denial reason substring (informative) ``` ## Error Code Reference When `expected.decision` is `deny`, the fixture records the MCP JSON-RPC error code that the -implementation MUST return. The codes used in these fixtures are: +implementation MUST return. The codes are defined in `pkg/cli/gateway_logs_types.go` and the +normative specification (Appendix B): | Code | Denial Reason | |---|---| -| `-32001` | Repository not on the allowlist (`repos` filter) | -| `-32002` | User role is insufficient (`role` filter) | -| `-32003` | Repository is private and `private-repos: false` | -| `-32004` | User is blocked (`blocked-users` filter) | -| `-32005` | Tool name not permitted (`allowed-tools` filter) | -| `-32006` | Content integrity level below threshold (`min-integrity` filter) | +| `-32001` | General access denied (tool not in `allowed-tools` filter) | +| `-32002` | Repository not in allowlist (`repos` filter) | +| `-32003` | Insufficient permissions (`roles` filter) | +| `-32004` | Repository is private and `private-repos: false` | +| `-32005` | Content from blocked user (`blocked-users` filter) | +| `-32006` | Content integrity below minimum threshold (`min-integrity` filter) | A `null` error code in `expected.error_code` means the scenario produces an `allow` decision and no error is returned. @@ -78,3 +135,25 @@ To run all related tests: ```bash go test -v -run "TestValidateGitHubGuardPolicy" ./pkg/workflow/ ``` + +To run the formal conformance test suite (predicate-mapped tests): + +```bash +go test -v -run "TestFormal_(ExactMatch|WildcardMatch|OmittedRepos|RoleFilter|PrivateRepo|BlockedUser|ToolName|IntegrityLevel|UnknownContent|InvalidMinIntegrity|CombinedFilters|ErrorCode|NoSpurious)" ./pkg/workflow/ +``` + +To run the YAML fixture runner (drives every scenario from the fixture files above through the formal evaluator): + +```bash +go test -v -run "TestFormal_FixtureRunner" ./pkg/workflow/ +``` + +## Generated Test Suite + +Formal conformance tests are implemented in: + +`pkg/workflow/github_mcp_access_control_formal_test.go` + +The test suite includes: +- **Predicate-mapped tests** (`TestFormal_*`) — each test maps to a specific guard predicate (P1–P6) or invariant documented in the Formal Model section above. +- **Fixture runner** (`TestFormal_FixtureRunner`) — loads every YAML fixture file from this directory and drives each scenario through the formal evaluator. This ensures the fixture files, error codes, and expected decisions remain consistent with the formal model. diff --git a/specs/github-mcp-access-control-compliance/blocked-user-deny.yaml b/specs/github-mcp-access-control-compliance/blocked-user-deny.yaml index b934a97e0b6..ac83f997ca8 100644 --- a/specs/github-mcp-access-control-compliance/blocked-user-deny.yaml +++ b/specs/github-mcp-access-control-compliance/blocked-user-deny.yaml @@ -36,7 +36,7 @@ scenarios: content_integrity: "approved" expected: decision: deny - error_code: -32004 + error_code: -32005 reason: "user is blocked" # --- Scenario B: request from a non-blocked user proceeds normally --- diff --git a/specs/github-mcp-access-control-compliance/combined-filter-allow.yaml b/specs/github-mcp-access-control-compliance/combined-filter-allow.yaml index 7b22d48f016..cd5ef058d38 100644 --- a/specs/github-mcp-access-control-compliance/combined-filter-allow.yaml +++ b/specs/github-mcp-access-control-compliance/combined-filter-allow.yaml @@ -56,12 +56,12 @@ scenarios: content_integrity: "approved" expected: decision: deny - error_code: -32001 + error_code: -32002 reason: "repository not in allowed list" - # --- Scenario D: role condition fails → denied --- - - scenario_id: "combined-filter-allow-D" - description: "Request with insufficient role is denied even when repo, visibility, and integrity match" + # --- Scenario C: integrity condition fails → denied --- + - scenario_id: "combined-filter-allow-C" + description: "Request with insufficient integrity is denied even when repo, role, and visibility match" input: tool_config: repos: @@ -72,17 +72,17 @@ scenarios: min-integrity: "approved" request: repository: "github/gh-aw" - user_role: "read" + user_role: "write" is_private: true - content_integrity: "approved" + content_integrity: "none" expected: decision: deny - error_code: -32002 - reason: "user role does not meet minimum required role" + error_code: -32006 + reason: "content integrity below minimum required level" - # --- Scenario E: private-repos condition fails → denied --- - - scenario_id: "combined-filter-allow-E" - description: "Request targeting a public repo is denied when private-repos=true requires a private repository" + # --- Scenario D: role condition fails → denied --- + - scenario_id: "combined-filter-allow-D" + description: "Request with insufficient role is denied even when repo, visibility, and integrity match" input: tool_config: repos: @@ -93,29 +93,31 @@ scenarios: min-integrity: "approved" request: repository: "github/gh-aw" - user_role: "write" - is_private: false + user_role: "read" + is_private: true content_integrity: "approved" expected: decision: deny error_code: -32003 - reason: "repository visibility does not satisfy private-repos requirement" - - scenario_id: "combined-filter-allow-C" - description: "Request with insufficient integrity is denied even when repo, role, and visibility match" + reason: "user role does not meet minimum required role" + + # --- Scenario E: private-repos condition fails → denied --- + - scenario_id: "combined-filter-allow-E" + description: "Request targeting a private repository is denied when private-repos: false" input: tool_config: repos: - "github/gh-aw" roles: - "write" - private-repos: true + private-repos: false min-integrity: "approved" request: repository: "github/gh-aw" user_role: "write" is_private: true - content_integrity: "none" + content_integrity: "approved" expected: decision: deny - error_code: -32006 - reason: "content integrity below minimum required level" + error_code: -32004 + reason: "private repository access denied" diff --git a/specs/github-mcp-access-control-compliance/empty-repos-block.yaml b/specs/github-mcp-access-control-compliance/empty-repos-block.yaml index ac051158a5e..0a59395baf1 100644 --- a/specs/github-mcp-access-control-compliance/empty-repos-block.yaml +++ b/specs/github-mcp-access-control-compliance/empty-repos-block.yaml @@ -4,34 +4,35 @@ fixture_id: "empty-repos-block" description: > - When the `repos` list is absent or empty, the tool configuration MUST deny access - to all repositories (T-GH-015, T-GH-016). An absent repos field is equivalent to - an empty allow-list: no repository matches and every request is denied. + When the `repos` field is absent (omitted), all accessible repositories are allowed (§4.4.1). + When the `repos` field is present but empty (`repos: []`), it is rejected at compile time as + an invalid configuration; at runtime the formal model treats it as a no-match, denying access + to every repository (T-GH-016). spec_refs: - - "§5.3 — An absent or empty repos list MUST deny all repository access" - - "§5.3 — T-GH-015: absent repos list denies access" - - "§5.3 — T-GH-016: empty repos list denies access" + - "§4.4.1 — Absent repos field allows all accessible repositories" + - "§5.3 — Empty repos array is a compile-time validation error; runtime treats as no-match" + - "§5.3 — T-GH-016: empty repos list results in deny at runtime" scenarios: - # --- Scenario A: absent repos field denies all repositories --- + # --- Scenario A: absent repos field allows all repositories --- - scenario_id: "empty-repos-block-A" - description: "Tool config with no repos field denies request for any repository" + description: "Tool config with no repos field allows request for any repository" input: tool_config: - # repos field is intentionally absent + # repos field is intentionally absent — all accessible repos are allowed min-integrity: "unapproved" request: repository: "github/gh-aw" content_integrity: "unapproved" expected: - decision: deny - error_code: -32001 - reason: "repository not in allowed list" + decision: allow + error_code: null + reason: "" # --- Scenario B: empty repos list denies all repositories --- - scenario_id: "empty-repos-block-B" - description: "Tool config with an empty repos: [] denies request for any repository" + description: "Tool config with an empty repos: [] denies request for any repository (invalid config; runtime no-match)" input: tool_config: repos: [] @@ -41,5 +42,5 @@ scenarios: content_integrity: "unapproved" expected: decision: deny - error_code: -32001 + error_code: -32002 reason: "repository not in allowed list" diff --git a/specs/github-mcp-access-control-compliance/exact-match-allow.yaml b/specs/github-mcp-access-control-compliance/exact-match-allow.yaml index f64bfd92994..a99fc708eba 100644 --- a/specs/github-mcp-access-control-compliance/exact-match-allow.yaml +++ b/specs/github-mcp-access-control-compliance/exact-match-allow.yaml @@ -54,5 +54,5 @@ scenarios: content_integrity: "unapproved" expected: decision: deny - error_code: -32001 + error_code: -32002 reason: "repository not in allowed list" diff --git a/specs/github-mcp-access-control-compliance/private-repo-block.yaml b/specs/github-mcp-access-control-compliance/private-repo-block.yaml index 1b97de7d20a..ae30f37125c 100644 --- a/specs/github-mcp-access-control-compliance/private-repo-block.yaml +++ b/specs/github-mcp-access-control-compliance/private-repo-block.yaml @@ -51,7 +51,7 @@ scenarios: content_integrity: "none" expected: decision: deny - error_code: -32003 + error_code: -32004 reason: "private repository access denied" # --- Scenario C: private-repos: false → public repo still allowed --- diff --git a/specs/github-mcp-access-control-compliance/role-deny.yaml b/specs/github-mcp-access-control-compliance/role-deny.yaml index eae1ca0a3ea..400f92c90c6 100644 --- a/specs/github-mcp-access-control-compliance/role-deny.yaml +++ b/specs/github-mcp-access-control-compliance/role-deny.yaml @@ -53,7 +53,7 @@ scenarios: content_integrity: "none" expected: decision: deny - error_code: -32002 + error_code: -32003 reason: "insufficient role" # --- Scenario C: user has no role in the repository → denied --- @@ -72,5 +72,5 @@ scenarios: content_integrity: "none" expected: decision: deny - error_code: -32002 + error_code: -32003 reason: "insufficient role" diff --git a/specs/github-mcp-access-control-compliance/tool-name-filter.yaml b/specs/github-mcp-access-control-compliance/tool-name-filter.yaml index 15b8e1fc3a5..99a7d39e976 100644 --- a/specs/github-mcp-access-control-compliance/tool-name-filter.yaml +++ b/specs/github-mcp-access-control-compliance/tool-name-filter.yaml @@ -6,7 +6,7 @@ fixture_id: "tool-name-filter" description: > When `allowed-tools` is configured, the MCP gateway MUST allow only the explicitly listed tool names (T-GH-031). A request invoking a tool not in the allowed list - MUST be denied with error code -32005 (T-GH-032). When `allowed-tools` is absent, + MUST be denied with error code -32001 (T-GH-032). When `allowed-tools` is absent, all tool names are permitted subject to other access controls (T-GH-033). spec_refs: @@ -53,7 +53,7 @@ scenarios: content_integrity: "unapproved" expected: decision: deny - error_code: -32005 + error_code: -32001 reason: "tool not in allowed-tools list" # --- Scenario C: absent allowed-tools permits all tool names --- diff --git a/specs/github-mcp-access-control-compliance/wildcard-deny.yaml b/specs/github-mcp-access-control-compliance/wildcard-deny.yaml index 82b8ededdc8..5f8dfd99acd 100644 --- a/specs/github-mcp-access-control-compliance/wildcard-deny.yaml +++ b/specs/github-mcp-access-control-compliance/wildcard-deny.yaml @@ -4,14 +4,16 @@ fixture_id: "wildcard-deny" description: > - An owner-wildcard pattern (e.g., "github/*") MUST allow access to any repository under the - specified owner (T-GH-013), and MUST deny access to repositories under a different owner - (T-GH-014). The wildcard matches all repository names under the given owner and does not - match across owners. + The supported wildcard forms are owner/*, */repo, and */*. An owner-wildcard pattern + (e.g., "github/*") MUST allow access to any repository under the specified owner (T-GH-013), + and MUST deny access to repositories under a different owner (T-GH-014). A wildcard-owner + pattern (e.g., "*/gh-aw") MUST allow access to the named repository under any owner, and + MUST deny access when the repo name does not match. spec_refs: - - "§5.2 — Owner wildcard matches all repositories under the specified owner" - - "§5.2 — Owner wildcard rejects repositories under a different owner" + - "§5.2 — owner/* matches all repositories under the specified owner" + - "§5.2 — owner/* rejects repositories under a different owner" + - "§5.2 — */repo matches the named repository under any owner" scenarios: # --- Scenario A: owner wildcard matches repository under same owner --- @@ -43,21 +45,37 @@ scenarios: content_integrity: "none" expected: decision: deny - error_code: -32001 + error_code: -32002 reason: "repository not in allowed list" - # --- Scenario C: prefix wildcard within owner --- + # --- Scenario C: wildcard-owner pattern matches exact repo under any owner --- - scenario_id: "wildcard-deny-C" - description: "Pattern 'github/gh-*' denies repository 'github/copilot' (no 'gh-' prefix)" + description: "Pattern '*/gh-aw' allows request for repository 'github/gh-aw'" input: tool_config: repos: - - "github/gh-*" + - "*/gh-aw" + min-integrity: "none" + request: + repository: "github/gh-aw" + content_integrity: "none" + expected: + decision: allow + error_code: null + reason: "" + + # --- Scenario D: wildcard-owner pattern denies non-matching repo name --- + - scenario_id: "wildcard-deny-D" + description: "Pattern '*/gh-aw' denies request for repository 'github/copilot'" + input: + tool_config: + repos: + - "*/gh-aw" min-integrity: "none" request: repository: "github/copilot" content_integrity: "none" expected: decision: deny - error_code: -32001 + error_code: -32002 reason: "repository not in allowed list"