spdd: 2026-07-11 spec work plan — normative requirements, combined-integrity fixture, coverage audit#44986
Conversation
- guard-policies-specification.md: add ## Normative Requirements (GP-001–GP-006) covering allowed-repos, min-integrity, safe-outputs derivation, extension points - guard-policies-specification.md: add ## Sync Follow-ups naming schemas/mcp-gateway-config.schema.json and Go policy implementation files - github-mcp-access-control-compliance/combined-blocked-integrity.yaml: new fixture covering P5_NotBlocked + P6_IntegrityMet evaluated simultaneously (T-GH-91–093) - github-mcp-access-control-compliance/README.md: register new fixture in table and coverage map - github-mcp-access-control-specification.md: add ## Sync Follow-ups naming Go implementation file and compliance README as mandatory sync targets - security-architecture-spec.md: add Appendix G.10 formal test coverage audit table for all 9 checklist items with gap analysis - security-architecture-spec-validation.md: add §4b PM-11 formal test coverage audit noting gap and recommending TestFormalPM11_PreActivationContainsMembershipStep Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>
- security-architecture-spec.md G.10: clarify table intro (zero/one/many tests); fix §4 → §4b cross-reference - guard-policies-specification.md: add JSON path (#/definitions/...) for schema objects - github-mcp-access-control-specification.md: clarify mcp_access_control.go reference Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>
🤖 PR Triage
Spec/planning docs only (SPDD work plan). Draft state, no code changes, low urgency. Defer.
|
🤖 PR Triage
Rationale: Draft. Daily SPDD spec work plan document. Informational/process-tracking content, not a behavioral change. Defer. Triage run §29183606049
|
There was a problem hiding this comment.
Pull request overview
Adds SPDD specification requirements, compliance fixtures, synchronization guidance, and formal-test coverage audits.
Changes:
- Defines guard-policy requirements and synchronization targets.
- Adds combined blocked-user/integrity compliance scenarios.
- Audits security architecture formal-test coverage.
Show a summary per file
| File | Description |
|---|---|
specs/security-architecture-spec.md |
Adds Appendix G coverage audit. |
specs/security-architecture-spec-validation.md |
Documents the PM-11 formal-test gap. |
specs/github-mcp-access-control-compliance/README.md |
Registers combined-integrity coverage. |
specs/github-mcp-access-control-compliance/combined-blocked-integrity.yaml |
Adds five P5/P6 scenarios. |
scratchpad/guard-policies-specification.md |
Adds normative requirements and sync guidance. |
scratchpad/github-mcp-access-control-specification.md |
Adds access-control sync guidance. |
Review details
Tip
Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
- Files reviewed: 6/6 changed files
- Comments generated: 20
- Review effort level: Medium
| |---|---|---| | ||
| | **G.1** Action pinning | _(none)_ | **gap** — no formal test verifies that compiled `uses:` lines are SHA-pinned; relies on actionlint/poutine in CI | | ||
| | **G.2** Permission separation — agent job | `TestFormalSG02_AgentJobHasNoWritePermissions`, `TestFormalSG04_LeastPrivilegeBasePermissions` | covered | | ||
| | **G.2** Permission separation — safe_outputs job | `TestFormalStaged_HandlerRequiresNoWritePerms` | covered | |
There was a problem hiding this comment.
Fixed in a179a1f — G.2 safe-output row is now marked partial with the accurate rationale: TestFormalStaged_HandlerRequiresNoWritePerms verifies the handler does not accumulate write grants but does not inspect the compiled safe_outputs job's own permissions: block.
| | **G.1** Action pinning | _(none)_ | **gap** — no formal test verifies that compiled `uses:` lines are SHA-pinned; relies on actionlint/poutine in CI | | ||
| | **G.2** Permission separation — agent job | `TestFormalSG02_AgentJobHasNoWritePermissions`, `TestFormalSG04_LeastPrivilegeBasePermissions` | covered | | ||
| | **G.2** Permission separation — safe_outputs job | `TestFormalStaged_HandlerRequiresNoWritePerms` | covered | | ||
| | **G.3** Fork protection | `TestFormalBasicConformance_AllFourControls` (compiles a real workflow; fork guard verified via activation `if:`) | covered | |
There was a problem hiding this comment.
Fixed in a179a1f — G.3 fork protection row is now marked partial with rationale: TestFormalBasicConformance_AllFourControls covers safe_outputs job presence and permission management but does not inspect the activation job's if: expression or assert a repository-ID fork guard.
| | **G.2** Permission separation — agent job | `TestFormalSG02_AgentJobHasNoWritePermissions`, `TestFormalSG04_LeastPrivilegeBasePermissions` | covered | | ||
| | **G.2** Permission separation — safe_outputs job | `TestFormalStaged_HandlerRequiresNoWritePerms` | covered | | ||
| | **G.3** Fork protection | `TestFormalBasicConformance_AllFourControls` (compiles a real workflow; fork guard verified via activation `if:`) | covered | | ||
| | **G.4** Input sanitization | `TestFormalSG01_InputSanitizationInvariant` | covered | |
There was a problem hiding this comment.
Fixed in a179a1f — G.4 input sanitization row is now marked partial: TestFormalSG01_InputSanitizationInvariant verifies expression rewriting in a generic run: step but does not assert either required activation step or that compiled prompts consume steps.sanitized.outputs.text.
| | **G.2** Permission separation — safe_outputs job | `TestFormalStaged_HandlerRequiresNoWritePerms` | covered | | ||
| | **G.3** Fork protection | `TestFormalBasicConformance_AllFourControls` (compiles a real workflow; fork guard verified via activation `if:`) | covered | | ||
| | **G.4** Input sanitization | `TestFormalSG01_InputSanitizationInvariant` | covered | | ||
| | **G.5** Threat detection | `TestFormalSG06_ThreatDetectionAuditArtifact`, `TestFormalThreatDetection_EnabledByDefault`, `TestFormalThreatDetection_ExplicitDisable` | covered | |
There was a problem hiding this comment.
Fixed in a179a1f — G.5 threat detection row is now marked partial: detection-job presence and configuration defaults are covered, but permissions: {} on the detection job and the needs.detection.outputs.success gate on safe_outputs are not directly asserted.
| | **G.5** Threat detection | `TestFormalSG06_ThreatDetectionAuditArtifact`, `TestFormalThreatDetection_EnabledByDefault`, `TestFormalThreatDetection_ExplicitDisable` | covered | | ||
| | **G.6** RBAC — job topology (PM-10b) | `TestFormalJobTopology_PipelineOrderEnforced` (verifies `pre_activation → activation` needs dependency) | covered | | ||
| | **G.6** RBAC — membership check step (PM-11) | _(none)_ | **gap** — `TestFormalJobTopology_PipelineOrderEnforced` verifies job ordering but does NOT assert that the `pre_activation` job contains a `check_membership.cjs` step; no dedicated PM-11 formal test exists in this file | | ||
| | **G.7** AWF sandbox | `TestFormalSG05_SandboxIsolationPresence` | covered | |
There was a problem hiding this comment.
Fixed in a179a1f — G.7 AWF sandbox row is now marked partial: TestFormalSG05_SandboxIsolationPresence verifies isSandboxEnabled() for configuration combinations but does not compile a workflow or assert install_awf_binary.sh step presence or execution inside the AWF container.
|
|
||
| 2. **`specs/github-mcp-access-control-compliance/README.md`** — Update the Formal Model section (`ALLOW(r, c) ≜ …`) and the Behavioral Coverage Map table to reflect the new predicate order. Regenerate `TestFormal_BlockedUserSafetyProperty` and `TestFormal_ErrorCodeFirstFailingGuard` test cases to match. | ||
|
|
||
| 3. **`specs/github-mcp-access-control-compliance/combined-blocked-integrity.yaml`** — Review the `combined-blocked-integrity-C` and `combined-blocked-integrity-D` scenarios whose expected error codes depend on the relative order of P5_NotBlocked vs P6_IntegrityMet. Update expected `error_code` values if the predicate order changes. |
There was a problem hiding this comment.
Fixed in a179a1f — the "revisit if order changes" note is now narrowed to Scenario C only. Scenario D has the user blocked AND integrity merged ≥ approved threshold, so P6 already passes regardless of evaluation order.
| | **G.8** Concurrency control | _(none)_ | **gap** — no formal test verifies `concurrency.group` is set or that `cancel-in-progress` matches workflow type | | ||
| | **G.9** Runtime validation — timestamp check | `TestFormalSG07_FailSecureOnSecurityError` (compilation fail-secure; does not verify timestamp step) | partial — fail-secure behavior covered; timestamp step presence not directly asserted | | ||
|
|
||
| **Summary of coverage gaps (as of 2026-07-11)**: |
There was a problem hiding this comment.
Fixed in a179a1f — the summary section now itemises all nine gaps/partial items: G.1, G.2 (safe_outputs job), G.3, G.4, G.5, G.6 (PM-11 membership step), G.7, G.8, and G.9.
| - "§4.5.3 — predicate evaluation order: P5_NotBlocked evaluated before P6_IntegrityMet" | ||
| - "§7.2 — blocked-users MUST deny access unconditionally for listed actors" | ||
| - "§8.1 — min-integrity allows content at or above the configured threshold" |
There was a problem hiding this comment.
Fixed in a179a1f — section references in the fixture header and spec_refs are corrected: §4.5.3 → §8.5, §7.2 → §8.2, §8.1 → §8.4. Scenario C's inline reference is also updated to §8.5.
| This section lists the files that **MUST** be reviewed and updated whenever a normative section of this specification changes, especially §4.5.3 (predicate evaluation order), §4.4 (field definitions), and §11 (compliance tests). | ||
|
|
||
| ### After Changing §4.5.3 Predicate Evaluation Order |
There was a problem hiding this comment.
Fixed in a179a1f — §4.5.3 is replaced with the correct §8.5 (Combined Evaluation Order) throughout the Sync Follow-ups section.
|
@copilot please run the Run: https://github.com/github/gh-aw/actions/runs/29187567992
|
- specs/security-architecture-spec.md: correct Appendix G.10 coverage audit table — G.2 safe_outputs, G.3, G.4, G.5, G.7 downgraded from 'covered' to 'partial' with accurate rationale; G.9 changed from 'partial' to 'gap' (TestFormalSG07 is unrelated); summary extended to list all newly-identified partial/gap items - specs/github-mcp-access-control-compliance/README.md: replace nonexistent TestFormal_CombinedBlockedIntegrity with TestFormal_FixtureRunner - specs/github-mcp-access-control-compliance/combined-blocked-integrity.yaml: fix section references (§4.5.3→§8.5, §7.2→§8.2, §8.1→§8.4) in header, spec_refs, and Scenario C description - scratchpad/github-mcp-access-control-specification.md: register T-GH-91–093 in §11.1.10 and add combined-blocked-integrity.yaml to §11.4 fixture table; fix Sync Follow-ups (§4.5.3→§8.5, replace fabricated mcp_access_control.go with actual runtime/test-model locations, narrow 'revisit if order changes' to Scenario C only) - scratchpad/guard-policies-specification.md: remove duplicate GP-001–006 'Normative Requirements' section (consolidates with existing GP-01–11 Conformance section); fix GP-01 to accept '${{ github.repository }}' scalar; fix GP-03 to allow expression exception in arrays; fix Sync Follow-ups schema paths to both pkg/workflow/schemas/ and docs/public/schemas/ copies, clarify guard-policies placement, and use 'definitions' (draft-07) not '$defs' Co-authored-by: gh-aw-bot <259018956+gh-aw-bot@users.noreply.github.com>
All review feedback addressed in commit
|
|
@copilot please run the Run: https://github.com/github/gh-aw/actions/runs/29190625506
|
All 19 unresolved review threads have been replied to and the prior code fixes confirmed.
Hand-off: A maintainer needs to re-trigger CI (close/reopen the PR, |
|
\n@copilot please run the skill, address the unresolved review feedback on the coverage audit/spec references and normative requirement mismatches, then rerun checks once updates are complete.
|
🤖 PR Triage
Spec work plan document. +254/-2. Low urgency, documentation only. Defer for when spec work is prioritized.
|
|
@copilot please run the
|
All review feedback was already addressed in
No remaining unresolved review feedback — all 19 threads were addressed and replied to in the previous pass (see |
|
@copilot please run the Run: https://github.com/github/gh-aw/actions/runs/29196572530
|
All review feedback was addressed in
No further changes needed. Ready for human CI re-trigger and merge. |
Implements all eight checklist items from the daily SPDD plan covering five spec files. Key gaps addressed: guard-policies spec lacked RFC 2119 normative requirements and schema sync targets; MCP access control compliance had no combined P5+P6 failure scenario; Appendix G had no machine-readable coverage audit; PM-11 membership validation had no formal test.
guard-policies-specification.md
## Normative Requirements— six GP-001…GP-006 SHALL/SHALL NOT requirements coveringallowed-repostype validation,min-integrityenum, pattern syntax, cross-field consistency (non-"all"scope withoutmin-integrityrejected), safe-outputs write-sink derivation, and absent-policy-is-not-permissive semantics.## Sync Follow-ups— explicitly namesschemas/mcp-gateway-config.schema.json(#/definitions/stdioServerConfig,#/definitions/httpServerConfig),tools_validation_github.go,mcp_github_config.go, andtools_types.goas mandatory update targets when normative sections change.MCP access control compliance
combined-blocked-integrity.yaml— new fixture (5 scenarios, T-[copilot] consistent table rendering #91–093) forP5_NotBlocked ∧ P6_IntegrityMetsimultaneous evaluation; key scenario: blocked user with sub-threshold integrity yields-32005(P5 fires first per §4.5.3 order), not-32006.github-mcp-access-control-specification.md
## Sync Follow-ups— namespkg/workflow/mcp_access_control.goand the compliance README as mandatory sync targets when §4.5.3 predicate order or §4.4 fields change; calls out thatcombined-blocked-integrity.yamlscenarios C/D must be revisited if P5/P6 ordering ever changes.security-architecture-spec.md
security_architecture_sg_formal_test.go. Three gaps identified: G.1 action pinning (covered by CI tooling, not by a Go test), G.6 PM-11 membership check step (topology verified; step content not asserted), G.8 concurrency control (no formal test).security-architecture-spec-validation.md
TestFormalSG04_LeastPrivilegeBasePermissionsandTestFormalJobTopology_PipelineOrderEnforceddo not assert that thepre_activationjob contains acheck_membership.cjsstep; recommendsTestFormalPM11_PreActivationContainsMembershipStepas the closure test.