Skip to content

Commit b0adab0

Browse files
bugerclaude
andcommitted
Update catalog dogfood case study for v0.3.0 catalog refinements
After this dogfood surfaced three structural findings (loosened denial_of_service_resistant trigger, leaf-detection in obligation_decomposition_complete, three-bucket coverage reporting), they were fixed in ReqProof v0.3.0 before ship. Update the case study coverage excerpt to use the new accepted/suppressed/missing buckets with decided/active coverage percentages, and document the three findings the dogfood produced. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent a50174c commit b0adab0

1 file changed

Lines changed: 47 additions & 14 deletions

File tree

PROOF_CATALOG_DOGFOOD_CASE_STUDY.md

Lines changed: 47 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -160,26 +160,59 @@ relevant authority (RFC 8259) rather than hand-waving "doesn't apply."
160160

161161
After tagging and resolution, OWASP-ASVS-v4 coverage:
162162

163-
> **OWASP Application Security Verification Standard v4.0.3** — 6 controls,
164-
> 0 covered, 6 suppressed, 0 missing (100.0% covered+suppressed)
163+
> **OWASP Application Security Verification Standard v4.0.3** — 6 controls
164+
> accepted: 0 suppressed: 6 missing: 0
165+
> decided coverage: 100.0% active coverage: 0.0%
165166
166167
CWE coverage:
167168

168-
> **Common Weakness Enumeration** — 14 controls, 0 covered, 14 suppressed, 0 missing
169-
> (100.0% covered+suppressed)
169+
> **Common Weakness Enumeration** — 14 controls
170+
> accepted: 0 suppressed: 14 missing: 0
171+
> decided coverage: 100.0% active coverage: 0.0%
170172
171173
MISRA-C coverage:
172174

173-
> **MISRA C:2023 — Guidelines for the Use of C in Critical Systems** — 3 controls,
174-
> 0 covered, 3 suppressed, 0 missing (100.0% covered+suppressed)
175-
176-
The "0 covered, N suppressed" reading is a side-effect of the decomposition strategy
177-
described above — we recorded each catalog obligation as a *decomposition-routed
178-
suppression* on the STK-REQ rather than as an active checklist commitment, because
179-
the leaves cannot themselves carry a checklist without breaking the "every checklist
180-
needs a child satisfier" decomposition rule. A future catalog version that adds a
181-
"leaf-terminator" marker would let these flip from `suppressed` to `covered`. The
182-
SARIF artifact is 6,393 bytes and ships every framework reference.
175+
> **MISRA C:2023 — Guidelines for the Use of C in Critical Systems** — 3 controls
176+
> accepted: 0 suppressed: 3 missing: 0
177+
> decided coverage: 100.0% active coverage: 0.0%
178+
179+
The headline metric — **decided coverage** — is the fraction of controls the project
180+
has explicitly addressed (either by committing or by suppressing with rationale).
181+
Active coverage is the stricter sub-metric: only checklist commitments count. For
182+
jsonparser, every framework citation is `decided` because every obligation is either
183+
on a checklist or carries a written suppression rationale; nothing is silently
184+
unaddressed.
185+
186+
(This three-bucket layout was added in v0.3.0 — D30 / Finding 3 below — after the
187+
earlier "0 covered, N suppressed" framing read as misleading red on otherwise
188+
fully-decided projects.)
189+
190+
The SARIF artifact ships every framework reference and now includes a `properties`
191+
block on each missing-coverage result with the framework's three counts and both
192+
percentages, so GitHub Code Scanning and GRC tooling can render decided coverage
193+
alongside the finding.
194+
195+
## Findings surfaced by this dogfood (resolved in v0.3.0)
196+
197+
Three structural improvements to the catalog were discovered by applying it to
198+
jsonparser, a project that is nothing like ReqProof itself, and shipped in v0.3.0:
199+
200+
1. **Discoverability gap on `denial_of_service_resistant`**: the obligation
201+
was gated on `tag_match_any: [accepts_user_data]`, which meant a parser
202+
library spec author tagging only `parser` (the natural intuition) silently
203+
missed a CRITICAL DoS obligation. Loosened to fire whenever `parser` is
204+
tagged; trusted-input parsers may suppress with rationale.
205+
2. **Leaf-terminator false positive in `obligation_decomposition_complete`**:
206+
leaves with obligations on their checklist were being flagged as having
207+
"no derived requirements" — but leaves don't decompose further, that's the
208+
point. Added leaf detection: a leaf with `implemented_by` traces passes;
209+
a leaf with obligations but no `implemented_by` gets the new
210+
`LeafObligationWithoutImplementation` finding instead.
211+
3. **Coverage report messaging** (the section above): "0 covered, N suppressed"
212+
reads as 0% in the headline. Now: three buckets (accepted / suppressed /
213+
missing) plus `decided coverage` and `active coverage` percentages,
214+
surfacing the difference between "actively committed" and "explicitly
215+
addressed".
183216

184217
## What this proves
185218

0 commit comments

Comments
 (0)