docs(invariants): add programmability screening methodology and canar… - #6
Merged
Merged
Conversation
…y results Introduce a project-level screening framework in invariants/README.md so each mechanism's invariant survey can separate "checker-worthy" rows from explicitly-excluded ones using the same four dimensions (observability, decisiveness, cost, static/dynamic category). Apply the framework to stack-canary.md, listing 10 invariants that pass and 18 that are excluded with reasons pointing back to specific dimensions.
Reviewer's GuideIntroduces a shared project-level methodology for determining which documented invariants are suitable for automated checking, and applies it to the stack-canary invariants by adding a new section that classifies each invariant as checker-worthy or explicitly excluded with reasons tied to the four screening dimensions. Flow diagram for invariant programmability screening methodologyflowchart TD
A[Invariant from survey] --> B[Evaluate observability]
B --> C[Evaluate decisiveness]
C --> D[Evaluate implementation_cost]
D --> E[Determine static_vs_dynamic category]
E --> F{Any dimension severely inadequate?}
F -- Yes --> G[Classify as excluded_invariant]
G --> H[Record 排除理由 referencing specific dimension]
F -- No --> I[Classify as checker_worthy_invariant]
I --> J[Record 通过理由 referencing dimensions]
J --> K[Emit entry under stack_canary 可程序化 invariants]
H --> K
File-Level Changes
Tips and commandsInteracting with Sourcery
Customizing Your ExperienceAccess your dashboard to:
Getting Help
|
added 2 commits
May 28, 2026 13:18
Rewrite stack-canary.md and invariants/README.md as pure research artifacts. Remove project-specific coupling that crept in: - drop oracle_mapping field; replace with observation describing the phenomenon rather than how DeFuzz detects it - drop all references to checker file paths, seed templates, exit code conventions, sentinel markers, and DREV identifiers - delete the §10 "DeFuzz Canary Oracle 映射总表" and §12 usage advice — these are implementation docs, not invariants research - rewrite INV-SP-R03 entry around the observable phenomenon (guard residue in callee-saved register at function return) instead of the EpilogueCanaryScrubChecker probe protocol Verify versions against current upstream: - GCC 16.1 (released 2026-04-30) confirmed for stack_protect_* predicates in cfgexpand.cc - -fhardened meta-flag list re-checked against GCC 14+ docs - add S/390 follow-up note for GCC 16.1 backend coverage Drop "正控/负控" jargon throughout in favor of plain language.
Restrict stack-canary.md and the cross-mechanism source survey to invariants whose violation results in silent bypass: the defense appears to run, no trap fires, but control-data is overwritten or the guard is predictable. Items whose violation only causes mechanism strengthening, compile-time errors, or link-time errors are removed. stack-canary.md: - New unified threat model: silent bypass. - Drop heuristic-detail/flag-precondition/attribute/runtime-contract/ guard-source/non-bypass register-convention invariants (E01-E03, F02-F03, X01-X02, A01-A03, G01-G04, R01-R02, H01-H02 details). - Retain and reframe: L01 (canary between vulnerable locals and saved regs/retaddr), L02 (VLA/alloca on stack-low side, CVE-2023-4039), L03 (multiple vulnerable objects share canary protection face). - Add L04 (protector slot must not be reallocated after locals; CERT VU#129209 / LLVM D64759). - Add V01 (epilogue compares guard value, not address; GCC 9 Cortex-M4 bug). - Add V02 (__stack_chk_fail must be noreturn). - Add S01 (guard value/address must not spill to attacker-writable stack; GCC PR 85434, LLVM D64759). - Add S02 (epilogue must clobber registers holding canary; GCC PR 96191 + meta-bug 125045). - Keep H01 only as the documentation-level guarantee that VLA/alloca functions are always instrumented (its violation is whole-function silent bypass). - Add a "Known silent-bypass cases" table mapping CVE-2023-4039, CERT VU#129209, GCC 9 Cortex-M4 codegen bug, GCC PR 85434, GCC PR 96191 + 125045 to the invariants they violate. gcc-llvm-defense-invariant-source-survey.md: - Retitle and rescope to silent-bypass perspective; explicitly state the threat model. - Restate the implicit-constraint bullet list to highlight silent-failure paths (layout, verification logic, secrecy, dedicated registers, ELF notes, runtime contracts, byte-pattern constraints). - Replace the verification anchor table with known silent-bypass cases (CVE-2023-4039, CERT VU#129209, GCC PR 85434, GCC PR 96191 + 125045, GCC 9 Cortex-M4 codegen, _FORTIFY_SOURCE degradation, IBT byte collision, missing CET ELF note, SCS x86_64 removal, Clang CFI -flto/-fvisibility prerequisites). - Rewrite the usage-recommendation section to drop project coupling (DeFuzz, oracle_mapping) and align with the README field convention. Evidence verified by web search and source review for each new invariant (CVE-2023-4039 patch series, CERT VU#129209 advisory, LLVM D64759, GCC PR 85434 / 96191 / 125045, GCC 9 Cortex-M4 bug report).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
…y results
Introduce a project-level screening framework in invariants/README.md so each mechanism's invariant survey can separate "checker-worthy" rows from explicitly-excluded ones using the same four dimensions (observability, decisiveness, cost, static/dynamic category). Apply the framework to stack-canary.md, listing 10 invariants that pass and 18 that are excluded with reasons pointing back to specific dimensions.
Summary by Sourcery
Define a shared project-level methodology for screening invariants for programmability and apply it to the stack canary invariant survey, classifying which invariants are checker-worthy and which are explicitly excluded with reasons.
Documentation: