DSLLogicVerifier NL->DSL bridge returns VERIFIED for contradictory or altered constraints (incomplete fix of GHSA-mfh5-3c8f-975p)

Impact

On POST /verify/logic, the natural-language-to-DSL bridge _constant_to_dsl strips quotes from string constants and rewrites them into bare tokens, which the DSL compiler then auto-creates as integer variables. As a result the logic engine returns status=VERIFIED, is_authoritative=True with a proof_ref, for claims that do not hold:

• Contradictory categorical rules (for example tier == 'gold' and tier == 'silver') come back SAT/VERIFIED, because the two distinct strings both become the same auto-created integer variable.
• Distinct string constants that normalise to the same token, or numeric-looking strings coerced to integers, collapse the same way.

The published fix for GHSA-mfh5-3c8f-975p rejects string literals at the direct-DSL sink, but the NL bridge reaches the compiler through a path that fix never covered, so the same class of false VERIFIED is reachable again.

Note: admission_decision returns BLOCKED for these (logic VERIFIED results carry no is_valid=True), so a consumer gating strictly on the admission decision is not affected. The exposed surface is the authoritative VERIFIED verdict, its proof_ref, and the audit record (is_verified=true).

Affected

All releases through 7.2.3; reproduced at the verdict level on main @ a4d6714 (deterministic, post-translation — the LLM step is not involved in the repro).

Details

• src/qwed_new/core/dsl_logic_verifier.py _constant_to_dsl (around 402-404): re.sub(r"\W+", "_", value) emits a bare token.
• src/qwed_new/core/dsl/compiler.py (around 161-168): the quote-guard only fires on tokens that still carry quotes; everything else auto-creates an Int.
• A routing test currently asserts the mangling as expected behaviour (tests/test_dsl_logic_verifier_routing.py), and evals/cases/logic.json has no string-constant cases.

Fix

Reject string constants in _constant_to_dsl (fail closed to UNVERIFIABLE) rather than coercing them to integer variables, so the GHSA-mfh5 quote-guard covers the NL bridge too; update the routing test that locks in the mangling; and add string-constant cases to the logic eval. Tracked as an incomplete fix of GHSA-mfh5-3c8f-975p.

Source

OpenVuln external audit (2026-10), NL->DSL logic bridge findings. Reported privately.