Hostile Artifact Hardening, Fuzzing, Differential Testing, And Formal Invariants

Full report

On this page

1. Executive Hardening Strategy and Assumptions

The ingestion, validation, and execution of externally provided machine learning artifacts represent a critical security frontier, characterized by extreme input complexity and vast attack surfaces. The architecture of TinyRustLM demands an implementation-grade parser hardening strategy rooted in the principles of Language-Theoretic Security (LangSec)1. The LangSec paradigm posits that software accepting untrusted input must treat that input as a formal language, implementing a mathematically sound recognizer whose behavior matches a precise specification2. Ad-hoc parsing logic inevitably creates "weird machines"—unintended computational environments that attackers can manipulate by submitting inputs that exploit parser ambiguities3. TinyRustLM operates under a strict zero-trust assumption regarding input provenance. Artifacts sourced from local storage, peer-to-peer (P2P) exchanges, browser boundaries via WebAssembly (WASM) and JavaScript (JS) Application Binary Interfaces (ABI), and external model catalogs are categorically treated as hostile. Because the Rust runtime and packer enforce a zero third-party crate policy for production execution, the project cannot rely on battle-tested community parsers such as nom1 or serde\_json6. Custom parsing logic must be engineered from first principles, demanding rigorous formal validation. The architectural strategy strictly prohibits permissive recovery; ambiguous bytes, structurally invalid states, or trailing data must result in a deterministic, fail-atomic rejection without modifying the system's last-known-good state. Furthermore, because Rust's standard library allocator defaults to process abortion upon memory exhaustion, the parsers must calculate, verify, and reserve all memory bounds before large allocations occur8. Utilizing patterns akin to the experimental try\_reserve enables the application to gracefully handle allocation limits without invoking catastrophic panics or aborts10. All exposed diagnostics must remain privacy-safe, leaking no user prompts, token streams, local paths, or underlying memory structures. Raw input bytes must never be echoed back in error messages, as this introduces secondary vulnerabilities such as cross-site scripting (XSS) in browser contexts or log-injection attacks3. The resulting defensive posture guarantees that validation is strictly bounded before any large allocation, hardware activation, or execution takes place.

2. Attack-Surface and Trust-Boundary Matrix

The trust boundary for TinyRustLM is drawn at the absolute perimeter of the application. No byte enters the validation phase with any implicit trust, regardless of its origin. The following matrix details the primary attack surfaces, the nature of the artifacts processed, the trust boundary classification, and the specific security objectives required to neutralize potential threats.

Each parser interacting with these boundaries must adhere to strict type safety and memory safety guarantees. A network destination injection, for instance, must be prevented by ensuring that canonical interpretation of routing metadata does not allow the overriding of internal P2P routing tables. The objective is to achieve a canonical interpretation of every artifact, eliminating parser differentials across different components of the system.

3. Universal Bounded-Reader and Checked-Arithmetic Contract

To safely parse complex .slm binaries and associated hierarchical metadata without relying on third-party libraries, TinyRustLM must implement a custom Universal Bounded-Reader pattern. This architecture replaces unbounded std::io::Read loops with a strictly constrained, zero-copy memory-slice state machine. The reader operates exclusively on a zero-copy byte slice, maintaining an internal cursor that tracks the exact position within the buffer. It enforces a strict "no-holes" policy, ensuring every byte is sequentially indexed and semantically validated. This policy explicitly prevents the creation of polyglot files—a vulnerability class where an artifact is valid in multiple formats simultaneously (e.g., a valid tensor model that is also a malicious ZIP archive or executable script)21. By mandating that all bytes are accounted for, attackers cannot interleave malicious payloads into unused padding or hidden segments22. The Universal Bounded-Reader contract requires several critical mechanisms. Exact consumption must be enforced; methods designed to read data must strictly advance the cursor by the requested length. If an over-read is attempted, the reader must return a deterministic UnexpectedEof domain-specific error code without triggering a runtime panic. To defend against stack-exhaustion attacks commonly seen in naive JSON or grammar parsers, a monotonically decreasing maximum nesting depth counter must be passed through all recursive calls6. If this depth counter reaches zero, the parser immediately halts, neutralizing deeply nested array or map bombs7. Furthermore, a total work budget must be integrated to prevent CPU exhaustion via algorithmic complexity attacks, such as overlapping offset decompression bombs or infinite recursive references. This budget decrements on every loop iteration or significant parsing operation. The reader must also enforce a trailing-byte policy: upon completion of parsing, the cursor must match the exact length of the input buffer. Any unparsed trailing bytes immediately invalidate the artifact, preventing appended malicious payloads. Finally, memory allocation must be managed through an explicit reservation system, checking requested sizes against a predefined total allocation budget before utilizing safe, fallible allocation primitives to avoid standard library aborts.

4. Parser Phases and Fail-Atomic State Invariants

Parser execution within TinyRustLM must be explicitly stratified into rigid, sequential phases. No operation in a subsequent phase may commence until the preceding phase completes with absolute success. This stratification is paramount for maintaining fail-atomic state invariants, ensuring that a malformed artifact cannot leave the system in a partially initialized or corrupted state. The first phase is the Bounded Structural Preflight. During this phase, the parser verifies magic bytes, extracts the header, and checks for polyglot padding. It executes arithmetic invariant checks on all file offsets, tensor dimensions, and chunk ranges. Crucially, this phase is strictly read-only. It may read the input slice and cache lightweight structural metadata (e.g., offset tables), but it is expressly forbidden from allocating large memory buffers, decompressing data, or mutating any global system state. Following the structural preflight is the Semantic Validation phase. Here, the extracted metadata is evaluated against logical system limits and canonical rules. Model hyperparameters are scrutinized to ensure they fall within supported bounds—for example, verifying that context window sizes are non-zero, that quantization parameters match the declared tensor types, and that no unhandled NaN (Not-a-Number) values exist in critical configuration fields where they are disallowed21. The third phase involves Hashing and Allocation. Cryptographic hashes of the parsed artifact are computed and verified against trusted signatures or receipts. Only after cryptographic provenance and structural integrity are guaranteed does the system proceed to allocation. Memory is reserved using the limits validated in the first phase. The final phases involve Decompression (if applicable) and Activation. The model is transferred into its execution state, such as being uploaded to GPU memory via WebGPU or mapped into WASM linear memory. Throughout all phases, candidate validation is entirely isolated from active model state. If a parse or activation fails at any point, the operation is rolled back idempotently. The prior model remains exact and untainted, ensuring service continuity. Cleanup routines must guarantee the independent release of owned resources even after an earlier failure in the sequence.

5. Binary, Structured-Data, Network, Path, and Archive Mutation Taxonomies

To adequately harden the parsers, the engineering architecture requires comprehensive mutation taxonomies. These taxonomies categorize the specific malformations and adversarial payloads that the parsers must be explicitly designed to reject. The binary artifact mutation taxonomy focuses on .slm headers, tensors, and memory envelopes. Attack vectors include arbitrary bit flips, byte insertions, and deletions designed to misalign parsers. Truncation at every possible byte offset must be tested to ensure graceful EOF handling. Attackers may attempt to provide duplicate tables or overlapping tensor byte ranges, violating memory isolation21. Boundary integers must be mutated to edge cases (0, 1, u32::MAX, u64::MAX). Dimensions containing a zero or a one must be carefully handled to avoid division-by-zero errors or infinite loops in optimized mathematical kernels21. Extreme dimensions, invalid quantization tails, checksum swaps, and polyglot prefixes/suffixes22 must all result in structural rejection. Furthermore, the taxonomy must include internally consistent but malicious allocation bombs—files that are mathematically sound but demand physically impossible amounts of memory25. The structured-data mutation taxonomy addresses JSON, canonical metadata, and grammar schemas. The parser must reject duplicate keys, which can lead to canonicalization collisions or signature wrapping attacks. Alternate Unicode normalizations and invalid UTF-8 sequences must be sanitized or rejected. Deep arrays and maps require depth-limit enforcement to prevent stack overflows6. Long numbers, exponent extremes (e.g., 1e-2147483647), and unexpected NaN encodings can trigger underlying integer overflows in conversion libraries6. Unknown fields, missing fields, type confusion (e.g., parsing an integer as a string), and key reordering must be handled deterministically without inducing panics. Network parser tests must target HTTP requests, WebSocket frames, and P2P messages. Ambiguous Content-Length and Transfer-Encoding headers are the root cause of HTTP request smuggling; RFC 9112 dictates that Transfer-Encoding overrides Content-Length, but proxy disagreements allow attackers to smuggle payloads13. The taxonomy includes duplicate headers, oversized headers, prohibited obs-fold continuations, absolute-form paths, and malicious percent encoding. WebSocket fragmentation attacks, compressed frame bombs, slowloris byte-drip attacks, and pipelined connection reuse anomalies must be systematically modeled and rejected. Path and archive defenses are critical for native import and package consumption. The taxonomy here covers directory traversal utilizing .., absolute paths, drive-relative paths, and Windows Universal Naming Convention (UNC) paths. Archive extraction must defend against Alternate Data Streams (ADS), reserved device names (e.g., CON, PRN), Unicode separators designed to bypass simple string matching, and the deployment of symlinks, junctions, or hard links to escape the extraction sandbox. Extraction races (Time-of-Check to Time-of-Use, TOCTOU) must be mitigated, ensuring destination containment after canonical path resolution12.

