From daa39d279a77e50f5f7523066e84c3168e22939a Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Tue, 14 Apr 2026 08:27:35 -0700 Subject: [PATCH 1/2] fix: add falsification discipline to security audit template MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three changes to reduce false positive findings in security audits: 1. Add adversarial-falsification protocol to investigate-security template. The template previously lacked the protocol that requires actively disproving each finding before reporting it. This omission allowed findings to be reported without checking for upstream validation in caller functions or API postconditions. 2. Add validation provenance check to security-vulnerability protocol (Phase 2, step 5). The protocol described forward tracing (entry point to use site) but not backward tracing (use site back to validation origin). The new step requires checking caller validation, API postconditions, and initialization-time invariants before reporting any finding. 3. Add symmetric falsification to self-verification protocol (Rule 1). The sampling verification step now requires attempting to disprove reported findings with the same rigor applied when falsifying candidates that were concluded safe — breaking confirmation bias toward reporting. Motivated by a real audit where 2 of 9 findings were false positives because upstream validation (in a caller function and a kernel API contract) was missed. The audit correctly falsified 6 other candidates as safe, demonstrating the capability existed but was applied asymmetrically. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- manifest.yaml | 2 +- protocols/analysis/security-vulnerability.md | 15 +++++++++++++++ protocols/guardrails/self-verification.md | 6 ++++++ templates/investigate-security.md | 1 + 4 files changed, 23 insertions(+), 1 deletion(-) diff --git a/manifest.yaml b/manifest.yaml index dd3eaee..0a1ea5e 100644 --- a/manifest.yaml +++ b/manifest.yaml @@ -1351,7 +1351,7 @@ templates: Security audit of code or a system component. Systematic vulnerability analysis with severity classification. persona: security-auditor - protocols: [anti-hallucination, self-verification, operational-constraints, security-vulnerability] + protocols: [anti-hallucination, self-verification, operational-constraints, adversarial-falsification, security-vulnerability] taxonomies: [stack-lifetime-hazards] format: investigation-report diff --git a/protocols/analysis/security-vulnerability.md b/protocols/analysis/security-vulnerability.md index 95e86ae..ca21980 100644 --- a/protocols/analysis/security-vulnerability.md +++ b/protocols/analysis/security-vulnerability.md @@ -48,6 +48,21 @@ For every external input: re-encoded, decoded, or transformed before use. 4. Check for **integer overflow/underflow** in size or length parameters derived from external input. +5. **Validation provenance check**: For every candidate vulnerability at + a use site, trace **backward** to find all validation that may have + occurred between the input's entry and the use. Check: + - Caller functions that decode or validate before passing values + (e.g., a header-decode helper that checks `Field > MaxAllowed` + before the caller uses `Field` in arithmetic) + - Helper functions called earlier in the same code path + - API postconditions — when a system API (e.g., kernel API, stdlib) + returns success, what guarantees does it make about output buffer + contents, lengths, or value ranges? + - Initialization-time invariants — constructor or init functions + that constrain values to safe ranges (e.g., power-of-2 + requirements, maximum bounds) + Do NOT report a finding until you have confirmed that no upstream + validation neutralizes it. ## Phase 3: Authentication and Authorization diff --git a/protocols/guardrails/self-verification.md b/protocols/guardrails/self-verification.md index 3c94fbb..179ebe7 100644 --- a/protocols/guardrails/self-verification.md +++ b/protocols/guardrails/self-verification.md @@ -36,6 +36,12 @@ presenting it as final. Treat it as a pre-submission checklist. - Does the evidence actually support the conclusion stated? - If any sampled item fails verification, **re-examine all items of the same type** before proceeding. +- For each sampled finding, apply **symmetric falsification**: attempt + to disprove the finding with the same rigor you applied when + falsifying candidate findings that you concluded were safe. Ask: + "Is there a validation, API contract, or initialization invariant + I missed that makes this safe?" If you cannot answer "no" with + specific code evidence, downgrade or remove the finding. ### 2. Citation Audit diff --git a/templates/investigate-security.md b/templates/investigate-security.md index 7926d07..886efc1 100644 --- a/templates/investigate-security.md +++ b/templates/investigate-security.md @@ -12,6 +12,7 @@ protocols: - guardrails/anti-hallucination - guardrails/self-verification - guardrails/operational-constraints + - guardrails/adversarial-falsification - analysis/security-vulnerability taxonomies: - stack-lifetime-hazards From bf241cee7334412d5f6034395efa36d06c3ef0bd Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Tue, 14 Apr 2026 08:39:36 -0700 Subject: [PATCH 2/2] fix: replace prove-a-negative phrasing with auditable documentation requirements Address review feedback: 'confirmed no upstream validation' and 'answer no with code evidence' ask for proof of nonexistence, which is hard to satisfy consistently. Rephrase to require explicit documentation of what was checked, the evidence source, and why each check does not neutralize the finding. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- protocols/analysis/security-vulnerability.md | 8 ++- protocols/guardrails/self-verification.md | 10 ++-- .../reasoning/exhaustive-path-tracing.md | 1 + templates/investigate-security.md | 55 ++++++++++++++++++- 4 files changed, 65 insertions(+), 9 deletions(-) diff --git a/protocols/analysis/security-vulnerability.md b/protocols/analysis/security-vulnerability.md index ca21980..9c190bf 100644 --- a/protocols/analysis/security-vulnerability.md +++ b/protocols/analysis/security-vulnerability.md @@ -61,8 +61,12 @@ For every external input: - Initialization-time invariants — constructor or init functions that constrain values to safe ranges (e.g., power-of-2 requirements, maximum bounds) - Do NOT report a finding until you have confirmed that no upstream - validation neutralizes it. + Do NOT report a finding until you have explicitly documented: + - Which upstream validators, contracts, and invariants you checked + - The evidence or source for any API postconditions you relied on + (e.g., vendor documentation, manpage, or header annotations) + - Why each checked item does not neutralize the candidate + vulnerability in this code path ## Phase 3: Authentication and Authorization diff --git a/protocols/guardrails/self-verification.md b/protocols/guardrails/self-verification.md index 179ebe7..30f1829 100644 --- a/protocols/guardrails/self-verification.md +++ b/protocols/guardrails/self-verification.md @@ -38,10 +38,12 @@ presenting it as final. Treat it as a pre-submission checklist. the same type** before proceeding. - For each sampled finding, apply **symmetric falsification**: attempt to disprove the finding with the same rigor you applied when - falsifying candidate findings that you concluded were safe. Ask: - "Is there a validation, API contract, or initialization invariant - I missed that makes this safe?" If you cannot answer "no" with - specific code evidence, downgrade or remove the finding. + falsifying candidate findings that you concluded were safe. Verify + whether any upstream validation, API contract, or initialization + invariant makes this safe; cite the specific call sites, checks, or + invariants reviewed and explain why they do not neutralize the + finding. If you have not verified that upstream validation does not + apply, downgrade or remove the finding. ### 2. Citation Audit diff --git a/protocols/reasoning/exhaustive-path-tracing.md b/protocols/reasoning/exhaustive-path-tracing.md index d57459a..2b0a12f 100644 --- a/protocols/reasoning/exhaustive-path-tracing.md +++ b/protocols/reasoning/exhaustive-path-tracing.md @@ -11,6 +11,7 @@ description: > applicable_to: - review-code - investigate-bug + - investigate-security - exhaustive-bug-hunt --- diff --git a/templates/investigate-security.md b/templates/investigate-security.md index 886efc1..cf57c3c 100644 --- a/templates/investigate-security.md +++ b/templates/investigate-security.md @@ -14,6 +14,7 @@ protocols: - guardrails/operational-constraints - guardrails/adversarial-falsification - analysis/security-vulnerability + - reasoning/exhaustive-path-tracing # optional — apply selectively to parser/decoder functions taxonomies: - stack-lifetime-hazards format: investigation-report @@ -89,6 +90,42 @@ code or system component. - Prefer deterministic methods (targeted search, structured enumeration) - Document your search strategy for reproducibility +7. **Apply the exhaustive-path-tracing protocol selectively** to + **parser and decoder functions** that process untrusted structured input. + This protocol is not applied to every function — only to functions + identified during Phase 2 (attack surface enumeration) that meet + ALL of the following criteria: + + - The function **decodes multiple fields** from a wire format, file + format, or serialized structure controlled by an untrusted source + - The function **performs arithmetic** (subtraction, addition, + multiplication, shift) on two or more decoded values, or between + a decoded value and a running accumulator + - The function contains **loops** that iterate over a variable number + of decoded elements, where each iteration updates shared state + (offsets, remaining lengths, accumulators) + + For each such function, apply the full exhaustive-path-tracing + protocol with particular attention to: + + - **Inter-value arithmetic validation**: After decoding a new field + value, verify that every subsequent arithmetic operation using that + value against a running accumulator (e.g., `Largest -= Count`) is + guarded against underflow or overflow — not just at the decode site, + but at every use site within the function, including the *current* + loop iteration (not just the next iteration's entry check). + - **Loop-carried invariant gaps**: When a loop body decodes a fresh + value and uses it immediately, but the bounds check for that value + only runs at the *next* iteration's entry, the current iteration's + use is unguarded. Explicitly verify that each decoded value is + validated before its first arithmetic use within the same iteration. + - **Truncation after bounds check**: When a decoded uint64_t value + passes a bounds check against a uint16_t buffer length and is then + cast to uint16_t, the cast is safe. But when a decoded value is + used in arithmetic *without* a prior bounds check against the + current accumulator, the arithmetic may underflow even though the + decode itself succeeded. + ## Non-Goals Explicitly define what is OUT OF SCOPE for this security audit. @@ -111,10 +148,19 @@ Before beginning analysis, produce a concrete step-by-step plan: data enters the system. 2. **Enumerate attack surface**: List every input handling path, authentication point, and privilege transition. -3. **Classify**: Apply the security-vulnerability protocol systematically +3. **Identify parser/decoder functions for deep analysis**: From the + attack surface enumeration, identify functions that decode multiple + fields from untrusted structured input and perform inter-value + arithmetic (see instruction 7). List these functions explicitly — + they will receive exhaustive path tracing. +4. **Classify**: Apply the security-vulnerability protocol systematically to each attack surface element. -4. **Rank**: Order findings by exploitability and impact. -5. **Report**: Produce the output according to the specified format. +5. **Deep-dive**: Apply the exhaustive-path-tracing protocol to each + function identified in step 3. For each, trace every arithmetic + operation on decoded values through every loop iteration and + verify underflow/overflow guards exist at every use site. +6. **Rank**: Order findings by exploitability and impact. +7. **Report**: Produce the output according to the specified format. ## Quality Checklist @@ -128,3 +174,6 @@ Before finalizing, verify: - [ ] At least 3 findings have been re-verified against the source - [ ] Coverage statement documents what was and was not examined - [ ] No fabricated vulnerabilities — unknowns marked with [UNKNOWN] +- [ ] All parser/decoder functions identified in step 3 have coverage + ledgers from exhaustive-path-tracing (or explicit justification + for skipping)