←back to thread

Compiling C to Safe Rust, Formalized

(arxiv.org)
278 points love2read | 1 comments | 20 Dec 24 23:30 UTC | HN request time: 0s | source
Show context
nickpsecurity ◴[21 Dec 24 04:15 UTC] No.42477506[source]▶
The thing I wonder about is why we would do this. The technology to really convert industrial-grade apps from C to Rust could probably bullet proof the C apps more easily. They’d just have to do some analyses that fed into existing tooling, like static analyzers and test generators.

Similarly, it they might generate safe wrappers that let teams write new code in Rust side by side with the field-proven C. New code has the full benefits, old code is proven safe, and the interfaces are safer.

A full on translator might be an ideal option. We’d want one language for the codebase in the future. Push-button safety with low, false positives for existing C and C++ is still the greatest need, though. Maybe auto-correcting bad structure right in the C, too, like Google’s compiler tool and ForAllSecure’s Mayhem do.

replies(1): >>42478166 #
DonaldPShimoda ◴[21 Dec 24 08:05 UTC] No.42478166[source]▶
> The technology to really convert industrial-grade apps from C to Rust could probably bullet proof the C apps more easily.

No, some C programs cannot be made safe. This can be due to dependency on undefined or unspecified behaviors, or it can be because introducing proper safety checks would limit the domain of possible inputs too much to be useful, or other things.

Translating to a safe language can maintain the expressive capabilities of the inputs while statically guaranteeing correct operation at run-time. It is objectively better in these cases.

> field-proven C

I don't think this exists, as the numerous critical vulnerabilities over the years have shown. All we have is C that seems to work pretty well often enough to be useful.

> old code is proven safe

Old code is assumed to be safe due to luck, actually. "Prove" has a specific meaning (especially on a post for a paper about proving things), and the overwhelming majority of C code is not proven to any rigorous mathematical standard. In contrast, the Rust type system has been mathematically proven to be correct.

> A full on translator might be an ideal option.

It depends on what you're willing to give up. If you don't mind losing performance, limiting your domain of inputs or range of outputs, giving up code legibility, and so on, then sure, this can probably be done to some extent. But when you start wanting your translator to be both sound and complete over all of these concerns, you run into problems.

replies(3): >>42479119 #>>42479253 #>>42480752 #
1. nickpsecurity ◴[21 Dec 24 17:01 UTC] No.42480752[source]▶
There’s tools that prove the safety of C code. They include RV-Match, Astree Analzer, and Frama-C. CompCert certifies the compilation. There’s tons of tools to find bugs by model checking, test generation, etc. Rust was nowhere near C last I checked in terms of tooling available.

So, back to my original comment, the investment in making a Rust to C transpiler would make a C to safer C transpiler that fed that code into the verification tooling. A small transpiler would be easier to write with huge, immediate gains.

On field proven, there’s two angles: spec and code. Many C/C++ apps didn’t become usable at all until years of iteration based on feedback from field use. An alternative in Rust might have incorrect specs which. From there, a number have had much code review, static analysis, and testing. They have few to no known bugs at any point. So, there are definitely C/C++ applications out there that are field-proven with a decent level of safety.

(Note: Any transpiler might need to be bug for bug and weird behavior for weird behavior compatible to match the implicit spec in the C/C++ code.)

You’re right about the average Rust vs C code, like type system vs correctness. I’d prefer new code be written in safer languages, which I added to my proposal.

If apples to apples on correctness, you’d have to compare C written for verification with Rust. Quite a few C projects have been proven to be correct. Since you’re using a compiler, I’ll add that tools like Softbound+CETS make C code safe automatically.

I do think Rust brings the cost and effort down quite a lot, though. It’s tooling is usually more mature or at least free than most for verifying C.