docs(specs): WordPress flaw classes, the corpus insight, and an IR brief

Three directions recorded, each grounded in what this session measured.

**WordPress by flaw class, not by plugin** (tasks 5.8, 5.9). One plugin is
a checkout; a class is a claim. WordPress's recurring shapes are narrow and
each maps to a family that already exists -- unauthenticated wp_ajax_nopriv
reaching $wpdb, a missing capability check, unescaped output, arbitrary
file operations. Two of the four are blocked on gaps this session found:
access control cannot be asked at all because PHP has no obligation facts
(5.9), and unescaped output is blocked on the flat sanitizer list (5.6).
The observable is a class-by-class table across several plugins saying
found, missed, or out of scope -- a single found CVE is not the artifact
worth teaching from.

**Why a corpus of benchmarks is not enough on its own**, written into
overview.md as the finding it is rather than an opinion. Twelve engine
defects in one session against three real repositories, and the three gates
stayed byte-identical through every fix. A gate that does not move is a
corpus that could not see the bug. The reason is structural: a pair is a
labelled function with a declared family and a known answer, so it cannot
exercise which region to look at, what to spend, whether a capability is
reachable, whether two entry points share a sink, whether the question fits
in an argv slot, or whether a flow crosses a module. Three of the twelve
were quiet failures where the tool reported clean and every honesty counter
agreed -- which a benchmark score cannot express, because the score is
computed from the verdicts that exist. The corpus is the holdout that stops
per-repository tuning, and the wrong instrument for finding out whether the
tool works.

**ir-consolidation** (brief, unapproved) separates two questions the IR
suggestion contains, which have opposite answers. The SOURCE IR is already
carried rather than about to be added: semantic/ is 3218 lines, 16% of the
codebase, measured at 2.2% entailment against the CPG's 41.3% and still
running as a proposer -- and Vine and P-Code are binary IRs, so the work
there is subtraction. The MISSING abstraction is C arithmetic, and there
GhidraPAL's three-valued-logic abstract interpreter over Ghidra P-Code is
exactly the right shape: "can this index exceed this allocation" is a value
question, which is what a bit-level TVL domain answers and what every
libpng overflow needs. Vine is dormant since 2009 and is not the candidate.

The constraint is recorded as an ordering: question 1 lands before question
2 starts, or adopting an IR makes the growth problem worse. And the cost
that matters is not lines but the number of things that can silently return
nothing -- this session found three such in a single PHP scan, and a binary
pipeline adds a build, a lifter and a domain, each able to produce an empty
result that looks like a clean one.

Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>
Claude-Session: https://claude.ai/code/session_01T7XD7x5KonMdmGRkp63EQG
This commit is contained in:
Marius Ciepluch
2026-09-09 17:04:04 +02:00
co-authored by Claude Opus 5
parent 8579c10e7c
commit db273dde53
5 changed files with 169 additions and 0 deletions
+30
View File
@@ -493,6 +493,36 @@
- _Requirements: 4.4, 8.1, 9.1_
- _Depends: 5.1_
- [ ] 5.8 WordPress's popular flaw classes, on popular plugins
- > "in wp focus on some of their popular flaws and plugins. these are the keys to unlock practical
> software verification."
- One plugin is a checkout; a class is a claim. WordPress's recurring shapes are narrow and well
documented, and each maps to a family this engine already has:
- **Unauthenticated AJAX** — `wp_ajax_nopriv_*` reaching a `$wpdb` query. Declared-public plus injection,
both of which the mapper and the facts now carry.
- **Missing capability check** — a handler that acts without `current_user_can` / `check_admin_referer`.
This is the access_control family, and PHP has NO obligation facts yet, so it cannot be asked at all.
- **Unescaped output** — a stored option or meta value reaching `echo` without `esc_html`. Blocked on 5.6,
because the flat sanitizer list cannot say "escapes for HTML but not for SQL".
- **Arbitrary file operations** — a request value reaching `unlink`/`file_get_contents`. Facts exist.
- Pick plugins by installed base rather than by convenience, and pin each at a version with a verified
advisory the way `pmpro.toml` does -- the CVE read out of the code, not out of the advisory text.
- Observable: a class-by-class table over several plugins, saying for each whether it was found, missed, or
out of scope. That is the artifact worth teaching from; a single found CVE is not.
- _Requirements: 4.1, 4.4, 9.1_
- _Depends: 5.7_
- [ ] 5.9 PHP obligation facts, so access control can be asked at all
- `dominance_specs(language="php")` returns nothing: PHP has no obligated operations and no dischargers, so
the access-control family is silent on every WordPress scan rather than wrong on it.
- The vocabulary is small and conventional -- `current_user_can`, `check_admin_referer`, `wp_verify_nonce`,
`is_user_logged_in` as dischargers; `$wpdb` writes, `update_option`, `wp_delete_post`, `wp_update_user`
as obligated operations -- and it is the single largest missing WordPress flaw class.
- Do it after 5.6, so a discharge counts for the obligation it discharges rather than for all of them.
- Observable: a missing-capability finding on a plugin that has one, and silence on one that checks.
- _Requirements: 8.1, 9.1_
- _Depends: 5.6_
## Group 6 — Regression baselines
- [ ] 6.1 Repository baseline and delta