GHSA-2j4v-jw9r-f4gw: 
Python Schwachstellenanalyse und -minderung

Impact

dratify.parse_dimacs could read a clause out of a comment, so dratify could certify as unsatisfiable a file that every solver tested calls satisfiable. Before 0.1.11, a comment line ended at any Unicode line boundary, not only at a newline.

from dratify import parse_dimacs, check_proof
text = "p cnf 1 1\nc\x0cp cnf 1 2\n1 0\nc\x0c-1 0\n"
f = parse_dimacs(text, strict=True)
f.clauses                         # two clauses, (1) and (-1)
check_proof(f, "0\n").ok          # True before 0.1.11

Read a byte at a time, this file has one clause, (1), and setting variable 1 true satisfies it. minisat, CaDiCaL and kissat all answer SAT on it. dratify read the form feed as the end of the comment, then took the rest of the line as input: a second header, which replaced the first and so satisfied strict=True, and the clause (-1). The checker is right about the formula it was given. The fault is the distance between that formula and the file. The other separators behave the same way: \r, \x0b, \x1c, \x1d, \x1e, U+0085, U+2028 and U+2029. You are affected if you check proofs against DIMACS files you did not write, particularly where someone has reviewed the file or run a solver on it, and you use dratify's result as the certificate for that same file. Exploiting this takes control of the formula file; control of the proof alone is not enough. Not affected:

• Formulas built with CNF.add or read by anything other than dratify's parser.
• The Rust crate, which has no parser.
• Files using only \n or \r\n line endings, with no such character inside a comment. A hidden line in a proof is less serious: parse_proof shared the cause, but a hidden addition is still checked, so it obtains nothing that writing it openly would not.

Patches

Fixed in dratify 0.1.11, on PyPI. A line now ends at \n, with one trailing \r removed, in formulas and proofs alike. Characters inside a comment stay in the comment. The same release also tightens the parser:

• A second header raises ValueError, with or without strict.
• A header is exactly four tokens, and the first is p.
• Tokens are separated by ASCII whitespace and integers are -?[0-9]+, so 1_0, +1, Unicode digits and a no-break space raise.
• CR-only files raise. Some files that used to parse now raise, which is the intended direction: rejecting them is safer than guessing what they mean.

parse_dimacs_file reads the bytes as they are. Path.read_text() does not: its universal newlines turn a stray \r into a line break before any parser sees it, so use parse_dimacs_file on a file you do not trust.

Workarounds

Upgrade. Otherwise, read the file as bytes and refuse any that contains a non-ASCII byte, a byte below 0x20 other than \t, \n and \r, or a \r that is not followed by \n.

References

• Fix: https://github.com/carlok/dratify/commit/260d1ad
• Release notes: https://github.com/carlok/dratify/blob/main/CHANGELOG.md#0111--2026-11-09