FerroProve - C-to-Rust lifter emitting #![forbid(unsafe_code)] crates with a differential oracle

Дата публикации: 17-10-2026 18:08:59

FerroProve



FerroProve — Deterministic C-to-Safe-Rust Lifter (#![forbid(unsafe_code)])
Zero unsafe in src/lib.rs. Byte-exact on valid inputs, deterministic containment (-100) on out-of-bounds reads/writes. Paste any GitHub .c URL.






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):
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.
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

Схожие новости

#	Наименование новости	Тональность	Информативность	Дата публикации
1	Creusot 0.14.0 - Contracts for Rust, formally proved	0	8.83	13-10-2026
2	[Project] sol: A self-contained browser kernel written in Rust	0	9.76	18-10-2026
3	My state lib PurrGress	0	12.62	13-08-2026
4	Sping 1.5.5 — a cross-platform network diagnostics CLI written in Rust	0	9.19	10-10-2026
5	I built an unsafe scanner alternative to Cargo Geiger	0	8.82	09-10-2026
6	Multi_bimap - many-to-many bimap freely made of two arbitrary maps	0	13.1	16-10-2026
7	Hotcode: easy to use hot-reload	0	9.84	09-10-2026
8	Multicalc: Scientific computing for real-time embedded systems in no_std Rust	0	14.36	10-08-2026
9	[Show] taetype: Pure Rust font engine with zero unsafe code	0	10.19	27-07-2026
10	Mettle 0.17.0	0	24.52	03-09-2026

Классификация: . Схожих патентов: 0. Схожих новостей: 10. Тональность: 0. Информативность: 15.51. Источник: users.rust-lang.org.