6. Property-Based Generators, Metamorphic Tests, and Shrink Design

Property-based testing is mandated to verify that the parsers respect global invariants across millions of generated inputs. Rather than relying solely on hardcoded fixtures, generators must be implemented to produce both syntactically valid artifacts and invalid, near-valid corruptions. This approach ensures high coverage of the parser's state machine without binding the runtime to a specific test library dependency. Valid artifact generators build .slm files, metadata, and network frames that adhere strictly to the specification, ensuring the parser correctly accepts all permutations of legitimate data. Invalid near-valid generators construct artifacts that are structurally sound but semantically flawed (e.g., a tensor descriptor pointing exactly one byte past the end of the file), forcing the parser to exercise its error-handling paths. The test suites will assert specific metamorphic and structural properties. The round-trip property dictates that serializing a parsed artifact must result in an identical in-memory representation: parse(serialize(x)) \== x. The canonicalization property ensures that syntactically distinct but semantically equivalent representations map to the same deterministic hash: hash(serialize(parse(x))) \== hash(serialize(parse(y))). Resource-bound assertions must continuously monitor memory and CPU usage, mathematically proving that memory\_allocated(parse(generator(size))) \< limit(size). When a property test fails, the test framework must employ advanced shrink strategies. The generator must automatically shrink the failing payload by aggressively zeroing out tensor dimensions, truncating metadata strings, flattening nested JSON structures, and simplifying Unicode sequences. This isolation process strips away unrelated complexity, presenting the developer with the minimal exact byte sequence that violates the invariant, significantly accelerating debugging and patch development.

7. Coverage-Guided Fuzz Target Matrix and Corpus Strategy

Coverage-guided fuzzing translates mutated byte streams into exercised execution paths, serving as the primary automated discovery mechanism for memory corruption and logic flaws. Utilizing tools such as cargo-fuzz (libFuzzer) and AFL-family fuzzers28, the architecture requires a dedicated, pure, and resettable entry point for every parser and state transition. Fuzz targets must execute in complete isolation. They must operate without network access, persistent global state, real physical model execution, or the presence of secret credentials. This deterministic isolation ensures that any crash is infinitely reproducible.

The corpus strategy requires seeding the fuzzers with highly structured dictionaries and an initial corpus of both valid .slm files and known historical exploits (e.g., payloads mimicking the llama.cpp or hyper CVEs). Structure-aware fuzzing can be achieved by utilizing custom mutators that generate artifacts conforming loosely to the .slm specification, ensuring the fuzzer spends CPU cycles testing semantic logic rather than being continually rejected by the initial structural preflight28.

8. Differential Testing and Disagreement Adjudication

Parser differential testing involves cross-verifying the custom TinyRustLM parser against secondary implementations to identify semantic deviations. In the context of Language-Theoretic Security, a parser differential is not a mere curiosity; it is a critical vulnerability waiting to be exploited1. If two implementations parse the same artifact into different state representations, an attacker can leverage this ambiguity to bypass validation in one component while executing a malicious payload in another1. Differential vectors within TinyRustLM must be expansive. The architecture requires comparing independent scalar mathematical kernels against SIMD-optimized kernels to ensure identical tensor evaluations. The native Rust .slm parser must be run in lockstep against the WebAssembly compiled parser; any deviation implies an architecture-specific bug, such as a 32-bit truncation error in WASM that does not manifest in 64-bit native code. The source tokenizer must be differentially tested against the newly implemented Rust tokenizer to ensure identical token IDs are generated for complex Unicode inputs. Furthermore, the custom HTTP parser must be evaluated against standard HTTP compliance test suites (e.g., h2spec or similar HTTP/1.1 suites) to identify smuggling vulnerabilities. Archive validation must be differentially tested across Windows (which features case-folding and Alternate Data Streams) and Linux filesystems to ensure extraction logic is universally contained. Disagreement adjudication is strict: a differential disagreement is a bug to resolve, not a majority vote. When a differential is discovered, the grammar definition must be tightened, and the ambiguous byte sequence must be deterministically rejected by all implementations, closing the exploitation window.

