From 086e76261b4be1cbf21053c3f3f12a437ba9ffbe Mon Sep 17 00:00:00 2001 From: Sam Blake Date: Tue, 1 Sep 2026 17:16:31 +1000 Subject: [PATCH] fix(graph): fvc_search self-protects its FVC_MAX_VERTICES stack buffers Closes the RG-2 adversarial finding #2. fvc_search is exported in graph.h and its inner fvc_bb uses stack arrays seen[]/forbid[] sized to FVC_MAX_VERTICES (128). The cap was enforced only in the head builtin_find_vertex_coloring, not in fvc_search, and FVC_MAX_VERTICES is not visible in graph.h -- so a cross-TU caller passing n > 128 could not discover the precondition and would overflow those buffers. fvc_search now refuses (return 0) when n > FVC_MAX_VERTICES, locating the invariant with the buffers it guards. No behaviour change on the head path, which already filters n > 128 before calling in. Regression: a direct fvc_search on CompleteGraph[129] must return 0 with zero steps (test_vertex_coloring_internals). Without the guard it returns 129 via the lb >= ub short-circuit, so the assertion genuinely fails when the guard is absent. Verified: default build clean; graph_tests green (17 tests); make check-c99 and make check-packed-aware pass. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_018GNB6E1ftx4TkAk47VfkNJ --- docs/spec/changelog/2026-08-31.md | 14 ++++++++++++++ src/graph/vertexcoloring.c | 6 +++++- tests/test_graph.c | 17 +++++++++++++++++ 3 files changed, 36 insertions(+), 1 deletion(-) diff --git a/docs/spec/changelog/2026-08-31.md b/docs/spec/changelog/2026-08-31.md index 03b360c8..30d7402c 100644 --- a/docs/spec/changelog/2026-08-31.md +++ b/docs/spec/changelog/2026-08-31.md @@ -1,5 +1,19 @@ # Changelog: week of 2026-08-31 (Mon) – 2026-09-06 (Sun) +## FindVertexColoring — exported search self-protects its stack buffers (RG-2 #2) + +`fvc_search` (exported in `src/graph/graph.h`) drives a branch-and-bound whose +inner `fvc_bb` uses stack arrays `seen[]`/`forbid[]` sized to `FVC_MAX_VERTICES` +(128). The 128-vertex cap was enforced only in the head +`builtin_find_vertex_coloring`, not in `fvc_search` — and because the symbol is +exported while `FVC_MAX_VERTICES` is not, a cross-TU caller passing a larger +graph could not discover the precondition and would overflow those buffers. +`fvc_search` now refuses (`return 0`) when `n > FVC_MAX_VERTICES`, putting the +invariant with the buffers it protects. No behaviour change on the head path, +which already filters `n > 128`. Closes the RG-2 adversarial finding #2. +Regression: a direct `fvc_search` on `CompleteGraph[129]` must return 0 with +zero steps (`test_vertex_coloring_internals`, `tests/test_graph.c`). + ## Build — `USE_MPFR=0` / `USE_LAPACK=0` config compiles cleanly again The `build-no-mpfr` CI job (`make USE_MPFR=0 USE_FLINT=0 USE_ECM=0 USE_LAPACK=0 diff --git a/src/graph/vertexcoloring.c b/src/graph/vertexcoloring.c index ba6999b0..ef25d5c9 100644 --- a/src/graph/vertexcoloring.c +++ b/src/graph/vertexcoloring.c @@ -317,7 +317,11 @@ static void fvc_bb(FvcBB* s, int ncoloured, int used) { int fvc_search(const GraphAdj* a, int* colour, long* steps_out) { int n = a->n; if (steps_out) *steps_out = 0; - if (n <= 0) return 0; + /* Self-protect: fvc_bb's seen[]/forbid[] are stack arrays sized to the cap + * (FVC_MAX_VERTICES + 2). The head enforces the cap before calling in, but + * this symbol is exported (graph.h) and FVC_MAX_VERTICES is not, so a + * cross-TU caller cannot see the precondition -- enforce it here too. */ + if (n <= 0 || n > FVC_MAX_VERTICES) return 0; int ub = fvc_dsatur_bound(a, colour); if (ub <= 0) return 0; /* allocation failure inside DSATUR */ diff --git a/tests/test_graph.c b/tests/test_graph.c index ebf43482..37b3823a 100644 --- a/tests/test_graph.c +++ b/tests/test_graph.c @@ -418,6 +418,23 @@ static void test_vertex_coloring_internals(void) { ASSERT_MSG(ub >= 3, "DSATUR on C5 cannot beat chi = 3"); free(c); graph_adj_free(a); expr_free(g); } + + /* Exported-symbol precondition (RG-2 adversarial finding #2). fvc_bb's + * seen[]/forbid[] are stack arrays sized to FVC_MAX_VERTICES, and the cap is + * enforced in the head -- not in fvc_search, which graph.h exports. A direct + * caller passing n > cap must be refused (0), never overflow the buffers. + * CompleteGraph[129] is one vertex over the cap and drives exactly that. */ + { + Expr* g = evaluate(parse_expression("CompleteGraph[129]")); + GraphAdj* a = graph_build_adj(g); + ASSERT(a != NULL && a->n == 129); + int* c = calloc((size_t)a->n, sizeof(int)); + steps = 999; + ASSERT_MSG(fvc_search(a, c, &steps) == 0, + "fvc_search must refuse n > FVC_MAX_VERTICES, not overflow"); + ASSERT_MSG(steps == 0, "a cap-refused search reports zero steps"); + free(c); graph_adj_free(a); expr_free(g); + } } /* ---- FindVertexColoring: the registered head (AC-1 .. AC-18) --------------