Twitter/X

modelvet is a freestanding C11 library + CLI (pip install modelvet) that…

2026-08-04 · 13:40 UTC ·@tetsuoai ·2 min read

Brief

modelvet is a conservative C11 library and CLI that pre-validates GGUF and safetensors files for structural safety before any model loader parses bytes. The author demonstrates a real exploit: a 65‑byte GGUF that triggers a SIGFPE crash in llama.cpp (exit 136) via a division-by-zero from a [4,0] shape at ggml/src/gguf.cpp:685; modelvet instead rejects it with violation 304 (MVETVTENSORNERANGE) at offset 45. The project enforces no malloc/no recursion, pervasive checked arithmetic, loop bounds tied to compile-time caps, and a single caller buffer whose worst case is closed-form (fits inside 64 KiB for the CVE corpus). v0.1.0 (MIT) is tested against 18 advisory files, 249 GGUF and 68 safetensors differentials, and CI runs gcc/clang and sanitizers plus 32-bit and aarch64 qemu builds; acceptance is explicitly structural only.

Why it matters

modelvet is a freestanding C11 library + CLI (pip install modelvet) that validates GGUF and safetensors files structurally before a loader touches bytes; CLI exit codes: 0 accept, 1 reject, 2 no verdict; v0.1.0 MIT, signed reproducible tarball (github/tetsuo-ai/modelvet).

Key details

  • A crafted 65‑byte GGUF crashes llama.cpp on x86‑64 with SIGFPE (exit 136) due to a division-by-zero from shape [4,0] at ggml/src/gguf.cpp:685; modelvet rejects that input as violation 304 (MVET_V_TENSOR_NE_RANGE) at offset 45 and exits 1.
  • Design constraints: no malloc, no recursion; every integer derived from file bytes is checked with bounded arithmetic; loop bounds map to validated fields with compile-time caps; working memory is a single caller-provided buffer whose worst case is closed-form and the entire CVE corpus verifies inside 64 KiB.
  • Testing and hardening: corpus of 18 historical-advisory files (each must be rejected with the exact violation code); differential testing: 249 GGUF inputs vs llama.cpp and 68 safetensors vs the canonical Rust crate with all divergences triaged (no cases where modelvet accepts what upstream rejects); CI uses -Wall -Wextra -Werror -Wconversion -Wshadow, gcc/clang, ASan/UBSan/MSan, 32-bit and aarch64 under qemu.
Source evidence

modelvet is a freestanding C11 library that checks whether a GGUF or safetensors file is structurally safe to parse, before your loader touches the bytes.

pip install modelvet

The 65-byte GGUF in the video kills the real llama.cpp loader on x86-64: SIGFPE, exit 136. modelvet rejects the same bytes: violation 304, MVETVTENSORNERANGE, offset 45, exit 1.

modelvet has rejected that shape since its first version, I read llama.cpp's guard and refused to mirror it. It bounds tensor dimensions at ggml/src/gguf.cpp:685 with a check that divides by one of them:

INT64_MAX / info .t. ne[1] <= info .t. ne[0]

ne[1] comes straight from the file. The validation loop above it rejects negative dimensions and never zero, so shape [4, 0] divides INT64MAX by zero inside ggufinitfromfile and the process is gone before it reads a single weight. Floating point exception (core dumped). On aarch64 the divide returns 0 instead of trapping, so parsing continues with a garbage element count. Reproduced against a Release build of ggml-base, still on master, already filed and open as llama.cpp issue #26366 with the hardening PR open too.

I don't think this is one project's mistake. llama.cpp in C++, ollama in Go, and MLX in C++ each wrote their own GGUF parser and each shipped the same class of integer overflow. The 2025 fix (CVE-2025-53630) got bypassed in 2026 (CVE-2026-27940) because the patch checked every addition into the size accumulator and never the combined total. general.alignment has the same shape: 2^31 accepted straight from the file into padding and seek arithmetic, upper-bound fix PR open since June.

So modelvet is paranoid by construction. No malloc, no recursion. Every integer derived from file bytes goes through checked arithmetic, even where a raw add is provably safe, because the uniformity is what makes it auditable. Every loop bound traces to a validated field checked against a named compile-time cap. Working memory is one caller-provided buffer whose worst case is closed-form in those caps, and the entire CVE corpus verifies inside 64 KiB of it. Malformed input is a normal result: verdict, violation code, byte offset, two detail values. Clean under -Wall -Wextra -Werror -Wconversion -Wshadow. CI runs gcc and clang, ASan, UBSan, MSan, 32-bit, and aarch64 under qemu.

That corpus is 18 files, one per historical advisory. Each must be rejected with its exact violation code or the build fails. Rejecting for the wrong reason also fails, because that means the invariant that kills that advisory stopped working. Differential runs: 249 GGUF inputs through modelvet and the real llama.cpp loader, 68 safetensors inputs through the canonical Rust crate at the commit modelvet was written against, every divergence triaged. No input where modelvet accepts what upstream rejects. The 6 remaining safetensors divergences are deliberate policy, like rejecting duplicate JSON keys.

An ACCEPT verdict is structural only. It says nothing about model behavior, poisoned weights, tokenizer contents, or provenance, and pickle stays out of scope because pickle executes.

v0.1.0, MIT, signed reproducible tarball. Vendor the two generated files (modelvet.c and modelvet.h), or run the CLI, where the exit code is the verdict: 0 accept, 1 reject, 2 no verdict.

github/tetsuo-ai/modelvet

Video