9. Formal-Method, Typestate, and Concurrency Recommendations

Empirical testing, while powerful, cannot prove the absence of flaws. For the highest-value invariants within TinyRustLM—specifically the Universal Bounded-Reader and the Arithmetic Invariant Library—formal verification techniques must be employed. The Kani Rust Verifier, built upon the CBMC bit-precise verification engine, enables bounded model checking of Rust code31. Kani translates Rust's Mid-level Intermediate Representation (MIR) into logic formulas, utilizing SAT/SMT solvers to mathematically prove that certain conditions hold for all possible inputs up to a specified bound33. Proof harnesses must be written for the parser's arithmetic core, allowing Kani to verify the complete absence of undefined behavior, array out-of-bounds accesses, division by zero, and unhandled panics35. While exhaustive tests on small domains are useful, Kani provides rigorous mathematical assurance that no combination of bytes can force the cursor past the slice boundary. Typestate programming provides a compile-time enforcement mechanism for the parser phases. By encoding the state of an artifact into the Rust type system, the architecture guarantees valid transitions. A RawArtifact can only be transitioned to a StructurallyValidArtifact by passing through the preflight function. Functions requiring semantic validation will strictly accept the SemanticallyValidArtifact type. This linear capability model prevents developers from accidentally bypassing security checks by calling internal methods out of order. Concurrency and asynchronous execution introduce severe race conditions, particularly in worker message ordering, model activation commits, and cache replacements. Two P2P lanes fetching shards of the same .slm model must not corrupt shared memory. The Loom concurrency testing tool must be employed to exhaustively permute all possible thread interleavings for state-machine transitions. This ensures that cancellations are idempotent, receipt appends are atomic, and service shutdowns perform safe cleanup regardless of the thread scheduling order.

10. Native Sanitizer, Miri, Browser, WASM, and WebGPU Test Matrix

Execution environments for TinyRustLM span native hardware, WebAssembly sandboxes, and GPU pipelines. Each environment requires specialized dynamic analysis and hardening tests. In native environments, the continuous integration pipeline must execute the fuzz corpora through a suite of LLVM sanitizers. AddressSanitizer (ASan) is required to detect use-after-free errors, heap buffer overflows, and memory leaks. UndefinedBehaviorSanitizer (UBSan) will catch unaligned pointers, integer overflows, and invalid boolean states. ThreadSanitizer (TSan) must run against the concurrent P2P and worker modules to detect data races. Additionally, the Miri interpreter will execute the test suite to guarantee that no aliasing violations or Stacked Borrows rules are breached, ensuring the complete absence of undefined behavior in any safe or approved unsafe blocks. The browser and WebAssembly environments introduce unique limitations. WebAssembly linear memory is rigidly capped at 4GB (65536 pages in wasm32)36. The parser must actively predict and track memory footprints. If a .slm artifact demands 4.1GB, the system must cleanly reject it during the semantic validation phase. Relying on memory.grow to fail will trigger a hard WASM trap, terminating the application abruptly without allowing cleanup routines to execute37. The WASM sandbox does not excuse application-level denial of service or cross-tab data leakage. Hardening tests for the WASM/JS ABI boundary must simulate malformed host pointers, out-of-bounds lengths, stale handles, and detached array views. WebGPU integration requires strict validation. When uploading tensors, the application must utilize WebGPU's pushErrorScope to capture asynchronous validation errors, such as buffer size mismatches or out-of-bounds shader reads39. A failure inside the GPU pipeline must be caught and mapped gracefully to a deterministic TinyRustLM state cancellation, destroying the pipeline object cleanly rather than causing a catastrophic device loss event or browser process restart.

11. Resource Controls, Timeout, Isolation, and Privacy-Safe Evidence

To defend against denial-of-service attacks targeting resource exhaustion, all parsing and validation routines must be strictly governed by resource controls. The total work budget implemented in the Universal Bounded-Reader addresses algorithmic complexity, but physical time limits must also be enforced. All parsers must be wrapped in strict timeout monitors to mitigate slowloris-style byte-drip attacks over network connections. In native environments across Windows, Linux, and arm64 architectures, child processes executing model inference must be contained. Operating system-level constructs, such as Linux cgroups or Windows Job Objects, must be utilized to enforce hard physical memory limits and CPU quotas, ensuring that a runaway model cannot destabilize the host system. When a failure occurs, the generation of evidence and diagnostic logs must be strictly privacy-safe. Raw input bytes, user prompts, generated tokens, credentials, and unknown remote names must be explicitly scrubbed from crash reports. A malicious artifact might embed a user's local file paths or PII within a corrupted metadata field; exposing this field in a public error log constitutes an information leak. Error diagnostics must log only the structural nature of the failure (e.g., "Tensor dimension overflow at offset 0x4A00") and the cryptographic hash of the artifact, keeping sensitive context entirely quarantined.

12. Crash Triage, Immutable Regression, and Disclosure Workflow

The lifecycle of a discovered vulnerability, whether found via fuzzing, differential testing, or dynamic analysis, must follow a rigorous, immutable triage and disclosure workflow. When a crash is detected, the exact identity of the failure is captured. This includes the tool identity, the cryptographic hash of the target artifact, the random seed that triggered the path, the duration of the run, the sanitizer mode active, and the bounded stack signature of the fault. The payload is then subjected to a privacy-safe minimization process. Automated test-case reducers strip away non-essential bytes, preserving only the precise structural corruption that triggered the flaw. The hash of this minimized input is permanently added to the regression corpus, guaranteeing that the specific boundary violation is tested in all future builds. Remediation must be narrow and decisive. Permissive recovery is strictly banned; if a state is invalid, the fix must ensure swift, deterministic rejection. Following the fix, all invalidated phases of the test suite must be rerun. Reproducible vulnerabilities must be accurately classified—for example, differentiating between Resource Exhaustion, Numerical Mismatch, Parser Ambiguity, or a Harness Defect. Public disclosure of the vulnerability is authorized separately and must refer exclusively to the hash identity of the artifact and the abstract nature of the boundary violation. The actual malicious bytes and exploit chains are kept out of public reports to prevent weaponization before the ecosystem has patched.

13. CI Scheduling and Cross-Platform Evidence

The continuous integration (CI) scheduling must reflect the diverse deployment environments of TinyRustLM. Parser logic, particularly path sanitization and archive extraction, behaves differently depending on the underlying operating system. The CI pipeline must schedule cross-platform evidence collection across Linux, Windows, and macOS, spanning both x86\_64 and arm64 architectures. Archive validation tests must verify that directory traversal defenses hold up against Windows case-folding and Linux case-sensitivity. Fuzzing operations, which are highly CPU-intensive, must be scheduled intelligently. Short-duration fuzzing runs execute on every pull request to catch shallow regressions, while deep, continuous fuzzing campaigns run asynchronously on dedicated infrastructure, continuously mutating the corpus and exploring complex state transitions. Deterministic schedules are required where tools permit, ensuring that a race condition caught by Loom or TSan on a Monday can be perfectly reproduced by a developer on a Tuesday.

14. Universal Checked-Arithmetic Contract and llama.cpp Case Analysis

