Add executable VAL-P1–VAL-P15 coverage for security architecture validation

.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:

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.*

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)))
+}