Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Compiling C to Safe Rust, Formalized

arxiv.org

Post reply on HN
Print view View original

31–40 of 173 posts

Re: Compiling C to Safe Rust, Formalized

#31

Post by quuxplusone »

orf wrote: post #23
pizlonator wrote: post #19

Earlier quoted context omitted.

Rust’s ownership model forbids things like doubly linked lists, which C programs use a lot. That’s just one example of how C code is nowhere near meeting Rust’s requirements. There are lots of others.

> Rust’s ownership model forbids things like doubly linked lists, which C programs use a lot. It’s literally in the standard library https://doc.rust-lang.org/std/collections/struct.LinkedList....

But it's not in C's standard library. So the exercise isn't merely to auto-translate one language's standard library to another language's standard library (say, replacing C++ std::list with Rust LinkedList) — which would already be very hard. The exercise here is to auto-identify-and-refactor idioms open-coded in one language, into idioms suited for the other language's already-written standard library.

Imagine refactoring your average C program to use GLib for all (all!) of its data structures. Now imagine doing that, but also translating it into Rust at the same time.

Re: Compiling C to Safe Rust, Formalized

#32

Post by nickpsecurity »

tonetegeatinst wrote: post #30
wffurr wrote: post #6

Note that this is done for “existing formally verified C codebases” which is a lot different from typical systems C code which is not formally verified.

What is the main difference? Can compiler flags force compliance?

Formal verification often requires simplified code in a restrictive style. You might not even be able to use C features or structures that have the performance you want. How theorem provers and brains work are also different enough that making something easy for one often makes it harder for the other.

You can also see this effect in the article on the history of Coverity’s analyzer. Real-world code was horrible to deal with vs the academic examples they started with.

https://cacm.acm.org/research/a-few-billion-lines-of-code-la...

Re: Compiling C to Safe Rust, Formalized

#33

Post by andrewflnr »

orf wrote: post #28
singron wrote: post #27

Earlier quoted context omitted.

This implementation uses unsafe. You can write a linked list in safe rust (e.g. using Rc), but it probably wouldn't resemble the one you write in C. In practice, a little unsafe is usually fine. I only bring it up since the article is about translating to safe rust.

Safe rust isn’t “rust code with absolutely 0 unsafe blocks in any possible code path, ever”. Rc uses unsafe code every time you construct one, for example. Unsafe blocks are an escape hatch where you promise that some invariants the compiler cannot verify are in fact true. If the translated code were to use that collection, via its safe interfaces, it would still be “safe rust”. More generally: it’s incorrect to say…

No one here is confused about what unsafe means. The point is, they're not implemented by following Rust's ownership model, because Rust's ownership model does in fact forbid that kind of thing.

You can nitpick the meaning of "forbids", but as far as the current context is concerned, if you translate code that implements a doubly linked list (as opposed to using one from a library) into Rust, it's not going to work without unsafe. Or an index-based graph or something.

Re: Compiling C to Safe Rust, Formalized

#34

Post by LPisGood »

tonetegeatinst wrote: post #30
wffurr wrote: post #6

Note that this is done for “existing formally verified C codebases” which is a lot different from typical systems C code which is not formally verified.

What is the main difference? Can compiler flags force compliance?

My understanding is that formal verification is a tough goal to achieve and that it usually requires designing the program or the language to be a specific way.

The problem with transpiling C to rust is that unsafe and unverified behavior can be a key property of the behavior resulting program, so there isn’t an obvious way to spit out a sort of rustified (CRustified?) binary that matches the behavior of the C program.

Re: Compiling C to Safe Rust, Formalized

#35

Post by jerf »

pornel wrote: post #17
pizlonator wrote: post #12

Compiling a tiny subset of C, that is. It might be so tiny as to be useless in practice. I have low hopes for this kind of approach; it’s sure to hit the limits of what’s possible with static analysis of C code. Also, choosing Rust as the target makes the problem unnecessarily hard because Rust’s ownership model is so foreign to how real C programs work.

Rust's ownership model is close enough for translating C. It's just more explicit and strongly typed, so the translation needs to figure out what a more free-form C code is trying to do, and map that to Rust's idioms. For example, C's buffers obviously have lengths, but in C the length isn't explicitly tied to a pointer, so the translator has to deduce how the C program tracks the length to convert that into a slice.…

That's a classic example of an argument that looks really good from the 30,000 foot view, but when you're actually on the ground... no, basically none of that beautiful idea can actually be manifested into reality.

Re: Compiling C to Safe Rust, Formalized

#37

Post by nickpsecurity »

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.

Re: Compiling C to Safe Rust, Formalized

#39

Post by pizlonator »

orf wrote: post #23
pizlonator wrote: post #19

Earlier quoted context omitted.

Rust’s ownership model forbids things like doubly linked lists, which C programs use a lot. That’s just one example of how C code is nowhere near meeting Rust’s requirements. There are lots of others.

> Rust’s ownership model forbids things like doubly linked lists, which C programs use a lot. It’s literally in the standard library https://doc.rust-lang.org/std/collections/struct.LinkedList....

Good luck inferring how to use that from some C programmer’s deranged custom linked list.

C programmers don’t do linked lists by using libraries, they hand roll them, and often they are more complex than “just” a linked list. Lots of complex stuff out there.

Re: Compiling C to Safe Rust, Formalized

#40

Post by pizlonator »

titzer wrote: post #22
pizlonator wrote: post #12

Compiling a tiny subset of C, that is. It might be so tiny as to be useless in practice. I have low hopes for this kind of approach; it’s sure to hit the limits of what’s possible with static analysis of C code. Also, choosing Rust as the target makes the problem unnecessarily hard because Rust’s ownership model is so foreign to how real C programs work.

Meh, you know people are just going to throw LLMs at it and they'll be fine with it hallucinating correctish code by the ton-load. But I agree that they are going to have tough time making idiomatic Rust from random C. Like I said, correct-ish.

Great way to introduce novel security vulnerabilities!

If that’s the Rust way, then I’m all for it. Will make it easier for Fil-C to have some epic kill shots.

Post reply on HN