To fully appreciate the necessity of the checked-arithmetic contract within the parser phases, one must analyze recent critical vulnerabilities in the wider machine learning ecosystem. The GGUF format parsing in llama.cpp suffered from catastrophic Remote Code Execution (RCE) vulnerabilities (CVE-2026-33298 and CVE-2026-27940) directly attributable to integer overflows25. In these exploits, crafted files contained malicious tensor dimensions. The C/C++ parser calculated the required memory size by multiplying tensor elements and strides: roughly [Figure omitted from source export]25. Because these variables were controlled by the untrusted file, an attacker could supply dimensions that, when multiplied, wrapped around the maximum value of a 64-bit integer25. The math overflowed, resulting in a drastically undersized heap allocation (e.g., 4MB) for a tensor that logically required exabytes of data25. When the parser subsequently attempted to read the file data into this undersized buffer, it caused a massive out-of-bounds write, corrupting the heap and enabling arbitrary code execution25. TinyRustLM's arithmetic invariant library prevents this exact class of memory corruption. Standard unchecked operators (+, \*) must be globally forbidden in parser modules via compiler lints. The library must enforce proof obligations using checked\_mul and checked\_add for all file offsets, tensor element counts, dimensions, strides, block counts, and padding limits. If any calculation overflows u64::MAX, the operation yields an immutable error, rejecting the artifact before allocation is even attempted. Furthermore, architecture width transitions require extreme scrutiny. If a .slm file specifies a 6GB tensor, native 64-bit Rust can represent this in a usize. However, when compiled to WebAssembly, usize is 32-bit. A naive u64 to usize downcast (e.g., tensor\_size as usize) will truncate the 6GB value, wrapping it modulo [Figure omitted from source export], creating the exact undersized buffer condition seen in the GGUF exploits26. The invariant library must safely reject values exceeding usize::MAX on the target architecture prior to casting.

15. TDD Backlog, Coverage Gates, and Clean Deletion Rules

The implementation of this hardening process must follow a strict, staged Test-Driven Development (TDD) plan. Security cannot be bolted on after the parser is written; it must drive the architecture.

1. Phase 1: Primitives and Proofs. Begin by implementing the checked arithmetic library and the pure bounded-reader primitives. Write Kani proof harnesses to guarantee they cannot panic or access memory out of bounds.

2. Phase 2: Property Tests and Single-Field Corruptions. Implement the phase-separated parsers. Assert property tests against the mutation taxonomy, verifying that deep nesting or single-byte corruptions are immediately rejected without altering global state.

3. Phase 3: Fuzzing and Dynamic Analysis. Stand up cargo-fuzz targets for binary, network, and structured data endpoints. Integrate ASan, UBSan, and Miri into the CI pipeline.

4. Phase 4: Concurrency and Browser Validation. Validate WASM OPFS locks using Web Locks API stress tests18. Test WebGPU pushErrorScope cancellations in headless browser environments39.

5. Phase 5: Quarantine and Real Artifacts. Test the parsers against real, complex artifacts, but keep them quarantined from production execution until all coverage gates (e.g., 95% branch coverage on parser modules) are met.

A rigid clean-deletion rule must be enforced throughout this lifecycle: any legacy, permissive parsing paths intended for unpublished, deprecated, or "compatibility" artifact formats must be completely expunged from the codebase. Unused or permissive code is unverified code, and in a zero-trust execution environment, unverified code represents a critical, lingering vulnerability.

16. Annotated Primary-Source Bibliography

This hardening strategy synthesizes current, primary-source security research, vulnerability disclosures, and architectural constraints. The following annotated bibliography details the core literature that shaped these engineering requirements, providing evidentiary backing for the prescribed defenses.

• Language-Theoretic Security (LangSec) and Parser Differentials: Research by Bratus, Patterson, and the LangSec community1 establishes the foundation of the bounded-reader pattern. The literature dictates that parsing untrusted input is a formal language recognition problem. Parser differentials—where two components interpret the same data differently (e.g., HTTP smuggling)—are identified as the root cause of widespread exploitation1.
• Integer Overflows in ML Formats (CVE-2026-33298, CVE-2026-27940): The llama.cpp GGUF vulnerabilities definitively prove that machine learning models are active attack vectors. Advisory reports detail how unchecked multiplication of tensor dimensions leads to integer wraparound, resulting in undersized heap allocations and Remote Code Execution via out-of-bounds writes25. This literature mandates the creation of the Checked-Arithmetic Contract and architecture-aware width transitions.
• HTTP Request Smuggling and hyper Vulnerabilities (CVE-2021-21299, CVE-2021-32714): Security advisories for the Rust hyper crate demonstrate how modern, memory-safe languages can still suffer from logical parser failures13. Failure to properly enforce RFC 9112 Section 6.3 regarding ambiguous Transfer-Encoding and oversized chunk headers allows attackers to desynchronize proxies13. This necessitates the strict network parser tests and the rejection of all ambiguous HTTP states.
• Structured Data and serde\_json Stack Overflows: Vulnerability databases track instances where deep JSON nesting or floating-point exponent extremes (e.g., 3.5E-2147483647) trigger stack overflows or panics in robust libraries like serde\_json6. This directly informs the requirement for monotonically decreasing maximum nesting counters and bounded total work budgets.
• Model Polyglots and the safetensors Specification: Academic research into Pickle deserialization RCE and polyglot files demonstrates that attackers can interleave malicious scripts within standard model formats22. The safetensors format specification mitigates this by enforcing a "no-holes" policy, ensuring all bytes are indexed and offsets do not overlap21. TinyRustLM adopts this exact defense to prevent polyglot artifact execution.
• WASM Linear Memory Limits and OPFS Concurrency: WebAssembly architectural documentation confirms that wasm32 linear memory is strictly bounded to 65536 pages (4GB)36. Exceeding this limit causes a hard trap. Furthermore, documentation on the Origin Private File System (OPFS) highlights the need for the Web Locks API to prevent data corruption during concurrent worker access17.
• Formal Verification via the Kani Rust Verifier: Technical documentation, tutorials, and academic case studies on Kani illustrate its capability to translate Rust MIR into bit-precise CBMC logic31. Its successful deployment in verifying the Rust standard library and the Firecracker VM validates its inclusion in this report as the primary tool for mathematically proving the absence of panics and out-of-bounds accesses in the parser boundaries.

Works cited

1. Language-Theoretic Security \- Wikipedia, https://en.wikipedia.org/wiki/Language-Theoretic\_Security

2. Object-centric Tracing for Language-Theoretic Security in Low-Level Interfaces, https://langsec.org/spw26/papers/palmer-object-tracing.pdf

3. Secure Input Handling \- Institute for Computing and Information Sciences, https://www.cs.ru.nl/\~erikpoll/papers/secure\_input\_handling.pdf

4. LangSec, http://langsec.org/

5. nom 1.0 is here\! REJOICE\! \- Clever Cloud, https://www.clever.cloud/blog/engineering/2015/11/16/nom-1-0/

6. Vulnerabilites collected today, Saturday 4/7 \- Meterian: Daily Vulnerabilities, https://meterian.io/vulns/?id=92f38818-0c1a-3ca3-b4cb-e6f3e355451d\&date=2026/05/07

7. mysql 14.2.0 \- Deps.rs, https://deps.rs/crate/mysql/14.2.0

8. rust/library/alloc/src/alloc.rs at main · rust-lang/rust \- GitHub, https://github.com/rust-lang/rust/blob/master/library/alloc/src/alloc.rs

9. Lecture 3 \- Software Systems \- Computer and Embedded Systems Engineering, https://cese.ewi.tudelft.nl/software-systems/part-1/lecture-notes/lecture-3.html

10. How to handle memory allocation failure? : r/rust \- Reddit, https://www.reddit.com/r/rust/comments/i4zvte/how\_to\_handle\_memory\_allocation\_failure/

11. alloc.rs \- source, https://doc.rust-lang.org/src/std/alloc.rs.html

12. strict-path \- Lib.rs, https://lib.rs/crates/strict-path

13. CVE-2021-21299 Detail \- NVD, https://nvd.nist.gov/vuln/detail/CVE-2021-21299

14. GHSA-5H46-H7HH-C6X9 \- Vulnerability-Lookup, https://vulnerability.circl.lu/vuln/ghsa-5h46-h7hh-c6x9

15. HTTP Request Smuggling: From RFC to Real-World Impact \- SecQuest, https://www.secquest.co.uk/white-papers/http-request-smuggling

16. CVE-2021-32715: Vulnerability in hyper package \- Lenient header parsing of Content-Length could allow request smuggling \- Vulert, https://vulert.com/vuln-db/crates-io-hyper-1059

17. File System API \- MDN Web Docs, https://developer.mozilla.org/en-US/docs/Web/API/File\_System\_API

18. Gatewatcher/hoddor \- GitHub, https://github.com/Gatewatcher/hoddor

19. The origin private file system : r/javascript \- Reddit, https://www.reddit.com/r/javascript/comments/1d6r42b/the\_origin\_private\_file\_system/

20. Resource Exhaustion via Unchecked File | Orbis AppSec, https://orbisappsec.com/blog/resource-exhaustion-via-unchecked-file-imports-how-missing-limits-create-dos-vulnerabilities

21. GitHub \- safetensors/safetensors: Simple, safe way to store and distribute tensors, https://github.com/safetensors/safetensors

22. Paged Out\! \#7, https://pagedout.institute/download/PagedOut\_007.pdf

