Validate FlatZinc constraint arity before indexing arguments (heap OOB read)

[evilgensec]

Problem

The FlatZinc front end accepts a constraint <name>(<args>) declaration with any number
of arguments; the parser performs no arity check (parser.yy stores the argument vector
verbatim). Both consumers that dispatch on the constraint name then read fixed positions of
constraint.arguments:

• the CP-SAT extractor CpModelProtoWithMapping::FillConstraint (cp_model_fz_solver.cc),
  invoked for every constraint on every solve, e.g. BoolNeConstraint reads arguments[0]
  and arguments[1], IntLinEqConstraint reads arguments[2].values[0];
• the solution checker CheckSolution (checker.cc), e.g. CheckBoolNot reads
  arguments[1].

Neither validates arguments.size() first. A hand-crafted .fzn that declares a known
constraint with too few arguments drives arguments[k] past the end of the heap-allocated
std::vector<fz::Argument>, an out-of-bounds read. The attacker chooses the constraint
type and therefore which fixed offset is read past the end; deeper handlers dereference the
out-of-bounds Argument's pointer/list members. .fzn is untrusted input for
fzn-ortools (constraint-solving services, CI, MiniZinc backends).

Reproduced with AddressSanitizer through the real ParseFlatzincString + CheckSolution:

var bool: x :: output_var;
constraint bool_not(x);   // bool_not takes 2 arguments; one given
solve satisfy;

==..==ERROR: AddressSanitizer: heap-buffer-overflow ... READ of size 4
  #0 ...Eval(...) checker.cc:41
  #1 ...CheckBoolNot(...) checker.cc:374
  #2 ...CheckSolution(...) checker.cc:1921
0x.. is located 0 bytes after a 104-byte region allocated in orfz_parse (parser.yy)

Fix

Add NumRequiredArguments(absl::string_view type) (in model.{h,cc}): a table of the
minimum number of arguments each constraint type needs, derived from the fixed argument
positions read by the checker and extractor handlers (the max literal arguments[k] index

• 1; FlatZinc constraints have a fixed per-type arity, so requiring it never rejects a
  well-formed model). Unknown types return 0 (no restriction). Both CheckSolution and
  FillConstraint reject a constraint with fewer arguments before dispatching.

With this change the crafted model above no longer reads out of bounds: the checker reports
the constraint as unsatisfied (CheckSolution returns false, ASAN clean), and the
extractor errors out instead of indexing past the vector.

The arity table is generated from the current handler set; the FlatZinc regression suite in
CI exercises the well-formed paths to confirm no valid model is rejected.

[lperron]

This is just a tad over-engineered.
Just check the arity without lookup at the start of each check method.

This being said, creating the fzn file should be done by the minizinc compiler, so they should not generate invalid fzn files

[evilgensec]

Thanks, simplified. Each Check* method now verifies its own argument count at the start and returns unsatisfied if a constraint has too few arguments, so there is no central table to keep in sync. Dropped the NumRequiredArguments table and the CheckSolution dispatch check; net reduction in code.

Agreed a correct MiniZinc compiler should not emit invalid .fzn. The guard is defense-in-depth for the standalone case: the solver/checker can be pointed at any .fzn (hand-written, third-party, or from another tool), where today a too-short constraint is an out-of-bounds read rather than a clean rejection.

One open point: the CP-SAT extractor (FillConstraint and the per-type methods) also indexes arguments directly, and I dropped its guard along with the table. If you would prefer the loader to fail gracefully on a malformed .fzn, I can add the same per-method checks there; otherwise I will leave it relying on the parser. Which do you prefer?

[lperron]

Please a DCHECK_EQ() in the FillConstraint code. It should have been caught before Laurent Perron | Operations Research | ***@***.*** | (33) 1 42 68 53 00 Le jeu. 18 juin 2026 à 12:01, evilgensec ***@***.***> a écrit :

…

*evilgensec* left a comment (google/or-tools#5228) <#5228 (comment)> Thanks, simplified. Each Check* method now verifies its own argument count at the start and returns unsatisfied if a constraint has too few arguments, so there is no central table to keep in sync. Dropped the NumRequiredArguments table and the CheckSolution dispatch check; net reduction in code. Agreed a correct MiniZinc compiler should not emit invalid .fzn. The guard is defense-in-depth for the standalone case: the solver/checker can be pointed at any .fzn (hand-written, third-party, or from another tool), where today a too-short constraint is an out-of-bounds read rather than a clean rejection. One open point: the CP-SAT extractor (FillConstraint and the per-type methods) also indexes arguments directly, and I dropped its guard along with the table. If you would prefer the loader to fail gracefully on a malformed .fzn, I can add the same per-method checks there; otherwise I will leave it relying on the parser. Which do you prefer? — Reply to this email directly, view it on GitHub <#5228?email_source=notifications&email_token=ACUPL3M3QKFA6ABF32BXSHL5AO4VXA5CNFSNUABFM5UWIORPF5TWS5BNNB2WEL2JONZXKZKDN5WW2ZLOOQXTINZUGA3TQNBQHA4KM4TFMFZW63VHMNXW23LFNZ2KKZLWMVXHJLDGN5XXIZLSL5RWY2LDNM#issuecomment-4740784088>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACUPL3MOMBMTOGOT4CIEMT35AO4VXAVCNFSNUABEKJSXA33TNF2G64TZHMZTCMJQGIYDSMR3JFZXG5LFHM2DMNZZGUYTANJZGGQXMAQ> . Triage notifications, keep track of coding agent tasks and review pull requests on the go with GitHub Mobile for iOS <https://github.com/notifications/mobile/ios/ACUPL3NG4JZUBZ5PWHBXXI35AO4VXA5CNFSNUABFM5UWIORPF5TWS5BNNB2WEL2JONZXKZKDN5WW2ZLOOQXTINZUGA3TQNBQHA4KM4TFMFZW63VHMNXW23LFNZ2KKZLWMVXHJKTGN5XXIZLSL5UW64Y> and Android <https://github.com/notifications/mobile/android/ACUPL3O3JTXJNQDW6SIG54L5AO4VXA5CNFSNUABFM5UWIORPF5TWS5BNNB2WEL2JONZXKZKDN5WW2ZLOOQXTINZUGA3TQNBQHA4KM4TFMFZW63VHMNXW23LFNZ2KKZLWMVXHJLTGN5XXIZLSL5QW4ZDSN5UWI>. Download it today! You are receiving this because you commented.Message ID: ***@***.***>

[evilgensec]

Done. Added a DCHECK at the start of each extractor method that indexes arguments, asserting the arity it needs before reading, rather than a single check in FillConstraint since the dispatch is generic and has no per-type arity now that the table is gone. Used DCHECK_GE on the minimum each method indexes so it stays a debug-only invariant and will not trip on constraints that carry extra arguments. Happy to switch to DCHECK_EQ on exact arity if you prefer.