GHSA-mfh5-3c8f-975p

Summary

Two independent root causes let the logic engines produce a VERIFIED verdict that does not follow from the input.

Root cause 1 — Python boolean operators on Z3 objects (`LogicVerifier`)

src/qwed_new/core/safe_evaluator.py allows ast.BoolOp (and/or), ast.UnaryOp(Not) and multi-operator ast.Compare. With Z3 objects, Python evaluates these with bool() / structural == instead of building a Z3 formula, so the constraint changes silently:

Call	Result	Correct
`prove_theorem({"x":"Int"}, [], "not (x == 5)")`	VERIFIED "Theorem proved by contradiction"	BLOCKED (counterexample x=5)
`check_equivalence({"x":"Int"}, "x == 1 and x == 2", "x == 1")`	VERIFIED	BLOCKED (not equivalent)
`verify_logic({"x":"Int"}, ["not (x == 1)", "x == 1"])`	VERIFIED (SAT)	UNVERIFIABLE (UNSAT)
same with `Not(...)` / `And(...)` (control)	correct	—

Inputs using or or chained comparisons raise and fail closed (BLOCKED). The false VERIFIED outcome is specific to and / not.

Reachable from: the LogicVerifier public Python API, and ConsensusVerifier._verify_with_logic (constraints produced by an LLM).

Root cause 2 — DSL compiler auto-creates variables from any string atom (`DSLLogicVerifier`, `/verify/logic`)

src/qwed_new/core/dsl/compiler.py L129-134: every str node that is not a declared variable becomes Int(node), including quoted literals.

DSL	Result	Correct
`(AND (EQ color 1) (EQ color 2))` (control)	UNSAT	—
`(AND (EQ color "red") (EQ color "blue"))`	SAT, model `color=0, "red"=0, "blue"=0`	UNSAT or BLOCKED

/verify/logic (src/qwed_new/api/main.py ~L541) maps SAT to DiagnosticResult.verified(...).

Note: the compiler half of root cause 2 was identified earlier in a related public issue, but the fix at that time changed only logic_verifier.py.

Impact

Downstream components (Finance, Tax, Legal, MCP, A2A, etc.) that gate actions on a logic VERIFIED verdict can admit claims that are false. No code execution is involved. This is an integrity violation of the core verification contract ("VERIFIED must follow from the evidence").

Patches

SafeEvaluator._validate_ast: reject ast.BoolOp, ast.UnaryOp with ast.Not, and ast.Compare with more than one operator (or rewrite them to And/Or/Not explicitly).
Z3Compiler._compile_expr: reject undeclared identifiers and quoted string atoms with a BLOCKED-mapped compile error. Do not auto-create variables.
Regression tests: every row above must not produce VERIFIED.

Workarounds

Use only And(...), Or(...), Not(...) in LogicVerifier constraints and avoid quoted literals in DSL. Treat logic VERIFIED verdicts on untrusted input as advisory until upgrading.