23. MLFiles: Using Input-Handling Bugs to Inject Backdoors Into Machine Learning Pipelines, https://repository.gatech.edu/bitstreams/c678f4b3-dc3b-4e14-a5a0-81c4fc2b57d1/download

24. SafePickle: Robust and Generic ML Detection of Malicious Pickle-based ML Models \- arXiv, https://arxiv.org/pdf/2602.19818

25. Heap Buffer Overflow via Integer Overflow in GGUF Tensor Parsing · Advisory · ggml-org/llama.cpp \- GitHub, https://github.com/ggml-org/llama.cpp/security/advisories/GHSA-96jg-mvhq-q7q7

26. Integer Overflow in GGUF Parser can lead to Heap Out-of-Bounds Read/Write in gguf, https://github.com/ggml-org/llama.cpp/security/advisories/GHSA-vgg9-87g3-85w8

27. Security considerations for the ASP.NET Core Kestrel web server, https://learn.microsoft.com/en-us/aspnet/core/fundamentals/servers/kestrel/security-considerations?view=aspnetcore-10.0

28. Support custom mutators · Issue \#170 · rust-fuzz/cargo-fuzz \- GitHub, https://github.com/rust-fuzz/cargo-fuzz/issues/170

29. libafl — Claude Code skill · Trail of Bits, https://trailofbits.com/skills/libafl/

30. Reversed arbitrary · Issue \#44 · rust-fuzz/arbitrary \- GitHub, https://github.com/rust-fuzz/arbitrary/issues/44

31. GitHub \- model-checking/kani: Kani Rust Verifier, https://github.com/model-checking/kani

32. Comparison with other tools \- The Kani Rust Verifier, https://model-checking.github.io/kani/tool-comparison.html

33. Can somebody explain how Kani verifier works? \- The Rust Programming Language Forum, https://users.rust-lang.org/t/can-somebody-explain-how-kani-verifier-works/113918

34. Kani: A Model Checker for Rust \- arXiv, https://arxiv.org/html/2607.01504v1

35. Using the Kani Rust Verifier on a Rust Standard Library CVE, https://model-checking.github.io/kani-verifier-blog/2022/06/01/using-the-kani-rust-verifier-on-a-rust-standard-library-cve.html

36. Can either wasmer or wasmtime handle 1M concurrent wasm modules switching every 1 microsecond? \- The Rust Programming Language Forum, https://users.rust-lang.org/t/can-either-wasmer-or-wasmtime-handle-1m-concurrent-wasm-modules-switching-every-1-microsecond/100017

37. catvec/alligator-wasm-alloc: Real-time memory allocator built for WebAssembly, written in Rust. \- GitHub, https://github.com/Noah-Huppert/alligator-wasm-alloc

38. How to set max memory limit in wasm \- Rust Users Forum, https://users.rust-lang.org/t/how-to-set-max-memory-limit-in-wasm/64725

39. wgpu package \- github.com/gogpu/wgpu \- Go Packages, https://pkg.go.dev/github.com/gogpu/wgpu@v0.30.22

40. WebGPU Explained: The Browser's New Graphics and Compute Engine \- DEV Community, https://dev.to/biomathcode/webgpu-explained-the-browsers-new-graphics-and-compute-engine-1cld

41. CVE-2026-33298 \- Red Hat Customer Portal, https://access.redhat.com/security/cve/cve-2026-33298

42. Malicious GGUF File RCE: llama.cpp Parser Flaws 2026 \- Stingrai, https://www.stingrai.io/blog/malicious-gguf-file-llama-cpp-parser-rce

43. CVE-2026-33298: llama.cpp Integer Overflow RCE Vulnerability \- SentinelOne, https://www.sentinelone.com/vulnerability-database/cve-2026-33298/

44. CVE-2021-32714 Detail \- NVD, https://nvd.nist.gov/vuln/detail/CVE-2021-32714

45. HTTP Request Smuggling in hyper · CVE-2021-21299 · GitHub Advisory Database, https://github.com/advisories/GHSA-6hfq-h8hq-87mf

46. SafePickle: Robust and Generic ML Detection of Malicious Pickle-based ML Models \- arXiv, https://arxiv.org/html/2602.19818v1

47. Scaling multithreaded WebAssembly applications with mimalloc and WasmFS | Articles, https://web.dev/articles/scaling-multithreaded-webassembly-applications