modelvet threat model

Adversary

The attacker fully controls every byte of the model file. The file may arrive from a hub download, a user upload, or an untrusted local path. Parsing a field does not make it trusted: range, alignment, overflow, and cross-field checks must all succeed before the field can govern later work.

Obligations

While processing any input, the library:

• never reads or writes out of bounds. Every read is checked against the input buffer. Writes are limited to the caller's arena, report, and explicit output parameters;
• never recurses and never loops over an unvalidated hostile count. Iteration is bounded by named compile-time caps;
• never allocates. Working memory comes from one caller-owned fixed arena with an exact closed-form worst-case bound;
• checks overflow-capable arithmetic before using file-derived sizes, counts, offsets, alignment, or tensor geometry;
• treats hostile input as normal operation. A malformed file returns MVET_OK with a REJECT verdict. Status errors are reserved for API misuse and arena exhaustion.

Payload parsing is linear in the bytes examined. Duplicate-key and duplicate-tensor-name detection uses deterministic, iterative heapsort and takes O(k log k + t log t) bounded comparisons for k keys and t tensors. Each comparison is itself bounded by the configured key or name length cap. This avoids hash-flooding and quadratic scans while making the non-linear work explicit.

Verdicts

• ACCEPT (structural). The file passed all implemented structural checks: header and counts, bounded strings, metadata types and values, unique keys and tensor names, tensor geometry and dtype, dense aligned layout, data extent, and the exact file boundary.
• REJECT. The first failed invariant is recorded with a stable violation code, byte offset, and two rule-specific detail values.

The report is fail-closed. It is cleared to a REJECT state before other public arguments are inspected, and remains rejected on API or arena errors.

Resource bounds

All hostile counts are checked against MVET_MAX_* constants before they control iteration or arena use. The GGUF verifier stores only two-word span indexes for keys and tensor names. MVET_GGUF_ARENA_WORST_BYTES exactly covers those indexes plus worst-case initial alignment padding for the configured caps. The arena high-water mark is exposed as mvet_arena_t.used.

What ACCEPT does not promise

• It does not assess model behavior. A structurally valid file may contain poisoned weights or architectural backdoors.
• It does not assess tokenizer contents or semantic payloads.
• It does not establish provenance or byte integrity. A signing scheme is complementary: signing identifies bytes; modelvet checks their structure.
• Pickle and PyTorch zip payloads are outside the parser boundary.
• It is not a sandbox. ACCEPT removes a class of parser-level hazards before a loader runs; it cannot prevent independent bugs in that loader.
• It does not promise parity with every loader's extra policy. modelvet has deliberate strictness, including unique names, canonical booleans, dense tensor offsets, and no trailing bytes.