fix: add falsification discipline to security audit template

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
 

protocols/analysis/security-vulnerability.md

@@ -48,6 +48,25 @@ 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 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
 

protocols/guardrails/self-verification.md

@@ -36,6 +36,14 @@ 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. 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
 

protocols/reasoning/exhaustive-path-tracing.md

@@ -11,6 +11,7 @@ description: >
 applicable_to:
   - review-code
   - investigate-bug
+  - investigate-security
   - exhaustive-bug-hunt
 ---
 

templates/investigate-security.md

@@ -12,7 +12,9 @@ protocols:
   - guardrails/anti-hallucination
   - guardrails/self-verification
   - 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
@@ -88,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.
@@ -110,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
 
@@ -127,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)