[formal-spec] security-architecture-spec-summary.md — Formal model & test suite — 2026-07-03

[github-actions]

Summary

specs/security-architecture-spec-summary.md — gh-aw 7-layer security architecture with SG-01–SG-07, three conformance classes, 130+ requirements. Formalizes 10 TLA+/F*/Z3 predicates mapped to Go testify unit tests.

Specification

• File: specs/security-architecture-spec-summary.md
• Focus area: Multi-layer security architecture for GitHub Agentic Workflows
• Formal notation: TLA+ (invariants), F* (pre/post), Z3 (constraints)

Formal Model

Predicates (illustrative notation)

P1 (SG-01): (requires sanitize raw = s /\ expr_safe s) — InputNotDirectlyInterpolated

P2 (SG-02): \A j \in AgentJobs : j.permissions.write = {} — NoDirectAgentWrite

P3 (SG-03): \A r : r.domain \in AllowedDomains \/ EcosystemDomains — NetworkRestricted

P4 (SG-04): default_perms.write = {} /\ default_perms.contents = "read" — LeastPrivilege

P5 (SG-05): \A j \in AgentJobs : j.container \in {AWF, SRT} — AgentSandboxed

P6 (SG-07): security_check = Fail => (halted /\ writes = 0) — FailSecure

P7: conformant(Complete,s) => conformant(Standard,s) => conformant(Basic,s) — Monotonicity

P8: \A i : depends_on(chain[i+1], chain[i]) — JobOrder (chain: pre_activation..conclusion)

P9: compile(md) = Ok(lf) => schema_valid(lf) /\ perms_minimal(lf) — CompileValidates

P10: WriteTokens \cap env(AgentJobs) = {} /\ \cap env(SafeOut) /= {} — TokenIsolation

Behavioral Coverage Map

Predicate	Test Function	Description
P1 InputNotDirectlyInterpolated	TestFormal_P1_InputSanitizationRequired	Expressions rejected without sanitization
P2 NoDirectAgentWrite	TestFormal_P2_AgentHasNoWritePermissions	Agent job must have zero write scopes
P3 NetworkRestricted	TestFormal_P3_NetworkDomainAllowlist	Requests outside allowlist blocked
P4 LeastPrivilege	TestFormal_P4_DefaultPermissionsMinimal	Defaults grant only read, never write
P5 AgentSandboxed	TestFormal_P5_AgentMustRunInSandbox	Agent jobs require approved container
P6 FailSecure	TestFormal_P6_SecurityFailureHaltsExecution	Security failure stops execution pre-write
P7 Monotonicity	TestFormal_P7_ConformanceLevelMonotonicity	Complete >= Standard >= Basic
P8 JobOrder	TestFormal_P8_JobDependencyChainOrder	Canonical dependency order enforced
P9 CompileValidates	TestFormal_P9_CompilationValidatesBeforeEmit	Invalid input blocks lock-file emission
P10 TokenIsolation	TestFormal_P10_WriteTokenIsolatedToSafeOutput	Write tokens absent from agent job env

Generated Test Suite

📄 `pkg/workflow/security_architecture_formal_test.go`

// security_architecture_formal_test.go
// Source: specs/security-architecture-spec-summary.md — Predicates P1–P10
package workflow_test

import (
	"strings"
	"testing"
	"github.com/stretchr/testify/assert"
	"github.com/stretchr/testify/require"
)

// stub — replace with real implementation
type Perms struct{ Contents, Issues, PullRequests string }
type Job struct {
	Name, Kind, Container string
	Perms   Perms; EnvKeys []string; DependsOn []string
}
type CLevel int
const (CBasic CLevel = iota+1; CStandard; CComplete)

