From 1382443898fd3204499d30624c947fed59ce6621 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 3 Jul 2026 16:29:28 +0000 Subject: [PATCH 1/6] Initial plan From 0663aa6cbcd466cc46106e75d6d7d10e1f72572b Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 3 Jul 2026 16:42:33 +0000 Subject: [PATCH 2/6] =?UTF-8?q?feat:=20add=20security=20architecture=20for?= =?UTF-8?q?mal=20test=20suite=20(P1=E2=80=93P10)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com> --- .../security_architecture_formal_test.go | 347 ++++++++++++++++++ 1 file changed, 347 insertions(+) create mode 100644 pkg/workflow/security_architecture_formal_test.go diff --git a/pkg/workflow/security_architecture_formal_test.go b/pkg/workflow/security_architecture_formal_test.go new file mode 100644 index 00000000000..3779b96a404 --- /dev/null +++ b/pkg/workflow/security_architecture_formal_test.go @@ -0,0 +1,347 @@ +//go:build !integration + +// Package workflow – security architecture formal model tests. +// +// This file encodes the formal specification predicates (P1–P10) for the +// gh-aw 7-layer security architecture defined in +// specs/security-architecture-spec-summary.md. +// +// Each predicate is mapped to a Go test function: +// +// P1 InputNotDirectlyInterpolated → TestFormal_P1_InputSanitizationRequired +// P2 NoDirectAgentWrite → TestFormal_P2_AgentHasNoWritePermissions +// P3 NetworkRestricted → TestFormal_P3_NetworkDomainAllowlist +// P4 LeastPrivilege → TestFormal_P4_DefaultPermissionsMinimal +// P5 AgentSandboxed → TestFormal_P5_AgentMustRunInSandbox +// P6 FailSecure → TestFormal_P6_SecurityFailureHaltsExecution +// P7 Monotonicity → TestFormal_P7_ConformanceLevelMonotonicity +// P8 JobOrder → TestFormal_P8_JobDependencyChainOrder +// P9 CompileValidates → TestFormal_P9_CompilationValidatesBeforeEmit +// P10 TokenIsolation → TestFormal_P10_WriteTokenIsolatedToSafeOutput +// +// Tests exercise production Go code directly; no stubs are used. +package workflow + +import ( + "testing" + + "github.com/github/gh-aw/pkg/constants" + "github.com/stretchr/testify/assert" + "github.com/stretchr/testify/require" +) + +// secArchConformanceLevel is a typed integer representing a spec conformance class. +// Basic=1, Standard=2, Complete=3 (spec Section 2). +type secArchConformanceLevel int + +const ( + secArchConformanceBasic secArchConformanceLevel = 1 + secArchConformanceStandard secArchConformanceLevel = 2 + secArchConformanceComplete secArchConformanceLevel = 3 +) + +// formalConformanceMonotonicity checks the spec invariant: +// Complete >= Standard >= Basic. +func formalConformanceMonotonicity(basic, standard, complete secArchConformanceLevel) bool { + return complete >= standard && standard >= basic +} + +// formalJobOrderValid checks that every pair of consecutive canonical job names +// appears in the correct order within the supplied slice. +// It only enforces ordering for names that are both present in the slice. +func formalJobOrderValid(order []string) bool { + canonical := []string{ + string(constants.PreActivationJobName), + string(constants.ActivationJobName), + string(constants.AgentJobName), + string(constants.DetectionJobName), + string(constants.SafeOutputsJobName), + string(constants.ConclusionJobName), + } + idx := make(map[string]int, len(order)) + for i, name := range order { + idx[name] = i + } + for i := 1; i < len(canonical); i++ { + a, okA := idx[canonical[i-1]] + b, okB := idx[canonical[i]] + if okA && okB && a >= b { + return false + } + } + return true +} + +// formalTokenAbsentFromEnv reports whether tokenKey is absent from the env map, +// implementing the isolation invariant: write tokens must not appear in the agent +// job's environment. +func formalTokenAbsentFromEnv(env map[string]string, tokenKey string) bool { + _, present := env[tokenKey] + return !present +} + +// formalValidationBlocksEmit encodes the fail-secure predicate: a non-nil +// validation error must prevent lock-file emission. +func formalValidationBlocksEmit(validateErr error) bool { + return validateErr != nil +} + +// TestFormal_P1_InputSanitizationRequired (P1 InputNotDirectlyInterpolated) +// +// SG-01: Untrusted input must not be directly interpolated into GitHub Actions +// expressions without sanitization. sanitizeRunStepExpressions must extract +// every ${{ … }} occurrence from a run: field into the step's env: block. +func TestFormal_P1_InputSanitizationRequired(t *testing.T) { + // A run: step that contains a GitHub Actions expression must be rewritten. + unsafeStep := map[string]any{ + "run": "echo ${{ github.event.issue.title }}", + } + sanitized, descriptions, changed := sanitizeRunStepExpressions(unsafeStep) + assert.True(t, changed, "expression in run: must be extracted to env: to prevent template injection") + assert.NotEmpty(t, descriptions, "at least one substitution description must be emitted") + + // The sanitized step must no longer contain the raw expression in its run: field. + if runVal, ok := sanitized["run"].(string); ok { + assert.NotContains(t, runVal, "${{", "sanitized run: field must not contain raw ${{ }} expression") + } + + // A run: step without any expression must not be modified. + cleanStep := map[string]any{ + "run": "echo hello", + } + _, _, cleanChanged := sanitizeRunStepExpressions(cleanStep) + assert.False(t, cleanChanged, "run: step without expressions must not be modified") +} + +// TestFormal_P2_AgentHasNoWritePermissions (P2 NoDirectAgentWrite) +// +// SG-02: AI agents must have no direct write access. validateDangerousPermissions +// must reject every write-capable scope on the agent job. +func TestFormal_P2_AgentHasNoWritePermissions(t *testing.T) { + for _, scope := range GetAllPermissionScopes() { + // id-token is used for OIDC authentication and does not grant repo write access. + // metadata is implicitly read-only and excluded from the rejection rule. + if scope == PermissionIdToken || scope == PermissionMetadata { + continue + } + t.Run(string(scope), func(t *testing.T) { + perms := NewPermissions() + perms.Set(scope, PermissionWrite) + err := validateDangerousPermissions(&WorkflowData{Permissions: "permissions: {}"}, perms) + require.Error(t, err, "agent job scope %s:write must be rejected", scope) + assert.Contains(t, err.Error(), "write permissions") + }) + } +} + +// TestFormal_P3_NetworkDomainAllowlist (P3 NetworkRestricted) +// +// SG-03: Network access must be restricted to explicitly allowed domains. +// validateNetworkAllowedDomains must accept valid domain lists, and +// validateStrictNetwork must reject wildcard-only allowlists. +func TestFormal_P3_NetworkDomainAllowlist(t *testing.T) { + compiler := NewCompiler() + + // An explicit allowlist of valid domains must be accepted. + validNet := &NetworkPermissions{Allowed: []string{"github.com", "api.github.com"}} + require.NoError(t, compiler.validateNetworkAllowedDomains(validNet), + "explicit allowlist of valid domains must be accepted") + + // A wildcard-only allowlist must be rejected in strict mode (CTR-011). + err := compiler.validateStrictNetwork(&NetworkPermissions{Allowed: []string{"*"}}) + require.Error(t, err, "wildcard-only allowlist must be rejected in strict mode") + assert.Contains(t, err.Error(), "wildcard") + + // An empty network permission set must not cause a validation error. + require.NoError(t, compiler.validateNetworkAllowedDomains(nil), + "nil network permissions must not fail allowlist validation") +} + +// TestFormal_P4_DefaultPermissionsMinimal (P4 LeastPrivilege) +// +// SG-04: Permissions must follow the principle of least privilege. A freshly +// created Permissions object must grant no write access, and an all-read set +// must also be accepted. +func TestFormal_P4_DefaultPermissionsMinimal(t *testing.T) { + // Default (empty) permissions must contain no write grants. + perms := NewPermissions() + err := validateDangerousPermissions(&WorkflowData{Permissions: "permissions: {}"}, perms) + require.NoError(t, err, "default (empty) permissions must contain no write grants") + + // All-read permissions must also pass validation. + readAllPerms := NewPermissions() + for _, scope := range GetAllPermissionScopes() { + // id-token is treated as write-or-absent by GitHub Actions, so skip it here. + if scope == PermissionIdToken { + continue + } + readAllPerms.Set(scope, PermissionRead) + } + err = validateDangerousPermissions(&WorkflowData{Permissions: "permissions: {}"}, readAllPerms) + require.NoError(t, err, "read-only permissions must be accepted for the agent job") +} + +// TestFormal_P5_AgentMustRunInSandbox (P5 AgentSandboxed) +// +// SG-05: Agent processes must execute in isolated sandbox environments. +// isSandboxEnabled must return true for approved sandbox configurations and +// false when the sandbox is explicitly disabled. +func TestFormal_P5_AgentMustRunInSandbox(t *testing.T) { + // An explicit AWF sandbox configuration must be enabled. + awfSandbox := &SandboxConfig{ + Agent: &AgentSandboxConfig{Type: SandboxTypeAWF}, + } + assert.True(t, isSandboxEnabled(awfSandbox, nil), + "AWF sandbox must be enabled when agent.type=awf") + + // An explicitly disabled sandbox must not be enabled. + disabledSandbox := &SandboxConfig{ + Agent: &AgentSandboxConfig{Disabled: true}, + } + assert.False(t, isSandboxEnabled(disabledSandbox, nil), + "sandbox must not be enabled when agent.disabled=true") + + // A firewall-enabled network configuration must auto-enable the AWF sandbox. + firewallNet := &NetworkPermissions{ + Firewall: &FirewallConfig{Enabled: true}, + } + assert.True(t, isSandboxEnabled(nil, firewallNet), + "AWF firewall must auto-enable the sandbox") + + // Nil sandbox and nil network must not be treated as enabled. + assert.False(t, isSandboxEnabled(nil, nil), + "no sandbox configuration must not be treated as sandbox-enabled") +} + +// TestFormal_P6_SecurityFailureHaltsExecution (P6 FailSecure) +// +// SG-07: Security violations must prevent workflow execution rather than +// allowing degraded operation. A validation error from a write-permission +// check must block lock-file emission. +func TestFormal_P6_SecurityFailureHaltsExecution(t *testing.T) { + perms := NewPermissions() + perms.Set(PermissionContents, PermissionWrite) + + err := validateDangerousPermissions(&WorkflowData{Permissions: "permissions: {}"}, perms) + require.Error(t, err, "security violation must return a non-nil error") + + // formalValidationBlocksEmit is the formal emit-gate predicate: + // true → validation failed → lock-file must NOT be emitted + // false → validation passed → lock-file may be emitted + assert.True(t, formalValidationBlocksEmit(err), + "a non-nil validation error must block lock-file emission") + assert.False(t, formalValidationBlocksEmit(nil), + "a nil validation error must allow lock-file emission") +} + +// TestFormal_P7_ConformanceLevelMonotonicity (P7 Monotonicity) +// +// Spec Section 2: conformance classes must satisfy Complete >= Standard >= Basic. +func TestFormal_P7_ConformanceLevelMonotonicity(t *testing.T) { + assert.True(t, + formalConformanceMonotonicity( + secArchConformanceBasic, + secArchConformanceStandard, + secArchConformanceComplete, + ), + "Complete >= Standard >= Basic must hold") + + // A reversed assignment must violate the invariant. + assert.False(t, + formalConformanceMonotonicity( + secArchConformanceComplete, + secArchConformanceStandard, + secArchConformanceBasic, + ), + "reversed level assignment must not satisfy the monotonicity invariant") + + // The level constants themselves must satisfy the ordering numerically. + assert.True(t, + int(secArchConformanceComplete) >= int(secArchConformanceStandard) && + int(secArchConformanceStandard) >= int(secArchConformanceBasic), + "conformance level constants must be positive integers satisfying the ordering") +} + +// TestFormal_P8_JobDependencyChainOrder (P8 JobOrder) +// +// Spec Appendix A: the canonical job dependency order must be +// pre_activation → activation → agent → detection → safe_outputs → conclusion. +func TestFormal_P8_JobDependencyChainOrder(t *testing.T) { + canonical := []string{ + string(constants.PreActivationJobName), + string(constants.ActivationJobName), + string(constants.AgentJobName), + string(constants.DetectionJobName), + string(constants.SafeOutputsJobName), + string(constants.ConclusionJobName), + } + + assert.True(t, formalJobOrderValid(canonical), + "canonical job dependency order must be valid") + + // Reversing the order must violate the invariant. + reversed := make([]string, len(canonical)) + for i, v := range canonical { + reversed[len(canonical)-1-i] = v + } + assert.False(t, formalJobOrderValid(reversed), + "reversed job order must be invalid") + + // Job name constants must match the specification values exactly. + assert.Equal(t, "pre_activation", string(constants.PreActivationJobName)) + assert.Equal(t, "activation", string(constants.ActivationJobName)) + assert.Equal(t, "agent", string(constants.AgentJobName)) + assert.Equal(t, "detection", string(constants.DetectionJobName)) + assert.Equal(t, "safe_outputs", string(constants.SafeOutputsJobName)) + assert.Equal(t, "conclusion", string(constants.ConclusionJobName)) +} + +// TestFormal_P9_CompilationValidatesBeforeEmit (P9 CompileValidates) +// +// Spec Section 10: compilation-time security checks must block lock-file +// emission when the input is invalid. +func TestFormal_P9_CompilationValidatesBeforeEmit(t *testing.T) { + // Dangerous permissions detected at compile time must block emit. + perms := NewPermissions() + perms.Set(PermissionIssues, PermissionWrite) + err := validateDangerousPermissions(&WorkflowData{Permissions: "permissions: {}"}, perms) + require.Error(t, err, "dangerous permissions must be rejected at compile time") + assert.True(t, formalValidationBlocksEmit(err), + "dangerous-permissions error must block lock-file emission") + + // A wildcard-only network allowlist must be rejected in strict mode at compile time. + compiler := NewCompiler() + compiler.SetStrictMode(true) + strictErr := compiler.validateStrictNetwork(&NetworkPermissions{Allowed: []string{"*"}}) + require.Error(t, strictErr, "wildcard-only network allowlist must be rejected at compile time") + assert.True(t, formalValidationBlocksEmit(strictErr), + "strict-network error must block lock-file emission") +} + +// TestFormal_P10_WriteTokenIsolatedToSafeOutput (P10 TokenIsolation) +// +// Spec Section 5: write tokens must be absent from the agent job's environment +// and present only in the safe_outputs job. +func TestFormal_P10_WriteTokenIsolatedToSafeOutput(t *testing.T) { + // The agent job must not receive private key material or a dedicated write token. + agentJobEnv := map[string]string{ + "GH_TOKEN": "${{ github.token }}", + "GH_AW_GITHUB_TOKEN": "${{ secrets.GH_AW_GITHUB_TOKEN || github.token }}", + } + assert.True(t, formalTokenAbsentFromEnv(agentJobEnv, "GH_AW_APP_PRIVATE_KEY"), + "agent job env must not contain private key material") + assert.True(t, formalTokenAbsentFromEnv(agentJobEnv, "GH_AW_WRITE_TOKEN"), + "agent job env must not contain a dedicated write token") + + // The safe_outputs job must hold the write-capable token (private key). + safeOutputsJobEnv := map[string]string{ + "GH_AW_APP_PRIVATE_KEY": "${{ secrets.GH_AW_APP_PRIVATE_KEY }}", + } + assert.False(t, formalTokenAbsentFromEnv(safeOutputsJobEnv, "GH_AW_APP_PRIVATE_KEY"), + "safe_outputs job must hold the write token (private key)") + + // formalTokenAbsentFromEnv must correctly identify presence and absence. + emptyEnv := map[string]string{} + assert.True(t, formalTokenAbsentFromEnv(emptyEnv, "ANY_TOKEN"), + "empty env must report all tokens as absent") +} From 7bb8bdf8d0c1f3be11295bfd62fc283d8cd839b7 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 3 Jul 2026 16:44:10 +0000 Subject: [PATCH 3/6] style: apply code review feedback on formal test naming Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com> --- .../security_architecture_formal_test.go | 30 +++++++++---------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/pkg/workflow/security_architecture_formal_test.go b/pkg/workflow/security_architecture_formal_test.go index 3779b96a404..ad9bd725887 100644 --- a/pkg/workflow/security_architecture_formal_test.go +++ b/pkg/workflow/security_architecture_formal_test.go @@ -1,6 +1,6 @@ //go:build !integration -// Package workflow – security architecture formal model tests. +// Package workflow - security architecture formal model tests. // // This file encodes the formal specification predicates (P1–P10) for the // gh-aw 7-layer security architecture defined in @@ -30,19 +30,19 @@ import ( "github.com/stretchr/testify/require" ) -// secArchConformanceLevel is a typed integer representing a spec conformance class. +// formalConformanceLevel is a typed integer representing a spec conformance class. // Basic=1, Standard=2, Complete=3 (spec Section 2). -type secArchConformanceLevel int +type formalConformanceLevel int const ( - secArchConformanceBasic secArchConformanceLevel = 1 - secArchConformanceStandard secArchConformanceLevel = 2 - secArchConformanceComplete secArchConformanceLevel = 3 + formalConformanceLevelBasic formalConformanceLevel = 1 + formalConformanceLevelStandard formalConformanceLevel = 2 + formalConformanceLevelComplete formalConformanceLevel = 3 ) // formalConformanceMonotonicity checks the spec invariant: // Complete >= Standard >= Basic. -func formalConformanceMonotonicity(basic, standard, complete secArchConformanceLevel) bool { +func formalConformanceMonotonicity(basic, standard, complete formalConformanceLevel) bool { return complete >= standard && standard >= basic } @@ -240,25 +240,25 @@ func TestFormal_P6_SecurityFailureHaltsExecution(t *testing.T) { func TestFormal_P7_ConformanceLevelMonotonicity(t *testing.T) { assert.True(t, formalConformanceMonotonicity( - secArchConformanceBasic, - secArchConformanceStandard, - secArchConformanceComplete, + formalConformanceLevelBasic, + formalConformanceLevelStandard, + formalConformanceLevelComplete, ), "Complete >= Standard >= Basic must hold") // A reversed assignment must violate the invariant. assert.False(t, formalConformanceMonotonicity( - secArchConformanceComplete, - secArchConformanceStandard, - secArchConformanceBasic, + formalConformanceLevelComplete, + formalConformanceLevelStandard, + formalConformanceLevelBasic, ), "reversed level assignment must not satisfy the monotonicity invariant") // The level constants themselves must satisfy the ordering numerically. assert.True(t, - int(secArchConformanceComplete) >= int(secArchConformanceStandard) && - int(secArchConformanceStandard) >= int(secArchConformanceBasic), + int(formalConformanceLevelComplete) >= int(formalConformanceLevelStandard) && + int(formalConformanceLevelStandard) >= int(formalConformanceLevelBasic), "conformance level constants must be positive integers satisfying the ordering") } From 933fd5cd4ef677a47d060a8b51a3544bb0d4c631 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Sat, 4 Jul 2026 03:20:59 +0000 Subject: [PATCH 4/6] docs(adr): add draft ADR-43244 for formal security specification testing Draft ADR generated by the Design Decision Gate for PR #43244, which adds 10 formal predicate tests encoding the gh-aw security architecture spec. --- ...ng-for-security-architecture-predicates.md | 48 +++++++++++++++++++ 1 file changed, 48 insertions(+) create mode 100644 docs/adr/43244-formal-specification-testing-for-security-architecture-predicates.md diff --git a/docs/adr/43244-formal-specification-testing-for-security-architecture-predicates.md b/docs/adr/43244-formal-specification-testing-for-security-architecture-predicates.md new file mode 100644 index 00000000000..63809657c24 --- /dev/null +++ b/docs/adr/43244-formal-specification-testing-for-security-architecture-predicates.md @@ -0,0 +1,48 @@ +# ADR-43244: Formal Specification Testing for Security Architecture Predicates + +**Date**: 2026-07-04 +**Status**: Draft +**Deciders**: Unknown + +--- + +### Context + +The gh-aw 7-layer security architecture is defined in `specs/security-architecture-spec-summary.md` as 10 formal predicates (P1–P10), covering invariants such as input sanitization, agent permission boundaries, network allowlists, sandbox enforcement, and token isolation. Without executable tests tied to those predicates, compliance is checked only at code-review time and can silently regress when production helpers are refactored. The codebase already contains a `*_formal_test.go` convention in `pkg/workflow/` for encoding spec-level invariants as Go tests. This decision extends that pattern to cover all 10 security-architecture predicates and introduces file-local formal helpers for predicates that do not map to a single production call site. + +### Decision + +We will add `pkg/workflow/security_architecture_formal_test.go` containing 10 `TestFormal_P*` functions—one per predicate—that call production code directly with no stubs, plus four file-local formal helpers (`formalConformanceMonotonicity`, `formalJobOrderValid`, `formalTokenAbsentFromEnv`, `formalValidationBlocksEmit`) for predicates whose invariants span multiple call sites. This makes the formal spec continuously verifiable in CI under the default (non-integration) build tag. + +### Alternatives Considered + +#### Alternative 1: Manual Code-Review Enforcement + +Each PR touching security-sensitive code would rely on reviewers to verify predicate compliance against the spec document. This is simple to introduce (no new files) and imposes no coupling to production function signatures. It was not chosen because review coverage is inconsistent, spec drift is invisible to CI, and regressions in production helpers are not caught until the next human review. + +#### Alternative 2: Integration-Level Security Tests + +Predicates could be verified at the system level (full workflow compilation + execution) rather than at the unit level. This would test the full call stack and avoid direct coupling to internal function signatures. It was not chosen because integration tests are slower and gated behind the `integration` build tag, which is not part of every CI run; unit-level tests provide faster feedback and run unconditionally. + +#### Alternative 3: Embedding Invariant Checks in Production Code (Assertions/Panics) + +Security invariants could be enforced at runtime in production code via `panic` or explicit assertion helpers, ensuring they are checked during normal execution. This was not chosen because it conflates validation logic with the production hot path, adds noise to error messages surfaced to users, and makes it harder to reason about which checks are spec-mandated versus operational. + +### Consequences + +#### Positive +- All 10 security predicates become continuously verifiable in CI without any special build flags, catching regressions automatically. +- The test file acts as a living, executable cross-reference between the formal spec and the production codebase—each predicate maps one-to-one to a named test. +- File-local formal helpers make spec-level invariants (e.g., monotonicity, emit-gate logic) explicit and independently readable, even when no single production function encapsulates them. + +#### Negative +- Tests are tightly coupled to specific internal function signatures (`sanitizeRunStepExpressions`, `validateDangerousPermissions`, `isSandboxEnabled`, etc.); renaming or restructuring these functions breaks tests regardless of behavioral equivalence, increasing refactor friction. +- File-local formal helpers (`formalConformanceMonotonicity`, etc.) duplicate or paraphrase spec logic outside the canonical spec document; they may drift from `specs/security-architecture-spec-summary.md` as the spec evolves if not updated in tandem. + +#### Neutral +- The `//go:build !integration` tag places these tests in the default unit-test suite, consistent with the existing `*_formal_test.go` pattern in the package. +- Each predicate is mapped to exactly one test function, creating a traceable spec-to-test matrix that can be audited against the spec appendix. + +--- + +*ADR created by [adr-writer agent]. Review and finalize before changing status from Draft to Accepted.* From 24be9ec4a814dfc878a7ba99a753a9287fe98e0a Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 4 Jul 2026 04:12:05 +0000 Subject: [PATCH 5/6] fix(formal-tests): use real compile path for P6, P9, P10; strengthen P1 Address reviewer feedback on security_architecture_formal_test.go: - P1: replace conditional type assertion with require.True so the test fails if sanitization breaks the step shape; add hasEnv assertion to confirm an env block was added to the sanitized step. - P6/P9: replace vacuous formalValidationBlocksEmit (err != nil) with real compile-path exercises using ParseWorkflowString + CompileToYAML, asserting the returned YAML is empty when a dangerous-permissions or strict-network violation is present. - P10: replace synthetic env-map checks against a non-existent token identifier with a real compile path (ParseWorkflowFile + CompileToYAML on a temp file), using formalJobSections to partition the produced YAML by job boundary, asserting APP_PRIVATE_KEY is absent from the agent job and present only in the safe_outputs mint step with: block. - Update file header comment to accurately describe the mixed approach. - Extract jobKeyIndent named constant in formalJobSections helper. Co-authored-by: gh-aw-bot <259018956+gh-aw-bot@users.noreply.github.com> --- .../security_architecture_formal_test.go | 259 +++++++++++++----- 1 file changed, 192 insertions(+), 67 deletions(-) diff --git a/pkg/workflow/security_architecture_formal_test.go b/pkg/workflow/security_architecture_formal_test.go index ad9bd725887..46b55f837d1 100644 --- a/pkg/workflow/security_architecture_formal_test.go +++ b/pkg/workflow/security_architecture_formal_test.go @@ -19,10 +19,16 @@ // P9 CompileValidates → TestFormal_P9_CompilationValidatesBeforeEmit // P10 TokenIsolation → TestFormal_P10_WriteTokenIsolatedToSafeOutput // -// Tests exercise production Go code directly; no stubs are used. +// Most predicates exercise production Go code directly via the public compiler +// API (ParseWorkflowString, ParseWorkflowFile, CompileToYAML) or internal +// validators. P7 and P8 encode spec invariants that have no single production +// call site; they use file-local formal helpers instead. package workflow import ( + "os" + "path/filepath" + "strings" "testing" "github.com/github/gh-aw/pkg/constants" @@ -72,18 +78,58 @@ func formalJobOrderValid(order []string) bool { return true } -// formalTokenAbsentFromEnv reports whether tokenKey is absent from the env map, -// implementing the isolation invariant: write tokens must not appear in the agent -// job's environment. -func formalTokenAbsentFromEnv(env map[string]string, tokenKey string) bool { - _, present := env[tokenKey] - return !present -} +// formalJobSections parses a compiled GitHub Actions YAML string and returns +// the content of the named jobs as separate strings. Jobs are YAML keys at +// the 2-space indent level inside the top-level `jobs:` block. +func formalJobSections(yamlContent string) map[string]string { + // jobKeyIndent is the number of leading spaces that identifies a top-level + // job key inside the `jobs:` block (e.g. " agent:"). + const jobKeyIndent = 2 + + lines := strings.Split(yamlContent, "\n") + type boundary struct{ start, end int } + + var order []string + bounds := map[string]boundary{} + inJobs := false + + for i, line := range lines { + if strings.TrimSpace(line) == "jobs:" { + inJobs = true + continue + } + if !inJobs { + continue + } + // A job key is indented by exactly jobKeyIndent spaces and contains no + // interior spaces before the trailing colon + // (e.g. " agent:" not " steps:"). + if len(line) > jobKeyIndent && line[0] == ' ' && line[1] == ' ' && line[jobKeyIndent] != ' ' { + trimmed := strings.TrimSpace(line) + if strings.HasSuffix(trimmed, ":") && !strings.Contains(strings.TrimSuffix(trimmed, ":"), " ") { + name := strings.TrimSuffix(trimmed, ":") + order = append(order, name) + bounds[name] = boundary{start: i} + } + } + } + + // Close each section at the line before the next job key (or EOF). + for i, name := range order { + b := bounds[name] + if i+1 < len(order) { + b.end = bounds[order[i+1]].start - 1 + } else { + b.end = len(lines) - 1 + } + bounds[name] = b + } -// formalValidationBlocksEmit encodes the fail-secure predicate: a non-nil -// validation error must prevent lock-file emission. -func formalValidationBlocksEmit(validateErr error) bool { - return validateErr != nil + result := make(map[string]string, len(order)) + for name, b := range bounds { + result[name] = strings.Join(lines[b.start:b.end+1], "\n") + } + return result } // TestFormal_P1_InputSanitizationRequired (P1 InputNotDirectlyInterpolated) @@ -100,10 +146,13 @@ func TestFormal_P1_InputSanitizationRequired(t *testing.T) { assert.True(t, changed, "expression in run: must be extracted to env: to prevent template injection") assert.NotEmpty(t, descriptions, "at least one substitution description must be emitted") - // The sanitized step must no longer contain the raw expression in its run: field. - if runVal, ok := sanitized["run"].(string); ok { - assert.NotContains(t, runVal, "${{", "sanitized run: field must not contain raw ${{ }} expression") - } + // The sanitized step must still have a string run: field (sanitization must not break + // the step shape) and must have extracted the expression into an env: block. + runVal, ok := sanitized["run"].(string) + require.True(t, ok, "sanitized run: field must remain a string after sanitization") + assert.NotContains(t, runVal, "${{", "sanitized run: field must not contain raw ${{ }} expression") + _, hasEnv := sanitized["env"] + assert.True(t, hasEnv, "sanitized step must carry an env: block containing the extracted expression") // A run: step without any expression must not be modified. cleanStep := map[string]any{ @@ -216,22 +265,33 @@ func TestFormal_P5_AgentMustRunInSandbox(t *testing.T) { // TestFormal_P6_SecurityFailureHaltsExecution (P6 FailSecure) // // SG-07: Security violations must prevent workflow execution rather than -// allowing degraded operation. A validation error from a write-permission -// check must block lock-file emission. +// allowing degraded operation. A write-permission violation detected during +// compilation must block lock-file emission — CompileToYAML returns ("", err). +// +// strict:false in the frontmatter bypasses strict-mode-only checks so that +// validateDangerousPermissions (the spec-mandated P6 guard) is the sole blocker. func TestFormal_P6_SecurityFailureHaltsExecution(t *testing.T) { - perms := NewPermissions() - perms.Set(PermissionContents, PermissionWrite) - - err := validateDangerousPermissions(&WorkflowData{Permissions: "permissions: {}"}, perms) - require.Error(t, err, "security violation must return a non-nil error") - - // formalValidationBlocksEmit is the formal emit-gate predicate: - // true → validation failed → lock-file must NOT be emitted - // false → validation passed → lock-file may be emitted - assert.True(t, formalValidationBlocksEmit(err), - "a non-nil validation error must block lock-file emission") - assert.False(t, formalValidationBlocksEmit(nil), - "a nil validation error must allow lock-file emission") + md := `--- +name: fail-secure-test +on: push +engine: copilot +strict: false +permissions: + contents: write +--- + +# Mission + +Simulate a write-permission violation to verify that emit is blocked. +` + compiler := NewCompiler(WithNoEmit(true)) + wd, err := compiler.ParseWorkflowString(md, "workflow.md") + require.NoError(t, err, "ParseWorkflowString must succeed before the compilation-time security check runs") + + yamlOut, err := compiler.CompileToYAML(wd, "workflow.md") + require.Error(t, err, "CompileToYAML must return an error when a write-permission violation is present (P6 FailSecure)") + assert.Empty(t, yamlOut, "CompileToYAML must return empty YAML — the lock-file must not be emitted — when a security violation is detected") + assert.Contains(t, err.Error(), "write permissions", "error must identify the permission violation") } // TestFormal_P7_ConformanceLevelMonotonicity (P7 Monotonicity) @@ -300,48 +360,113 @@ func TestFormal_P8_JobDependencyChainOrder(t *testing.T) { // // Spec Section 10: compilation-time security checks must block lock-file // emission when the input is invalid. +// +// Two distinct code paths are exercised: +// +// a. Dangerous permissions → CompileToYAML returns ("", err) via +// validateDangerousPermissions. strict:false ensures the check comes from +// the non-strict validator rather than the strict-mode guard. +// +// b. Wildcard-only network allowlist in strict mode → ParseWorkflowString +// itself returns an error via runStrictFrontmatterValidations, so no +// WorkflowData is produced and no YAML can be emitted. func TestFormal_P9_CompilationValidatesBeforeEmit(t *testing.T) { - // Dangerous permissions detected at compile time must block emit. - perms := NewPermissions() - perms.Set(PermissionIssues, PermissionWrite) - err := validateDangerousPermissions(&WorkflowData{Permissions: "permissions: {}"}, perms) - require.Error(t, err, "dangerous permissions must be rejected at compile time") - assert.True(t, formalValidationBlocksEmit(err), - "dangerous-permissions error must block lock-file emission") - - // A wildcard-only network allowlist must be rejected in strict mode at compile time. - compiler := NewCompiler() - compiler.SetStrictMode(true) - strictErr := compiler.validateStrictNetwork(&NetworkPermissions{Allowed: []string{"*"}}) - require.Error(t, strictErr, "wildcard-only network allowlist must be rejected at compile time") - assert.True(t, formalValidationBlocksEmit(strictErr), - "strict-network error must block lock-file emission") + // a. Dangerous permissions detected by CompileToYAML must block emit. + mdPerms := `--- +name: compile-validates-perms +on: push +engine: copilot +strict: false +permissions: + issues: write +--- + +# Mission + +Simulate dangerous permissions at compile time. +` + compiler := NewCompiler(WithNoEmit(true)) + wd, err := compiler.ParseWorkflowString(mdPerms, "workflow.md") + require.NoError(t, err, "ParseWorkflowString must succeed before the compilation-time check runs") + + yamlOut, err := compiler.CompileToYAML(wd, "workflow.md") + require.Error(t, err, "dangerous permissions must be rejected at compile time (P9)") + assert.Empty(t, yamlOut, "CompileToYAML must return empty YAML when dangerous permissions are detected — no lock-file may be emitted") + + // b. Wildcard-only network allowlist with default strict mode is rejected by + // ParseWorkflowString (runStrictFrontmatterValidations → validateStrictNetwork), + // so no WorkflowData is produced and CompileToYAML cannot be reached. + mdNet := `--- +name: compile-validates-network +on: push +engine: copilot +network: + allowed: ["*"] +--- + +# Mission + +Simulate a wildcard network violation. +` + compiler2 := NewCompiler(WithNoEmit(true)) + _, strictErr := compiler2.ParseWorkflowString(mdNet, "workflow.md") + require.Error(t, strictErr, "wildcard-only network allowlist must be rejected before any YAML is generated (P9)") + assert.Contains(t, strictErr.Error(), "wildcard", "error must identify the wildcard violation") } // TestFormal_P10_WriteTokenIsolatedToSafeOutput (P10 TokenIsolation) // // Spec Section 5: write tokens must be absent from the agent job's environment // and present only in the safe_outputs job. +// +// Compiles a real workflow with a safe-outputs github-app configuration and +// inspects the produced YAML to verify that the private key appears only in +// the safe_outputs mint step inputs (under with:) and not in the agent job. func TestFormal_P10_WriteTokenIsolatedToSafeOutput(t *testing.T) { - // The agent job must not receive private key material or a dedicated write token. - agentJobEnv := map[string]string{ - "GH_TOKEN": "${{ github.token }}", - "GH_AW_GITHUB_TOKEN": "${{ secrets.GH_AW_GITHUB_TOKEN || github.token }}", - } - assert.True(t, formalTokenAbsentFromEnv(agentJobEnv, "GH_AW_APP_PRIVATE_KEY"), - "agent job env must not contain private key material") - assert.True(t, formalTokenAbsentFromEnv(agentJobEnv, "GH_AW_WRITE_TOKEN"), - "agent job env must not contain a dedicated write token") - - // The safe_outputs job must hold the write-capable token (private key). - safeOutputsJobEnv := map[string]string{ - "GH_AW_APP_PRIVATE_KEY": "${{ secrets.GH_AW_APP_PRIVATE_KEY }}", - } - assert.False(t, formalTokenAbsentFromEnv(safeOutputsJobEnv, "GH_AW_APP_PRIVATE_KEY"), - "safe_outputs job must hold the write token (private key)") - - // formalTokenAbsentFromEnv must correctly identify presence and absence. - emptyEnv := map[string]string{} - assert.True(t, formalTokenAbsentFromEnv(emptyEnv, "ANY_TOKEN"), - "empty env must report all tokens as absent") + md := `--- +name: token-isolation-test +on: push +engine: copilot +permissions: + contents: read +safe-outputs: + create-issue: + github-app: + app-id: ${{ vars.APP_ID }} + private-key: ${{ secrets.APP_PRIVATE_KEY }} +--- + +# Mission + +Token isolation test: verify the private key is restricted to the safe_outputs job. +` + tmpDir := t.TempDir() + mdPath := filepath.Join(tmpDir, "workflow.md") + require.NoError(t, os.WriteFile(mdPath, []byte(md), 0600)) //nolint:gosec // 0600 avoids world-readable files with embedded secret reference patterns + + compiler := NewCompiler(WithNoEmit(true)) + wd, err := compiler.ParseWorkflowFile(mdPath) + require.NoError(t, err, "workflow with safe-outputs github-app must parse without error") + + yamlOut, err := compiler.CompileToYAML(wd, mdPath) + require.NoError(t, err, "workflow must compile successfully") + require.NotEmpty(t, yamlOut, "compiled YAML must not be empty") + + // Partition the compiled YAML into per-job sections so we can verify + // isolation at the job boundary. + sections := formalJobSections(yamlOut) + + agentSection, hasAgent := sections["agent"] + require.True(t, hasAgent, "compiled YAML must contain an agent job") + + safeOutputsSection, hasSafeOutputs := sections["safe_outputs"] + require.True(t, hasSafeOutputs, "compiled YAML must contain a safe_outputs job") + + // The agent job must not carry the private key material in any form. + assert.NotContains(t, agentSection, "APP_PRIVATE_KEY", + "agent job must not carry the private key material — token isolation requires it stays in safe_outputs") + + // The safe_outputs job must hold the private key in its mint step inputs (with: block). + assert.Contains(t, safeOutputsSection, "private-key: ${{ secrets.APP_PRIVATE_KEY }}", + "safe_outputs job must hold the private key in the mint step with: block") } From 1f2f9110e28b92de751bf588b274335bb3591530 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 4 Jul 2026 06:58:02 +0000 Subject: [PATCH 6/6] fix: filter real GH_TOKEN from command env when processEnvLookup says it is absent Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com> --- pkg/workflow/github_cli.go | 30 +++++++++++++++++++++++++++++- 1 file changed, 29 insertions(+), 1 deletion(-) diff --git a/pkg/workflow/github_cli.go b/pkg/workflow/github_cli.go index a67462d760a..face5461cef 100644 --- a/pkg/workflow/github_cli.go +++ b/pkg/workflow/github_cli.go @@ -62,7 +62,17 @@ func setupGHCommand(ctx context.Context, args ...string) *exec.Cmd { cmd.Env = append(os.Environ(), "GH_TOKEN="+githubToken) } if lookupProcessEnv("GH_HOST") == "" { - SetGHHostEnv(cmd, getDefaultGHHost()) + host := getDefaultGHHost() + if host != "" && host != "github.com" { + if cmd.Env == nil { + // Build the base env from os.Environ(), filtering out GH_TOKEN when + // the processEnvLookup says it is absent. This prevents the real + // runner GH_TOKEN from leaking into commands that should not have it + // (e.g., under test mocks or when only GH_HOST must be injected). + cmd.Env = filterTokenFromEnv(os.Environ(), ghToken) + } + cmd.Env = append(cmd.Env, "GH_HOST="+host) + } } return cmd @@ -228,6 +238,24 @@ func RunGHContextWithHost(ctx context.Context, spinnerMessage string, host strin return output, enrichGHError(err) } +// filterTokenFromEnv returns env unchanged when knownToken is non-empty (the token is +// legitimately present), or returns a copy of env with all "GH_TOKEN=…" entries removed +// when knownToken is empty. This prevents the real runner GH_TOKEN from leaking into a +// command's environment when the processEnvLookup indicates no token should be present +// (e.g., under test mocks that override the env lookup). +func filterTokenFromEnv(env []string, knownToken string) []string { + if knownToken != "" { + return env + } + filtered := make([]string, 0, len(env)) + for _, e := range env { + if !strings.HasPrefix(e, "GH_TOKEN=") { + filtered = append(filtered, e) + } + } + return filtered +} + // SetGHHostEnv sets the GH_HOST environment variable on the command for non-github.com hosts. // This is needed for GitHub Enterprise Server (GHES) and Proxima (data residency) instances // because commands like `gh repo view`, `gh pr create`, and `gh run view` do not accept a