feat: formal model + 15-test suite for security architecture SG invariants#44590
Conversation
- Add Formal Model section to specs/security-architecture-spec-summary.md with TLA+/F*/Z3 invariants for SG-01 through SG-07 and the job pipeline topology invariant - Add Behavioral Coverage Map table (15 predicate → test function mappings) - Add Generated Test Suite section referencing the new Go test file - Create pkg/workflow/security_architecture_sg_formal_test.go with 15 tests: TestFormalSG01_InputSanitizationInvariant TestFormalSG02_AgentJobHasNoWritePermissions TestFormalSG03_NetworkAllowlistEnforcement TestFormalSG04_LeastPrivilegeBasePermissions TestFormalSG05_SandboxIsolationPresence TestFormalSG06_ThreatDetectionAuditArtifact TestFormalSG07_FailSecureOnSecurityError TestFormalBasicConformance_AllFourControls TestFormalThreatDetection_EnabledByDefault TestFormalThreatDetection_ExplicitDisable TestFormalThreatDetection_ContinueOnErrorDefault TestFormalStaged_HandlerRequiresNoWritePerms TestFormalIDToken_OIDCVaultActionsRequireWriteScope TestFormalPushFallback_DefaultsToTrue TestFormalJobTopology_PipelineOrderEnforced - Add Spec Maintenance Tasks entry tracking this work - Regenerate affected lock file (.github/workflows/test-dispatcher.lock.yml) Closes #44589 Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>
…cation
Address code review: extract the repeated "permissions: {}" literal into a
shared package-level constant formalEmptyPermissionsYAML in the SG formal test
file, used by TestFormalSG02, TestFormalSG04, and TestFormalBasicConformance.
Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>
|
PR Triage - Run 29041860272. Category: test | Risk: Medium | Score: 45/100 | Action: defer. DRAFT. Formal model + 15-test suite for security architecture SG invariants (781+/4-, 2 files). Adds TLA+/Go tests for SG-01..SG-07. Draft — needs review of formal model correctness before merge.
|
🤖 PR Triage — Run §29061171191
Formal model + 15-test suite for security SG invariants. DRAFT. 2 files, 781 additions. Medium risk — formal model PRs need design consensus before merging.
|
There was a problem hiding this comment.
Pull request overview
This PR adds an executable “formalization” layer for the security architecture guarantees (SG-01 through SG-07) by documenting invariants in the spec summary and introducing a dedicated Go unit test suite that encodes those invariants as continuously-verified checks against production compiler/validation code.
Changes:
- Added a “Formal Model” section (TLA+/F*/Z3-style invariants), a behavioral coverage map, and a pointer to the generated Go test suite in the security architecture spec summary.
- Introduced
pkg/workflow/security_architecture_sg_formal_test.gowith 15 unit tests covering SG-01..SG-07 and supporting invariants (threat-detection defaults, staged handler permissions, OIDC id-token detection, push fallback defaults, and job topology ordering).
Show a summary per file
| File | Description |
|---|---|
| specs/security-architecture-spec-summary.md | Documents SG invariants and maps each predicate to a concrete Go test, plus adds instructions for running the suite. |
| pkg/workflow/security_architecture_sg_formal_test.go | Adds a 15-test suite that exercises production code paths to continuously validate SG-related invariants. |
Review details
Tip
Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
- Files reviewed: 2/2 changed files
- Comments generated: 3
- Review effort level: Low
| for _, line := range []struct{ name string }{ | ||
| {string(constants.PreActivationJobName)}, | ||
| {string(constants.ActivationJobName)}, | ||
| {string(constants.AgentJobName)}, | ||
| {string(constants.DetectionJobName)}, | ||
| {string(constants.SafeOutputsJobName)}, | ||
| } { | ||
| if _, ok := sections[line.name]; !ok { | ||
| continue | ||
| } | ||
| // Find the byte-offset of the job's section header in the YAML. | ||
| needle := line.name + ":" | ||
| idx := strings.Index(yamlOut, "\n "+needle) | ||
| if idx < 0 { | ||
| idx = strings.Index(yamlOut, needle) | ||
| } | ||
| positions = append(positions, jobPos{name: line.name, line: idx}) | ||
| } | ||
|
|
||
| // Verify that every expected job is present. |
| SG04_LeastPrivilege ≜ | ||
| DefaultPermissions = {} ∧ | ||
| ∀ scope ∈ DefaultPermissions : scope.value = read |
| SG05_SandboxIsolation ≜ | ||
| isSandboxEnabled(sandboxConfig, network) ⟺ | ||
| (sandboxConfig.Agent.Type = AWF ∧ ¬sandboxConfig.Agent.Disabled) ∨ | ||
| network.Firewall.Enabled |
|
✅ PR Code Quality Reviewer completed the code quality review. |
|
🧠 Matt Pocock Skills Reviewer has completed the skills-based review. ✅ |
|
✅ Test Quality Sentinel completed test quality analysis. |
|
✅ Design Decision Gate 🏗️ completed the design decision gate check. |
🧪 Test Quality Sentinel Report✅ Test Quality Score: 98/100 — Excellent
📊 Metrics (15 tests)
Verdict
Highlights:
References: Warning Firewall blocked 1 domainThe following domain was blocked by the firewall during workflow execution:
network:
allowed:
- defaults
- "awmgmcpg"See Network Configuration for more information.
|
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
Review: Formal Model + 15-Test Suite for SG Invariants
The overall structure is solid — 15 focused tests, each mapping to a named predicate, no stubs, good TLA+/F*/Z3 documentation. One blocking correctness bug was found in the topology invariant test.
Blocking issue — topology check is trivially true
TestFormalJobTopology_PipelineOrderEnforced
positions is populated by iterating the canonical job list in canonical order (pre_activation, activation, agent, detection, safe_outputs). The slice is never sorted by its line (byte-offset) field, so foundOrder is always the canonical order regardless of what the compiler actually produces. formalJobOrderValid(foundOrder) is therefore trivially true and cannot catch a real ordering violation.
Fix: add sort.Slice(positions, func(i, j int) bool { return positions[i].line < positions[j].line }) before extracting foundOrder.
All other 14 tests are correct and well-scoped.
🧵 Reviewed using Impeccable skills by Impeccable Skills Reviewer · 47.6 AIC · ⌖ 4.46 AIC · ⊞ 4.8K
| for _, p := range positions { | ||
| foundOrder = append(foundOrder, p.name) | ||
| } | ||
| assert.True(t, formalJobOrderValid(foundOrder), |
There was a problem hiding this comment.
The positions slice is built by iterating the canonical job list in canonical order (pre_activation → activation → agent → detection → safe_outputs), so foundOrder is always the canonical order regardless of the actual byte-offsets in jobPos.line. The slice is never sorted by line before building foundOrder, making formalJobOrderValid(foundOrder) trivially true — it can never catch a real ordering violation.
To fix, sort positions by the line field before extracting foundOrder:
sort.Slice(positions, func(i, j int) bool {
return positions[i].line < positions[j].line
})Without this sort the topology invariant is untestable — the test always passes even if the compiler emits jobs in the wrong order.
@copilot please address this.
…chitecture invariants Records the decision to adopt TLA+/F*/Z3 formal specification methods and encode each of the 7 security guarantees as an executable Go unit test.
Design Decision Gate — ADR RequiredThis PR makes significant changes to core business logic (637 new lines in Draft ADR committed:
What to do next
Once an ADR is linked in the PR body, this gate will re-run and verify the implementation matches the decision. Why ADRs MatterADRs create a searchable, permanent record of why the codebase looks the way it does. Future contributors (and your future self) will thank you. Michael Nygard ADR Format ReferenceAn ADR must contain these four sections to be considered complete:
All ADRs are stored in
|
There was a problem hiding this comment.
Skills-Based Review 🧠
Applied /tdd — requesting changes on test correctness and assertion strength.
📋 Key Themes & Highlights
Key Issues
- Critical: topology test cannot fail —
positionsis built by iterating the canonical order and theidxbyte-offsets are never used to sort, soformalJobOrderValidalways sees canonical order regardless of actual YAML output (line 619). - Weak SG-03 assertion —
validateNetworkAllowedDomainsreturningNoErrordoes not verify blocked-domain precedence (line 141). - Silent-pass risk in staged-permissions test — the inner loop only fires for scopes already present in the permissions map; if
ComputePermissionsForSafeOutputsreturns an empty map, zero assertions execute (line 487). - SG-07 single-scope coverage — the
∀ wdinvariant is only exercised forcontents: write; other dangerous scopes are untested (line 278). - Substring match fragility in SG-06/BasicConformance — bare
DetectionJobName+":"matches any job whose name contains that string as a prefix (line 258).
Positive Highlights
- ✅ Comprehensive predicate-to-test mapping documented in the Behavioral Coverage Map — excellent traceability.
- ✅ Table-driven subtests in SG-02 cover every permission scope — the right pattern.
- ✅ All tests call production code directly with no test doubles — strong fidelity.
- ✅ Failure messages uniformly quote SG identifier and invariant clause — very debuggable.
- ✅
//go:build !integrationensures the full suite runs in default CI without flags.
🧠 Reviewed using Matt Pocock's skills by Matt Pocock Skills Reviewer · 52.5 AIC · ⌖ 4.89 AIC · ⊞ 6.6K
Comment /matt to run again
| // Verify that every expected job is present. | ||
| expectedJobs := []string{ | ||
| string(constants.PreActivationJobName), | ||
| string(constants.ActivationJobName), |
There was a problem hiding this comment.
[/tdd] The positions slice is never sorted by idx (byte-offset), so formalJobOrderValid always sees jobs in the fixed canonical iteration order — the topology invariant cannot actually fail.
💡 Fix: sort by byte-offset before validating order
import "sort"
sort.Slice(positions, func(i, j int) bool {
return positions[i].line < positions[j].line
})Without this, the test would pass even if the compiler emitted jobs in the wrong order.
@copilot please address this.
| compiler := NewCompiler() | ||
| err := compiler.validateNetworkAllowedDomains(net) | ||
| require.NoError(t, err, | ||
| "SG-03: allowed-domain validation must not fail when a blocked domain is also listed as allowed") |
There was a problem hiding this comment.
[/tdd] validateNetworkAllowedDomains is asserted to return NoError when a blocked domain is also in the allowed list, but this does not test the property it claims — it only checks that validation does not crash, not that the blocked domain actually takes precedence at runtime.
💡 Suggested strengthening
Also verify that blocked-domain precedence is enforced by the firewall or domain lookup rather than just the validator:
// after the NoError assertion, verify precedence is preserved
blocked := GetBlockedDomains(net)
assert.Contains(t, blocked, "evil.example.com",
"SG-03: evil.example.com must remain in block list even after validation runs")@copilot please address this.
| // | ||
| // Invariant: steps that use a known OIDC/vault action must trigger | ||
| // id-token:write — stepsRequireIDToken returns true. | ||
| // |
There was a problem hiding this comment.
[/tdd] The staged-permissions test only iterates scopes that Get returns with exists=true, so if a freshly-built staged permissions object returns nothing, the write-permission loop body never executes and the invariant trivially passes with zero assertions.
💡 Strengthen with an explicit scope check
// Assert that the full permissions object has no write grants for known scopes
for _, scope := range GetAllPermissionScopes() {
val, _ := perms.Get(scope)
assert.NotEqual(t, PermissionWrite, val,
"StagedHandlerNoWritePerms: staged create-issue must not grant %s:write", scope)
}This removes the guard that silently skips absent scopes.
@copilot please address this.
| strict: false | ||
| permissions: | ||
| contents: write | ||
| --- |
There was a problem hiding this comment.
[/tdd] SG-07 tests contents: write but the formal invariant is declared as ∀ wd : DangerousPermissions(wd) ⟹ .... No test covers other dangerous scopes (e.g. actions: write, packages: write). A future permission scope could silently bypass the invariant.
💡 Add a table-driven variant
dangerousScopes := []PermissionScope{PermissionContents, PermissionActions, PermissionPackages}
for _, scope := range dangerousScopes {
t.Run(string(scope), func(t *testing.T) {
// inline SG-07 check for this scope
})
}@copilot please address this.
| assert.Contains(t, yamlOut, string(constants.DetectionJobName)+":", | ||
| "SG-06: compiled workflow must contain a %q job — threat detection audit artifact is missing", | ||
| constants.DetectionJobName) | ||
| } |
There was a problem hiding this comment.
[/tdd] SG-06 asserts that constants.DetectionJobName+":" appears as a substring in the YAML, but a job named my_detection: would also match. Tighten the assertion to check job-level indentation to avoid false positives.
💡 Suggested fix
assert.Contains(t, yamlOut, "\n "+string(constants.DetectionJobName)+":",
"SG-06: detection job must appear as a top-level YAML job entry")@copilot please address this.
There was a problem hiding this comment.
REQUEST_CHANGES — three correctness bugs in the formal test suite
Two tests are permanently tautological (they always pass regardless of production code behaviour) and the job-topology test has a logic inversion that makes it unable to detect ordering regressions. These must be fixed before the test suite can make the security guarantees it claims.
Blocking issues (3)
1. Topology ordering assertion is permanently vacuous (line 603 — critical)
foundOrder is populated by iterating over the canonical-order slice, so it is always already in canonical order. formalJobOrderValid will always return true. A reordered compiled YAML is undetectable. Fix: use the order information already produced by formalJobSections.
2. StagedHandlerNoWritePerms loop never fires (line 474 — high)
The if exists guard means the inner assert is never reached when ComputePermissionsForSafeOutputs returns an empty map. The test proves nothing about write-permission grants. Add an unconditional negative assertion (e.g. HasAnyWrite()) or a control case with an un-staged config that does produce write grants.
3. formalJobOrderValid vacuously returns true on empty input (line 635 — medium)
If YAML parsing or string scanning produces zero positions, the order assertion passes silently. Add a require.GreaterOrEqual guard on len(foundOrder) before calling formalJobOrderValid.
Non-blocking spec issues (2)
SG04 TLA+ invariant is a tautology (spec line 90): ∀ scope ∈ DefaultPermissions ranges over an empty set because the preceding conjunct asserts DefaultPermissions = {}. Should range over AllPermissionScopes.
SG03 TLA+ invariant is a tautology (spec line 88): domain ∈ GetBlockedDomains(network) is trivially true if GetBlockedDomains returns the .blocked field directly. The invariant should assert precedence over the allowed list instead.
🔎 Code quality review by PR Code Quality Reviewer · 78.6 AIC · ⌖ 5.14 AIC · ⊞ 5.4K
Comment /review to run again
| {string(constants.AgentJobName)}, | ||
| {string(constants.DetectionJobName)}, | ||
| {string(constants.SafeOutputsJobName)}, | ||
| } { |
There was a problem hiding this comment.
Topology ordering assertion is permanently vacuous: foundOrder is always already in canonical order because positions is built by iterating over the hardcoded canonical slice — so formalJobOrderValid will always return true regardless of the actual YAML job order.
💡 Details and fix
Lines 603–619 iterate over a hardcoded canonical-order slice and append to positions in that same order. So foundOrder is always [pre_activation, activation, agent, detection, safe_outputs], trivially satisfying formalJobOrderValid. A reordered compiled YAML would never be caught.
The formalJobSections helper already captures the real insertion order of job sections in the YAML via its internal order slice — expose and use that instead:
// Change formalJobSections signature to also return []string (order).
sections, yamlOrder := formalJobSections(yamlOut)
assert.True(t, formalJobOrderValid(yamlOrder), ...)Until fixed, this test cannot falsify a misordered pipeline.
| } | ||
| perms := ComputePermissionsForSafeOutputs(stagedConfig) | ||
| require.NotNil(t, perms) | ||
| for _, scope := range GetAllPermissionScopes() { |
There was a problem hiding this comment.
StagedHandlerNoWritePerms write-permission loop never fires: if ComputePermissionsForSafeOutputs returns an empty map, perms.Get will return exists=false for every scope and the inner assert.NotEqual is never reached — the test always passes vacuously.
💡 Details and fix
The loop body is guarded by if exists. When all handlers are staged the returned Permissions struct has an empty internal map, so exists is never true. The test therefore proves nothing about whether write permissions are or are not granted.
Fix: assert unconditionally that each scope is absent or non-write, and add a length sanity check:
perms := ComputePermissionsForSafeOutputs(stagedConfig)
require.NotNil(t, perms)
for _, scope := range GetAllPermissionScopes() {
val, exists := perms.Get(scope)
if exists {
assert.NotEqual(t, PermissionWrite, val, "staged handler must not grant %s:write", scope)
}
}
// Assert that no write-granting scopes leaked through at all.
assert.False(t, perms.HasAnyWrite(),
"StagedHandlerNoWritePerms: staged config must not accumulate any write grant")If HasAnyWrite() does not exist, at minimum add a require that the function is exercised non-trivially (e.g. use an un-staged config as the control case that does produce write grants).
| for _, p := range positions { | ||
| foundOrder = append(foundOrder, p.name) | ||
| } | ||
| assert.True(t, formalJobOrderValid(foundOrder), |
There was a problem hiding this comment.
formalJobOrderValid vacuously returns true when foundOrder is empty: if string scanning fails to populate positions (e.g. YAML format changes), foundOrder is nil, and formalJobOrderValid(nil) returns true immediately with zero iterations.
💡 Details and fix
formalJobOrderValid starts with for i := 1; i < len(canonical); ... but the check compares positions from idx map built from the input slice, not from canonical. If the input is empty or nil, the loop body never fires and the function returns true.
Combined with the separate bug where foundOrder is always in canonical order (see comment at line 603), this test can never detect a job ordering regression.
Add a guard:
require.GreaterOrEqual(t, len(foundOrder), 5,
"JobTopologyOrder: expected at least 5 jobs in compiled YAML, got %d", len(foundOrder))
assert.True(t, formalJobOrderValid(foundOrder), ...)| domain ∈ GetBlockedDomains(WorkflowState.network) | ||
|
|
||
| SG04_LeastPrivilege ≜ | ||
| DefaultPermissions = {} ∧ |
There was a problem hiding this comment.
SG04_LeastPrivilege formal invariant is a tautology: the second conjunct ∀ scope ∈ DefaultPermissions : scope.value = read is vacuously true when DefaultPermissions = {}, so the invariant never constrains any permission value.
💡 Details and fix
The invariant asserts DefaultPermissions = {} and ∀ scope ∈ DefaultPermissions : scope.value = read. Because the first conjunct makes the domain empty, the universal quantifier fires zero times and is trivially satisfied. A regression where a default permission with a write value is added would not be caught by this invariant.
The intended invariant should range over all scopes and assert that none has a default write value:
SG04_LeastPrivilege ≜
∀ scope ∈ AllPermissionScopes :
DefaultPermissions[scope] ≠ write
The corresponding Go test (TestFormalSG04_LeastPrivilegeBasePermissions) tests the right thing (validates that a fresh NewPermissions() has no write grants), but the formal spec it claims to encode is wrong.
| SG03_NetworkAllowlist ≜ | ||
| ∀ domain ∈ WorkflowState.network.blocked : | ||
| domain ∈ GetBlockedDomains(WorkflowState.network) | ||
|
|
There was a problem hiding this comment.
SG03_NetworkAllowlist TLA+ invariant is a tautology: asserting domain ∈ GetBlockedDomains(network) for every domain ∈ network.blocked is trivially true if GetBlockedDomains simply returns the .blocked field — the invariant encodes no enforcement property.
💡 Details and fix
The meaningful SG-03 property is that a domain in blocked takes precedence over the allowed list — i.e. it is not reachable even when also listed as allowed. The invariant should be:
SG03_NetworkAllowlist ≜
∀ domain ∈ network.blocked :
domain ∉ EffectiveAllowedDomains(network)
where EffectiveAllowedDomains is the set of domains that actually pass through after blocked-list filtering. The current wording conflates the blocked field with enforcement and cannot detect a regression where blocked domains are ignored at runtime.
|
@copilot please run the
|
Co-authored-by: gh-aw-bot <259018956+gh-aw-bot@users.noreply.github.com>
Co-authored-by: gh-aw-bot <259018956+gh-aw-bot@users.noreply.github.com>
Done. Addressed all three unresolved review threads:
Local |
specs/security-architecture-spec-summary.mdlacked an executable formalization of its 7 security guarantees (SG-01 through SG-07). This adds a TLA+/F*/Z3 formal model and a Go test suite that encodes each guarantee as a continuously-verified CI invariant.specs/security-architecture-spec-summary.mdThree new sections inserted after "Core Security Guarantees":
parseThreatDetectionConfig/IsContinueOnError, Z3/SMT-LIB bounds for conformance level ordering, and the canonical job topology invariantpkg/workflow/security_architecture_sg_formal_test.go(new)15
TestFormal*functions (//go:build !integration), each calling production code directly with no stubs:TestFormalSG01_InputSanitizationInvariantTestFormalSG02_AgentJobHasNoWritePermissionsTestFormalSG03_NetworkAllowlistEnforcementTestFormalSG04_LeastPrivilegeBasePermissionsTestFormalSG05_SandboxIsolationPresenceTestFormalSG06_ThreatDetectionAuditArtifactTestFormalSG07_FailSecureOnSecurityErrorTestFormalBasicConformance_AllFourControlsTestFormalThreatDetection_EnabledByDefault,_ExplicitDisableIsContinueOnErrornil defaultTestFormalThreatDetection_ContinueOnErrorDefaultTestFormalStaged_HandlerRequiresNoWritePermsTestFormalIDToken_OIDCVaultActionsRequireWriteScopeTestFormalPushFallback_DefaultsToTrueTestFormalJobTopology_PipelineOrderEnforcedThe topology test compiles a real workflow with
create-issuesafe-outputs and verifies thepre_activation → activation → agent → detection → safe_outputssection order in the emitted YAML using the existingformalJobSections/formalJobOrderValidhelpers.