diff --git a/.github/workflows/agentic-auto-upgrade.yml b/.github/workflows/agentic-auto-upgrade.yml index 7035101ee35..e169cea32b6 100644 --- a/.github/workflows/agentic-auto-upgrade.yml +++ b/.github/workflows/agentic-auto-upgrade.yml @@ -34,7 +34,7 @@ name: Agentic Auto-Upgrade on: schedule: - - cron: "21 3 * * 5" # Weekly (auto-upgrade) + - cron: "11 4 * * 6" # Weekly (auto-upgrade) workflow_dispatch: permissions: diff --git a/docs/adr/46457-formal-spec-as-code-security-architecture-validation.md b/docs/adr/46457-formal-spec-as-code-security-architecture-validation.md new file mode 100644 index 00000000000..9567903d6a2 --- /dev/null +++ b/docs/adr/46457-formal-spec-as-code-security-architecture-validation.md @@ -0,0 +1,47 @@ +# ADR-46457: Adopt Spec-as-Code for Security Architecture Validation + +**Date**: 2026-07-18 +**Status**: Draft +**Deciders**: Unknown + +--- + +### Context + +`specs/security-architecture-spec-validation.md` existed as a static cross-reference document auditing the 7-layer security architecture against compiled `.lock.yml` workflow files and JavaScript implementation. The document verified 15 normative predicates (job topology, input sanitization, permission isolation, threat-detection ordering, action pinning, timestamp validation, concurrency constraints), but those predicates were prose-only. Without automated verification, the spec could silently drift from the actual compiler and validator behaviour as the codebase evolved, creating a gap where the spec claimed conformance that was no longer true. + +The project already has an established pattern of formal Go tests in `pkg/workflow` that drive the compiler and validator directly, so the infrastructure for this approach was already available. + +### Decision + +We will replace the static prose validation with 15 predicate-mapped Go tests (`TestFormalVAL_P1` through `TestFormalVAL_P15`) in `pkg/workflow/security_architecture_validation_formal_test.go`. Each test directly calls the production compiler or validator, compares compiled YAML output against expected security invariants, and is tagged `//go:build !integration` so it runs in the default unit-test suite. The formal model notation (TLA+, F*, Z3) is preserved in `specs/security-architecture-spec-validation.md` as the specification layer, while the Go tests serve as its executable binding. + +### Alternatives Considered + +#### Alternative 1: Keep Static Cross-References + +Maintain the existing prose document with periodic manual re-validation. This is the lowest-friction approach, requires no new code, and keeps the spec human-readable without any coupling to internal compiler APIs. However, manual re-validation is error-prone and easy to skip; any refactor that changes compiler output or validator behaviour could silently invalidate the spec with no automated signal. Given the security-critical nature of the invariants (permission isolation, fork protection, threat-detection ordering), undetected drift is unacceptable. + +#### Alternative 2: Run External Formal Verification Tools in CI (TLA+ / Z3 / F*) + +Model-check the TLA+ and Z3 invariants directly using the TLA+ Toolbox or the Z3 solver as CI steps, and type-check the F* contracts. This provides stronger formal guarantees than Go tests (exhaustive model checking vs. example-based testing). However, it requires specialist tooling not currently present in the repository, introduces significant CI infrastructure complexity, and cannot exercise the actual Go compiler and validator code paths — so a bug in the compiler would still go undetected. The spec-as-code approach exercises real production paths and is immediately executable with the existing `go test` infrastructure. + +### Consequences + +#### Positive +- All 15 security predicates are verified on every CI run; spec drift is caught automatically before it reaches production. +- Tests call production compiler and validator code directly, so they detect behavioural regressions in the actual enforcement logic, not just in a separate model. +- The formal model notation is preserved in the spec document, giving both human-readable specification and machine-verifiable bindings in one place. + +#### Negative +- The tests are tightly coupled to internal APIs (`compileFormalVALWorkflow`, `extractJobSection`, `sanitizeRunStepExpressions`, `validateConcurrencyQueueConfiguration`); any refactor of those functions requires updating the test suite. +- The `Generated Test Suite` section of the spec document contains an absolute filesystem path (`/home/runner/work/gh-aw/gh-aw/...`) that is environment-specific and will be incorrect outside the CI sandbox. +- Adding 15 additional tests increases unit-test suite runtime, though the impact is small since each test compiles a minimal synthetic workflow. + +#### Neutral +- The formal notation sections (TLA+, F*, Z3/SMT-LIB) in the spec remain illustrative rather than directly executed; they serve as design documentation alongside the Go tests. +- The PR also adjusts the cron schedule for `agentic-auto-upgrade.yml` as an unrelated change bundled in the same commit. + +--- + +*ADR created by [adr-writer agent]. Review and finalize before changing status from Draft to Accepted.* diff --git a/pkg/workflow/security_architecture_validation_formal_test.go b/pkg/workflow/security_architecture_validation_formal_test.go new file mode 100644 index 00000000000..4a03c9251d9 --- /dev/null +++ b/pkg/workflow/security_architecture_validation_formal_test.go @@ -0,0 +1,246 @@ +//go:build !integration + +package workflow + +import ( + "os" + "path/filepath" + "regexp" + "strings" + "testing" + + "github.com/github/gh-aw/pkg/constants" + "github.com/stretchr/testify/assert" + "github.com/stretchr/testify/require" +) + +const formalVALWorkflowFrontmatter = `--- +name: formal-validation-suite +on: + pull_request: + types: [opened] + roles: + - write +engine: copilot +permissions: + contents: read +safe-outputs: + create-issue: +concurrency: + group: "formal-${{ github.event.pull_request.number }}" + cancel-in-progress: true +---` + +var ( + formalVALWritePermissionLine = regexp.MustCompile(`(?m)^\s+[a-z0-9-]+:\s*write\s*$`) + formalVALUsesLine = regexp.MustCompile(`(?m)^\s*uses:\s*(\S+)`) + formalVALSHARef = regexp.MustCompile(`^[0-9a-f]{40}$`) + formalVALConcurrencyGroup = regexp.MustCompile(`(?m)^\s*group:\s*(.+)$`) +) + +func compileFormalVALWorkflow(t *testing.T) string { + t.Helper() + return compileFormalVALWorkflowFromFrontmatter(t, formalVALWorkflowFrontmatter) +} + +func compileFormalVALStrictWorkflow(t *testing.T) string { + t.Helper() + frontmatter := strings.Replace(formalVALWorkflowFrontmatter, "engine: copilot", "engine: copilot\nstrict: true", 1) + return compileFormalVALWorkflowFromFrontmatter(t, frontmatter) +} + +func compileFormalVALWorkflowFromFrontmatter(t *testing.T, frontmatter string) string { + t.Helper() + + md := frontmatter + ` + +# Mission + +Formal validation workflow. +` + + tmpDir := t.TempDir() + mdPath := filepath.Join(tmpDir, "workflow.md") + require.NoError(t, os.WriteFile(mdPath, []byte(md), 0600)) + + compiler := NewCompiler(WithNoEmit(true)) + wd, err := compiler.ParseWorkflowFile(mdPath) + require.NoError(t, err) + + yamlOut, err := compiler.CompileToYAML(wd, mdPath) + require.NoError(t, err) + require.NotEmpty(t, yamlOut) + + return yamlOut +} + +func assertFormalVALNoWritePermissions(t *testing.T, section string) { + t.Helper() + assert.False(t, formalVALWritePermissionLine.MatchString(section), "section must not contain write permissions:\n%s", section) +} + +func TestFormalVAL_P1_TripartiteJobArchitecture(t *testing.T) { + yamlOut := compileFormalVALWorkflow(t) + require.NotEmpty(t, extractJobSection(yamlOut, string(constants.ActivationJobName)), "OI-01: activation job must be present") + require.NotEmpty(t, extractJobSection(yamlOut, string(constants.AgentJobName)), "OI-01: agent job must be present") + require.NotEmpty(t, extractJobSection(yamlOut, string(constants.SafeOutputsJobName)), "OI-01: safe_outputs job must be present") +} + +func TestFormalVAL_P2_SanitizationPipelineOrder(t *testing.T) { + step := map[string]any{"run": `echo "${{ github.event.issue.title }}" && echo done`} + + sanitized, descriptions, changed := sanitizeRunStepExpressions(step) + require.True(t, changed, "IS-10: run expressions must be extracted into env before compilation continues") + require.NotEmpty(t, descriptions, "IS-10: extraction must emit a substitution description") + + runVal, ok := sanitized["run"].(string) + require.True(t, ok, "IS-10: sanitized run field must remain a string") + assert.NotContains(t, runVal, "${{", "IS-10: sanitized run field must not retain raw expressions") + + envMap, ok := sanitized["env"].(map[string]any) + require.True(t, ok, "IS-10: sanitized step must include an env block") + assert.Equal(t, "${{ github.event.issue.title }}", envMap["GH_AW_GITHUB_EVENT_ISSUE_TITLE"]) +} + +func TestFormalVAL_P3_AgentJobHasOnlyReadPermissions(t *testing.T) { + agentSection := extractJobSection(compileFormalVALWorkflow(t), string(constants.AgentJobName)) + require.NotEmpty(t, agentSection, "PM-01/PM-02: compiled workflow must contain an agent job") + assert.Contains(t, agentSection, "permissions:") + assert.Contains(t, agentSection, "contents: read") + assertFormalVALNoWritePermissions(t, agentSection) +} + +func TestFormalVAL_P4_ForkProtectionRepoIDComparison(t *testing.T) { + yamlOut := compileFormalVALWorkflow(t) + activationSection := extractJobSection(yamlOut, string(constants.ActivationJobName)) + preActivationSection := extractJobSection(yamlOut, string(constants.PreActivationJobName)) + + assert.Contains(t, activationSection, "github.event.pull_request.head.repo.id == github.repository_id") + assert.Contains(t, preActivationSection, "github.event.pull_request.head.repo.id == github.repository_id") +} + +func TestFormalVAL_P5_PreActivationGatesActivation(t *testing.T) { + yamlOut := compileFormalVALWorkflow(t) + activationSection := extractJobSection(yamlOut, string(constants.ActivationJobName)) + preActivationSection := extractJobSection(yamlOut, string(constants.PreActivationJobName)) + + assert.Contains(t, activationSection, "needs: pre_activation") + assert.Contains(t, activationSection, "needs.pre_activation.outputs.activated == 'true'") + assert.Contains(t, preActivationSection, "check_membership.cjs") + assert.Contains(t, preActivationSection, `GH_AW_REQUIRED_ROLES: "write"`) +} + +func TestFormalVAL_P6_DetectionJobBetweenAgentAndSafeOutputs(t *testing.T) { + yamlOut := compileFormalVALWorkflow(t) + agentIndex := indexInNonCommentLines(yamlOut, " agent:") + detectionIndex := indexInNonCommentLines(yamlOut, " detection:") + safeOutputsIndex := indexInNonCommentLines(yamlOut, " safe_outputs:") + + require.NotEqual(t, -1, agentIndex) + require.NotEqual(t, -1, detectionIndex) + require.NotEqual(t, -1, safeOutputsIndex) + assert.Less(t, agentIndex, detectionIndex, "TD-01: detection job must appear after agent") + assert.Less(t, detectionIndex, safeOutputsIndex, "TD-01: safe_outputs job must appear after detection") + assert.Contains(t, extractJobSection(yamlOut, string(constants.SafeOutputsJobName)), "- detection") +} + +func TestFormalVAL_P7_ActionPinsAre40CharSHA(t *testing.T) { + matches := formalVALUsesLine.FindAllStringSubmatch(compileFormalVALWorkflow(t), -1) + require.NotEmpty(t, matches, "CS-10: compiled workflow must contain uses steps") + + remoteUsesCount := 0 + for _, match := range matches { + ref := match[1] + if strings.HasPrefix(ref, "./") || strings.HasPrefix(ref, "docker://") { + continue + } + parts := strings.SplitN(ref, "@", 2) + require.Len(t, parts, 2, "CS-10: remote uses step must include @ref: %s", ref) + assert.True(t, formalVALSHARef.MatchString(parts[1]), "CS-10: remote uses step must be pinned to a 40-char SHA: %s", ref) + remoteUsesCount++ + } + + assert.Positive(t, remoteUsesCount, "CS-10: expected at least one remote uses step") +} + +func TestFormalVAL_P8_ActivationContainsTimestampCheck(t *testing.T) { + activationSection := extractJobSection(compileFormalVALWorkflow(t), string(constants.ActivationJobName)) + require.NotEmpty(t, activationSection) + assert.Contains(t, activationSection, "check_workflow_timestamp_api.cjs") +} + +func TestFormalVAL_P9_ConcurrencyGroupContainsDynamicExpr(t *testing.T) { + match := formalVALConcurrencyGroup.FindStringSubmatch(compileFormalVALWorkflow(t)) + require.Len(t, match, 2, "RS-16/RS-17: compiled workflow must contain a concurrency group") + assert.Contains(t, match[1], "${{", "RS-16/RS-17: concurrency.group must contain a dynamic expression") +} + +func TestFormalVAL_P10_WritePermissionsIsolatedToSafeOutputs(t *testing.T) { + yamlOut := compileFormalVALWorkflow(t) + activationSection := extractJobSection(yamlOut, string(constants.ActivationJobName)) + agentSection := extractJobSection(yamlOut, string(constants.AgentJobName)) + safeOutputsSection := extractJobSection(yamlOut, string(constants.SafeOutputsJobName)) + + assertFormalVALNoWritePermissions(t, activationSection) + assertFormalVALNoWritePermissions(t, agentSection) + assert.Contains(t, safeOutputsSection, "issues: write", "OI-07: safe_outputs must be the write-capable job") +} + +func TestFormalVAL_P11_QueueMaxConflictsWithCancelInProgress(t *testing.T) { + err := validateConcurrencyQueueConfiguration(`concurrency: + group: "formal-${{ github.ref }}" + queue: max + cancel-in-progress: true`) + require.Error(t, err, "RS-22: queue:max with cancel-in-progress:true must be rejected") + assert.Contains(t, err.Error(), "queue: max cannot be combined with cancel-in-progress: true") +} + +func TestFormalVAL_P12_RunStepExpressionsExtractedToEnv(t *testing.T) { + tests := []struct { + name string + step map[string]any + wantChanged bool + wantEnvKey string + }{ + {name: "empty run", step: map[string]any{"run": ""}, wantChanged: false}, + {name: "no expression", step: map[string]any{"run": "echo ${MY_VAR}"}, wantChanged: false}, + {name: "multiple expressions", step: map[string]any{"run": `echo "${{ github.event.issue.title }}" && echo "${{ github.event.issue.body }}"`}, wantChanged: true, wantEnvKey: "GH_AW_GITHUB_EVENT_ISSUE_TITLE"}, + } + + for _, tt := range tests { + t.Run(tt.name, func(t *testing.T) { + result, _, changed := sanitizeRunStepExpressions(tt.step) + assert.Equal(t, tt.wantChanged, changed) + if !tt.wantChanged { + assert.Equal(t, tt.step, result) + return + } + + envMap, ok := result["env"].(map[string]any) + require.True(t, ok) + assert.Contains(t, envMap, tt.wantEnvKey) + assert.NotContains(t, result["run"].(string), "${{") + }) + } +} + +func TestFormalVAL_P13_EmptyConcurrencyGroupRejected(t *testing.T) { + for _, group := range []string{"", " \n\t "} { + err := validateConcurrencyGroupExpression(group) + require.Error(t, err, "RS-17: empty concurrency groups must be rejected") + assert.Contains(t, err.Error(), "empty concurrency group expression") + } +} + +func TestFormalVAL_P14_MalformedConcurrencyExprRejected(t *testing.T) { + for _, group := range []string{"formal-${{ github.ref }", "formal-${{ (github.ref }}"} { + assert.Error(t, validateConcurrencyGroupExpression(group), "RS-17: malformed concurrency expressions must be rejected") + } +} + +func TestFormalVAL_P15_WritePermissionsRejectedInStrictMode(t *testing.T) { + yamlOut := compileFormalVALStrictWorkflow(t) + assert.Contains(t, yamlOut, "permissions: {}", "PM-01: strict-mode compiled workflows must default to top-level permissions:{}") + assertFormalVALNoWritePermissions(t, extractJobSection(yamlOut, string(constants.ActivationJobName))) + assertFormalVALNoWritePermissions(t, extractJobSection(yamlOut, string(constants.AgentJobName))) +} diff --git a/specs/security-architecture-spec-validation.md b/specs/security-architecture-spec-validation.md index bc51f9590cd..c14d4d0958a 100644 --- a/specs/security-architecture-spec-validation.md +++ b/specs/security-architecture-spec-validation.md @@ -1,7 +1,7 @@ # Security Architecture Specification Validation **Document**: Validation of `security-architecture-spec.md` against compiled `.lock.yml` files -**Date**: July 6, 2026 +**Date**: July 18, 2026 **Validator**: GitHub Copilot Agent **Scope**: Cross-reference specification requirements with actual implementation @@ -9,7 +9,7 @@ ## Executive Summary -✅ **VALIDATION RESULT**: The specification accurately reflects the implementation in compiled `.lock.yml` files and JavaScript implementation (revalidated on 2026-07-15). +✅ **VALIDATION RESULT**: The specification accurately reflects the implementation in compiled `.lock.yml` files and JavaScript implementation (revalidated on 2026-07-18). All major security architecture claims in the specification have been verified against actual workflow implementations: - ✅ Job architecture (activation, agent, safe_outputs) @@ -29,6 +29,117 @@ All major security architecture claims in the specification have been verified a --- +## Formal Model + +The validation pass is encoded as a compiled-workflow conformance model over job topology, sanitization rewrites, permission isolation, and concurrency guards. + +**State space** (`ValidationState`): + +```tla +ValidationState ≜ [ + compiledJobs : Seq(JobName), + jobSections : JobName → YAMLText, + runStep : Step, + permissions : PermissionScope → PermissionValue, + concurrencyYAML: YAMLText +] +``` + +**Representative invariants**: + +```tla +VAL_P1_TripartiteJobArchitecture ≜ + <<"activation", "agent", "safe_outputs">> ⊆ CompiledJobNames + +VAL_P2_InputSanitizationPipeline ≜ + ContainsExpression(runStep.run) ⟹ + (runStep.env ≠ nil ∧ ¬ContainsExpression(Sanitize(runStep).run)) + +VAL_P4_ForkProtectionRepoIDGuard ≜ + pull_request_trigger ⟹ + Contains(jobSections["activation"], "github.event.pull_request.head.repo.id == github.repository_id") + +VAL_P6_ThreatDetectionOrdering ≜ + IndexOf("agent", compiledJobs) < IndexOf("detection", compiledJobs) ∧ + IndexOf("detection", compiledJobs) < IndexOf("safe_outputs", compiledJobs) + +VAL_P10_PermissionWriteOnlySafeOutput ≜ + NoWrite(jobSections["activation"]) ∧ + NoWrite(jobSections["agent"]) ∧ + HasWrite(jobSections["safe_outputs"]) +``` + +**F* contracts** (selected): + +```fstar +val sanitizeRunStepExpressions : + step:map string any -> + Tot (map string any * list string * bool) + (requires True) + (ensures fun (sanitized, _, changed) -> + ContainsExpression(step["run"]) ==> (changed /\ Map.mem "env" sanitized)) + +val validateConcurrencyQueueConfiguration : + concurrencyYAML:string -> + Tot (option error) + (requires True) + (ensures fun err -> + Contains(concurrencyYAML, "queue: max") /\ Contains(concurrencyYAML, "cancel-in-progress: true") + ==> Some? err) +``` + +**Z3 / SMT-LIB constraints** (ordering and isolation): + +```smt2 +(declare-const agent Int) +(declare-const detection Int) +(declare-const safe_outputs Int) +(assert (< agent detection)) +(assert (< detection safe_outputs)) +(check-sat) ; sat +``` + +## Behavioral Coverage Map + +| Predicate / Invariant | Test Function | Description | +|---|---|---| +| `VAL-P1 JobArchitectureTripartite` | `TestFormalVAL_P1_TripartiteJobArchitecture` | activation, agent, safe_outputs jobs all present (OI-01) | +| `VAL-P2 InputSanitizationPipeline` | `TestFormalVAL_P2_SanitizationPipelineOrder` | `${{ }}` expressions moved to env: before other transforms (IS-10) | +| `VAL-P3 PermissionDefaultReadOnly` | `TestFormalVAL_P3_AgentJobHasOnlyReadPermissions` | agent job permissions are read-only, never write (PM-01/PM-02) | +| `VAL-P4 ForkProtectionRepoIDGuard` | `TestFormalVAL_P4_ForkProtectionRepoIDComparison` | PR workflows contain `head.repo.id == repository_id` guard (PM-08) | +| `VAL-P5 RBACPreActivationGates` | `TestFormalVAL_P5_PreActivationGatesActivation` | `pre_activation` gates activation via membership check (PM-10/PM-11) | +| `VAL-P6 ThreatDetectionOrdering` | `TestFormalVAL_P6_DetectionJobBetweenAgentAndSafeOutputs` | detection sits between agent and safe_outputs (TD-01) | +| `VAL-P7 ActionPinningSHA40` | `TestFormalVAL_P7_ActionPinsAre40CharSHA` | all non-local `uses:` are pinned to 40-char SHAs (CS-10) | +| `VAL-P8 TimestampValidationStep` | `TestFormalVAL_P8_ActivationContainsTimestampCheck` | activation references `check_workflow_timestamp_api.cjs` (RS-01/RS-02) | +| `VAL-P9 ConcurrencyDynamicGroup` | `TestFormalVAL_P9_ConcurrencyGroupContainsDynamicExpr` | `concurrency.group` contains a dynamic `${{ }}` expression (RS-16/RS-17) | +| `VAL-P10 PermissionWriteOnlySafeOutput` | `TestFormalVAL_P10_WritePermissionsIsolatedToSafeOutputs` | activation/agent have no write permissions while safe_outputs does (OI-07) | +| `VAL-P11 ConcurrencyQueueConflict` | `TestFormalVAL_P11_QueueMaxConflictsWithCancelInProgress` | `queue:max` + `cancel-in-progress:true` rejected (RS-22) | +| `VAL-P12 SanitizationRunStepExpr` | `TestFormalVAL_P12_RunStepExpressionsExtractedToEnv` | table-driven empty/no-expr/multi-expr run-step cases (IS-04) | +| `VAL-P13 EmptyGroupExpressionRejected` | `TestFormalVAL_P13_EmptyConcurrencyGroupRejected` | empty or whitespace concurrency group rejected (RS-17) | +| `VAL-P14 MalformedGroupExprRejected` | `TestFormalVAL_P14_MalformedConcurrencyExprRejected` | malformed `${{ }}` concurrency expressions rejected (RS-17) | +| `VAL-P15 WritePolicyRejectedInStrict` | `TestFormalVAL_P15_WritePermissionsRejectedInStrictMode` | strict-mode compiled activation/agent jobs retain no write perms (PM-01) | + +## Generated Test Suite + +The 15 predicate-mapped tests above are implemented in: + +- `/home/runner/work/gh-aw/gh-aw/pkg/workflow/security_architecture_validation_formal_test.go` + +They follow the repository’s existing formal-test conventions: + +- `//go:build !integration` so they run in the default unit-test suite +- direct calls into production compiler and validator code (no mocks) +- representative compiled-YAML assertions for topology, permission, and pinning requirements +- direct validator assertions for concurrency-expression and queue-compatibility edge cases + +Run the validation suite directly: + +```sh +go test ./pkg/workflow -run 'TestFormalVAL_' -v +``` + +--- + ## Detailed Validation ### 1. Job Architecture (Section 5.2 - OI-01)