func sanitizeRaw(raw string) bool {
	for _, d := range []string{"${{","secrets."} {
		if strings.Contains(raw,d) { return false }
	}
	return true
}
func defaultPerms() Perms { return Perms{"read","none","none"} }
func conformReqs(l CLevel) []string {
	b := []string{"input-sanitization","output-isolation","permission-management","compilation-checks"}
	s := append(append([]string{},b...),"network-isolation","sandbox-isolation")
	f := append(append([]string{},s...),"threat-detection","runtime-enforcement")
	switch l { case CBasic: return b; case CStandard: return s; default: return f }
}

// P1 — InputNotDirectlyInterpolated (SG-01)
func TestFormal_P1_InputSanitizationRequired(t *testing.T) {
	for _, c := range []struct{raw string; safe bool}{
		{"hello world", true}, {"${{ github.event.issue.title }}", false},
		{"secrets.TOKEN here", false}, {"", true},
	} {
		assert.Equal(t, c.safe, sanitizeRaw(c.raw), "P1 (SG-01): sanitizeRaw(%q)", c.raw)
	}
}

// P2 — NoDirectAgentWrite (SG-02)
func TestFormal_P2_AgentHasNoWritePermissions(t *testing.T) {
	j := Job{Kind:"agent", Perms:Perms{"read","none","none"}}
	for _,s := range []string{j.Perms.Contents,j.Perms.Issues,j.Perms.PullRequests} {
		assert.NotEqual(t,"write",s,"P2 (SG-02): agent must not have write scope, got %q",s)
	}
}

// P3 — NetworkRestricted (SG-03)
func TestFormal_P3_NetworkDomainAllowlist(t *testing.T) {
	allowed := map[string]bool{"api.github.com":true,"registry.npmjs.org":true}
	for _, tc := range []struct{d string; ok bool}{
		{"api.github.com",true},{"registry.npmjs.org",true},
		{"evil.attacker.io",false},{"169.254.169.254",false},
	} {
		assert.Equal(t,tc.ok,allowed[tc.d],"P3 (SG-03): domain %q",tc.d)
	}
}

// P4 — LeastPrivilege (SG-04)
func TestFormal_P4_DefaultPermissionsMinimal(t *testing.T) {
	p := defaultPerms()
	assert.Equal(t,"read",p.Contents,"P4: contents must default to read")
	assert.Equal(t,"none",p.Issues,"P4 (SG-04): issues must default to none")
	assert.Equal(t,"none",p.PullRequests,"P4 (SG-04): pull-requests must default to none")
}

// P5 — AgentSandboxed (SG-05)
func TestFormal_P5_AgentMustRunInSandbox(t *testing.T) {
	valid := map[string]bool{"awf-sandbox":true,"srt":true}
	j := Job{Kind:"agent", Container:"awf-sandbox"}
	require.NotEmpty(t,j.Container,"P5 (SG-05): agent must declare a container")
	assert.True(t,valid[j.Container],"P5 (SG-05): container %q not approved",j.Container)
}
func TestFormal_P5_BareAgentIsInvalid(t *testing.T) {
	j := Job{Kind:"agent", Container:""}
	assert.False(t,j.Container!="","P5 edge: bare-metal agent must be rejected by compiler")
}

// P6 — FailSecure (SG-07)
func TestFormal_P6_SecurityFailureHaltsExecution(t *testing.T) {
	exec := func(ok bool) (bool,bool) { if !ok {return true,false}; return false,true }
	h,w := exec(true);  assert.False(t,h,"P6: clean run not halted"); assert.True(t,w,"P6: proceeds")
	h,w  = exec(false); assert.True(t,h,"P6 (SG-07): failure must halt"); assert.False(t,w,"P6: no write")
}

