I built FerroProve to lift small C modules like parsers, checksums, byte-level helpers and more into crates that compile under #![forbid(unsafe_code)], with a separate extern "C" shim (ffi.rs) and .h header so existing C callers can link without changes.

c2rust transpile preserves raw pointer arithmetic inside unsafe, so an out of bounds read in C stays an out-of-bounds read in Rust. An LLM rewrite avoids unsafe but can change behavior on signed promotions or off by one inputs.

FerroProve pairs the lift with a differential check (what i mean is):

  1. Each vector runs under legacy C indexing semantics and against the lifted slice-based crate. Valid inputs must match byte-for-byte; an out-of-bounds C read or write must come back as -100 in the safe crate.
  2. The emitted crate is compiled with rustc --edition 2021 -D warnings with #![forbid(unsafe_code)] on lib.rs.

The top bar takes a GitHub .c URL. Nine upstream files are pre-wired as presets:

  • DaveGamble/cJSON v1.0.0 cJSON.c (parse_hex4, CVE-2016-4303 over-read on a truncated \u escape)
  • torvalds/linux v6.8 lib/crc8.c
  • madler/zlib v1.3.1 adler32.c
  • redis/redis 7.2 src/crc16.c
  • gcc-mirror/gcc libiberty/crc32.c
  • esmil/musl src/stdlib/atoi.c
  • openbsd/src lib/libc/string/timingsafe_bcmp.c
  • git/git v2.30.0 hex.c (hex_to_bytes)
  • jedisct1/libsodium 1.0.19 sodium/utils.c (sodium_memcmp)

Constructs outside the supported subset (goto, **, heap allocation) are rejected with a line number rather than falling back to unsafe.

If you have a small C function that breaks it or produces an awkward ffi.rs signature, I'd like to see it.

1 post - 1 participant

Read full topic