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..9c190bf 100644 --- a/protocols/analysis/security-vulnerability.md +++ b/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 diff --git a/protocols/guardrails/self-verification.md b/protocols/guardrails/self-verification.md index 3c94fbb..30f1829 100644 --- a/protocols/guardrails/self-verification.md +++ b/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 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 7926d07..cf57c3c 100644 --- a/templates/investigate-security.md +++ b/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)