// P7 — Monotonicity
func TestFormal_P7_ConformanceLevelMonotonicity(t *testing.T) {
	toSet := func(r []string) map[string]bool {
		s:=map[string]bool{}; for _,v:=range r{s[v]=true}; return s
	}
	b,s,f := toSet(conformReqs(CBasic)),toSet(conformReqs(CStandard)),toSet(conformReqs(CComplete))
	for r := range b { assert.True(t,s[r],"P7: Standard must include Basic req %q",r) }
	for r := range s { assert.True(t,f[r],"P7: Complete must include Standard req %q",r) }
	assert.Greater(t,len(f),len(s),"P7: Complete > Standard")
	assert.Greater(t,len(s),len(b),"P7: Standard > Basic")
}

// P8 — JobOrder
func TestFormal_P8_JobDependencyChainOrder(t *testing.T) {
	chain := []string{"pre_activation","activation","agent","detection","safe_outputs","conclusion"}
	jobs  := []Job{
		{Name:"pre_activation"},{Name:"activation",DependsOn:[]string{"pre_activation"}},
		{Name:"agent",DependsOn:[]string{"activation"}},{Name:"detection",DependsOn:[]string{"agent"}},
		{Name:"safe_outputs",DependsOn:[]string{"detection"}},{Name:"conclusion",DependsOn:[]string{"safe_outputs"}},
	}
	idx := map[string]*Job{}; for i := range jobs { idx[jobs[i].Name]=&jobs[i] }
	for i := 1; i < len(chain); i++ {
		j,ok := idx[chain[i]]; require.True(t,ok,"P8: job %q missing",chain[i])
		found := false
		for _,d := range j.DependsOn { if d==chain[i-1]{found=true;break} }
		assert.True(t,found,"P8: %q must depend on %q",chain[i],chain[i-1])
	}
}

// P9 — CompileValidates
func TestFormal_P9_CompilationValidatesBeforeEmit(t *testing.T) {
	compile := func(schema,expr,perms bool) bool { return schema && expr && perms }
	assert.True(t, compile(true,true,true),  "P9: valid input must emit")
	assert.False(t,compile(false,true,true), "P9: bad schema must block emit")
	assert.False(t,compile(true,false,true), "P9: unsafe expr must block emit")
	assert.False(t,compile(true,true,false), "P9: perm escalation must block emit")
}

// P10 — TokenIsolation
func TestFormal_P10_WriteTokenIsolatedToSafeOutput(t *testing.T) {
	wt := map[string]bool{"GITHUB_TOKEN":true}
	agent   := Job{Kind:"agent",       EnvKeys:[]string{"GITHUB_REPOSITORY","RUNNER_TEMP"}}
	safeOut := Job{Kind:"safe_output", EnvKeys:[]string{"GITHUB_TOKEN","GITHUB_REPOSITORY"}}
	for _,k := range agent.EnvKeys   { assert.False(t,wt[k],"P10: agent must not expose %q",k) }
	found := false
	for _,k := range safeOut.EnvKeys { if wt[k]{found=true;break} }
	assert.True(t,found,"P10: safe_output must have a write token")
}
func TestFormal_P10_WriteTokenLeakIsViolation(t *testing.T) {
	wt := map[string]bool{"GITHUB_TOKEN":true}
	leaky := Job{Kind:"agent", EnvKeys:[]string{"GITHUB_REPOSITORY","GITHUB_TOKEN"}}
	for _,k := range leaky.EnvKeys {
		if wt[k] { assert.Fail(t,"P10 edge: agent exposes write token %q — must be rejected",k) }
	}
}

Usage

1. Copy to pkg/workflow/security_architecture_formal_test.go.
2. Replace // stub types with real implementations from pkg/workflow/.
3. Run: go test ./pkg/workflow/... -run TestFormal

Context

• Spec: specs/security-architecture-spec-summary.md
• Notation: TLA+, F*, Z3 · Predicates: 10 · Tests: 12
• Run: https://github.com/github/gh-aw/actions/runs/28671381973

Generated by 🔬 Daily Formal Spec Verifier · 329.6 AIC · ⌖ 22.1 AIC · ⊞ 7.1K · ◷

• expires on Jul 10, 2026, 8:29 AM UTC-08:00