Compiling C to Safe Rust, Formalized

https://arxiv.org/abs/2412.15042

by love2read • 2 years ago

291 145 2 years ago

arxiv.org

ljlolel• 2 years ago

I wonder how well O3 can do just compiling C to rust in one shot

saagarjha• 2 years ago

Probably pretty bad.

ojosilva• 2 years ago

Funny, I came here to say just the opposite, that I'm glad algorithmic computing is still a thing in research and that not everything is AI.

Ironically, AI is able to produce research-grade algorithms and will probably become an authority on the subject, helping take more traditional CS to the next level.

Garlef• 2 years ago

I think it would make sense to evaluate if the the 'surgical' rewrites mentioned in the article can be carried out by or assisted by an LLM based process.

sunshowers• 2 years ago

There's a lot of code in the world where correctness is a requirement. :)

I agree with the sibling -- I think LLMs may be able to help automate some parts of it, but humans are still 95% of it. At least for now.

Alifatisk• 2 years ago

c2rust.com, but it uses things like libc::c_int

love2read• 2 years ago

C2Rust is mentioned in the second paragraph of the related work section.

rat87• 2 years ago

How is c2rust doing these days? For practical codebases?

wffurr• 2 years ago

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.

tonetegeatinst• 2 years ago

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

nickpsecurity3• 2 years ago

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

LPisGood3• 2 years ago

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.

immibis2• 2 years ago

"Formally verified" means someone has written a correct mathematical proof that the code has no bugs (the proof is checked by a computer program to make sure it is correct). This is a very high bar.

I'm not sure what it has to do with translating the code to Rust.

safercplusplus2• 2 years ago

And even then, not completely reliably it seems (from Section 2.2):

The coercions introduced by conversion rules can however lead to subtle semantic differences

The example they give is this C code:

    1 uint8_t x[1] = { 0 };
    2 uint8_t *y = x;
    3 *y = 1;
    4 assert(*x == 1); /* SUCCESS */

getting translated to this (safe) Rust code:

    1 let x: [u8; 1] = [0; 1];
    2 let mut y: Box<[u8]> = Box::new(x);
    3 y[0] = 1;
    4 assert!(x[0] == 1) /* failure */

So the pointer (iterator) targeting an existing (stack-allocated) array declared on line 2 gets translated to an owning pointer/Box) targeting a (heap-allocated) new copy of the array. So if the original code was somehow counting on the fact that the pointer iterator was actually targeting the array it was assigned to, the translated code may (quietly) not behave correctly.

For comparison, the scpptool (my project) auto-translation (to a memory safe subset of C++) feature would translate it to something like:

    1 mse::lh::TNativeArrayReplacement<uint8_t, 1> x = { 0 };
    2 mse::lh::TNativeArrayReplacement<uint8_t, 1>::iterator y = x; // implicit conversion from array to iterator
    3 *y = 1;
    4 assert(*x == 1); /* SUCCESS */ // dereferencing of array supported for compatibility

or if y is subsequently retargeted at another type of array, then line 2 may end up as something like:

    2 mse::TAnyRandomAccessIterator<uint8_t> y = x; // implicit conversion from array to iterator

So the OP project may only be converting C code that is already amenable to being converted to safe Rust. But given the challenge of the problem, I can respect the accomplishment and see some potential utility in it.

edit: added translation for line 2 in an alternate hypothetical situation.

lambda3• 2 years ago

  the translated code may (quietly) not behave correctly.

The whole point of them show that example is that they say they catch this case, and bring it to the attention of the programmer:

  If the original C program further relies on x, our translation will error out, and will ask the
  programmer to fix their source code. This is another area where we adopt a “semi-active” approach
  to verification, and declare that some patterns are poor enough, even for C, that they ought to be
  touched up before the translation takes place.

jokoon• 2 years ago

What is formally verified C? Why isn't there more of it?

PhilipRoman• 2 years ago

Because it takes a lot of effort. Google Frama-C. On the flip side, it can express not just memory safety constraints, but also correctness proofs.

In this case it's not about Frama-C or similar tools though, see your sibling comments about the caveats.

light_hue_12• 2 years ago

Oh, this has so so many more caveats! It's borderline false advertising.

First of all they never translated any C! At all. Zero lines.

They took code written in F* and modified its C compiler to emit Rust. They never had to deal with any actual C code of any complexity, aside from the most trivial code that might theoretically be emitted by a toy compiler (but wasn't even that!). They just pretended they were dealing with C (or a heavily restricted Mini-C).

Even if we accept this, there are plenty of arbitrary restrictions on the C it can even support in principle:

If the original C program further relies on x, our translation will error out, and will ask the programmer to fix their source code.

That's saying you want C to already be written in a style that makes the Rust borrow checker happy! They're avoiding the actual hard parts of the problem.

These rules present simplified versions of what we support. Our implementation features several peephole optimizations ...

If I may translate from the language of academia. "We present beautiful rules in figure 4. But in reality, our implementation relies on a large number of hacks."

But it gets worse!

For overlap cases that can be distinguished statically (as above), we emit a compile-time error; otherwise, the Rust code will panic at runtime.

The resulting code is not guaranteed to be correct! For example, aliasing in C can cause crashes in the resulting Rust code. See comment at the top of page 10. We're going from a formally verified C program to a "It may crash now" Rust program!? That's nuts!

We apply our methodology to existing formally verified C codebases, namely, the HACL* cryptographic library ...

This is such a blatant lie that I had to return to it. It's designed to catch an unwary reviewer. We often talk about HACL being in verified C because it gets compiled to that. But it's not a C library, it's written in a totally different language. You cannot confuse the two.

I'm not a reviewer for their paper. But if I was, I would strongly fight for rejection.

The fact that they only handle formally verified C is so astronomically far away from being their main problem.

An honest title would be "Compiling a subset of F* to partially Safe Rust, Partially Formalized"

lou13063• 2 years ago

An honest title would be "Compiling a subset of F* to partially Safe Rust, Partially Formalized"

Sadly that is the name of the game in conference publishing. Make a big claim in the title and hope the reviewer does not read the fine print.

If I may translate from the language of academia. "We present beautiful rules in figure 4. But in reality, our implementation relies on a large number of hacks."

Er, this I can understand. Every conference paper only presents you with a simplified view of the contributions. There is no way to describe every corner case within the page limits of a conference paper (specifically, I bet this was submitted to POPL 2025).

akkad33• 2 years ago

Is Rust formally verified? Not that I know of

PartiallyTyped• 2 years ago

You can always run model checkers like Kani, though even that is limited.

gpm3• 2 years ago

No, but small pieces of it are, and there's active work to extend it

The concept of the borrow checker has been on a simplified version of rust https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf - work has continued in this area steadily (e.g. see tree borrows)

There's a variety of tools that take rust code and translate it to something a proof system understands, and then checks that it matches a specification. AWS is leading a project to use these to verify the standard library: https://aws.amazon.com/blogs/opensource/verify-the-safety-of...

antiquark• 2 years ago

Rust doesn't have a specification or standard yet, which would make it difficult to formally verify.

https://stackoverflow.com/questions/75743030/is-there-a-spec...

medo-bear14• 2 years ago

What is the benefit of compiling formally correct code to Rust? It seems that all the possible benefits are already there (if not more)

gpm3• 2 years ago

I suppose hypothetically putting it in an easier language to make changes in. Though it's hard to imagine it being easier to make changes to transpiled code than the original.

Alternatively this might be seen as a stepping stone to translating non-formally-verified C to rust, which I understand the US government has expressed a fair bit of interest in.

cushychicken• 2 years ago

Woof. Major unspoken caveat in the title!

pizlonator4• 2 years ago

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.

whatisyourwork• 2 years ago

It can be good as an interface language. Good for bindings.

pornel• 2 years ago

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. It's non-trivial even if the length is an explicit variable, and even trickier if it's calculated or changes representations (e.g. sometimes used in the form of one-past-the-end pointer).

Other C patterns like `bool should_free_this_pointer` can be translated to Rust's enum of `Owned`/`Borrowed`, but again it requires deducing which allocation is tied to which boolean, and what's the true safe scope of the borrowed variant.

pizlonator4• 2 years ago

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.

bloppe• 2 years ago

Is this sarcastic? There's a reason why the lifetime checker is so annoying to people with a lot of C experience. You absolutely cannot just use your familiar C coding styles in Rust.

jerf• 2 years ago

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.

smolder• 2 years ago

It's not that simple. In fact it's impossible in some cases if you don't sprinkle unsafe everywhere and defeat the purpose. Rusts restrictions are so that it can be statically analyzed to guarantee safety. The superset of all allowable C program behaviors includes lots of things that are impossible to guarantee the safety of through static analysis.

Formally verified C involves sticking to a strict subset of the capabilities of C that is verifiable, much like Rust enforces, so it makes sense that programs meeting that standard could be translated.

titzer• 2 years ago

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.

pizlonator4• 2 years ago

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.

jtrueb2• 2 years ago

Interesting how higher optimization levels didn’t really help speed up rust in the O level comparison

vlovich123• 2 years ago

As they say it’s likely that the code they’re outputting is pessimizing rustc’s ability. Namely it sounds like they’re inlining code as part of the conversion

jtrueb2• 2 years ago

Yes, I’m just saying how it kicks in basically immediately (O1).

nickpsecurity3• 2 years ago

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.

DonaldPShimoda3• 2 years ago

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.

uecker• 2 years ago

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.

You can certainly replace code using undefined behavior in C code by using defined constructs.

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.

I think this highly misleading. Some of the most reliable programs I know are written in C and Rust projects will also have critical vulnerabilities. Most vulnerabilities are not actually related to memory safety and the use of unsafe Rust will also lead to memory safety issues in Rust code. So I see some advantage to Rust but to me it is obviously overhyped.

_flux• 2 years ago

In contrast, the Rust type system has been mathematically proven to be correct.

Is this the case? E.g. the issue "Prove the Rust type system sound" https://github.com/rust-lang/rust/issues/9883 is closed with comment "This will be an open issue forever. Closing." in 2016: https://github.com/rust-lang/rust/issues/9883#issuecomment-2... .

At least nowadays (since 2022) we do have a language specification for Rust: https://ferrous-systems.com/blog/the-ferrocene-language-spec...

nickpsecurity3• 2 years ago

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.

zoom6628• 2 years ago

I wonder how this compares to the zig-to-C translate function.

Zig seems to be awesome at creating mixed environs of zig for new code and C for old, and translating or interop, plus being a C compiler.

There must be some very good reasons why Linux kernel maintainers aren't looking to zig as a C replacement rather than Rust.

I don't know enough to even speculate so would appreciate those with more knowledge and experiencing weighing in.

capitol_• 2 years ago

Maybe because zig isn't memory safe.

ChristianJacobs• 2 years ago

looking to zig as a C replacement rather than Rust

Rust isn't a "replacement for C", but an addition to it. It's a tool that Torvalds et. al. has recognised the value of and thus it's been allowed in the kernel. The majority of the kernel code will still be written in C.

I'm no kernel maintainer, but I can speculate that two of the main reasons for Rust over Zig are the compile time guarantees that the language provides being better as well as the rate of adoption. There is a lot of work done by many leading companies in the industry to provide Rust native code or maintained Rust bindings for their APIs. Windows devs are re-writing parts of _their_ kernel in Rust. There's a "movement" going on that has been going on for a while. I only hope it doesn't stop.

Maybe the maintainers feel like Zig doesn't give them enough over C to be worth the change? Many of them are still opposed to Rust as well.

DonaldPShimoda3• 2 years ago

Rust isn't a "replacement for C"

Hmm I think to clarify I would say that Rust _is_ intended as a replacement for C in general, but that this isn't how the Linux kernel developers are choosing to use it.

As for why the kernel developers would choose Rust, I would think another one of the primary benefits is that the type system guarantees the absence of a wide class of memory-related errors that are prevalent in C, and this type system (as well as those of its predecessors) has been subjected to significant scrutiny by the academic community over the last couple of decades to help iron out problems. I suspect this is also part of why Rust has a relatively large and passionate community compared to other C alternatives.

josefx• 2 years ago

It's a tool that Torvalds et. al. has recognised the value of and thus it's been allowed in the kernel.

Has there actually been a successfull contribution to the mainline kernel? The last two big projects I heard of (ext2 / Apple drivers) seemed to have issues getting their code accepted.

spiffyk• 2 years ago

Zig is nowhere near mature enough to be considered for the kernel yet. There are breaking changes to it regularly still - which is a good thing for Zig now, but not so good for huge, long-lived codebases like Linux. Also compiler bugs happen.

Saying this as someone who generally likes Zig's direction.

3836293648• 2 years ago

Zig isn't 1.0 and has zero backcompat guarantees. It's also barely used anywhere and hasn't proven its value, even if parts of it may seem promising

devjab• 2 years ago

As I understand it most kernel maintainers aren’t looking to replace C with anything.

Zig has much better interoperability with C than Rust, but it’s not memory safe or stable. I think we’ll see quite a lot of Zig adoption in the C world, but I don’t think it’s in direct competition with Rust as such. In my region of the world nobody is adopting Rust, the C++ people are remaining in C++. There was some interest in Rust originally but it never really caught on in any company I know of. Likely for the same reason Go has become huge in younger companies but will not really make its way into companies which are traditionally Java/C# because even if it made sense technically (and it probably doesn’t) it’s a huge change management task. Zig is seeing traction for programs without the need for dynamic memory allocation, but not much beyond that.

Ar-Curunir• 2 years ago

Rust is stable and used by a number of big players, while Zig is not stable, and as a result hasn’t seen widespread adoption yet

mbana• 2 years ago

Can something like `C2Rust` then use this to generate formally correct code?

Also, is much of the authors did manual or was it run through something to produce the Rust code? If so, where is the code that generates Rust, I do not see any links to any source repos.

zozbot2343• 2 years ago

If so, where is the code that generates Rust, I do not see any links to any source repos.

The paper states that these developments will be released under open source licenses after the review process is completed, i.e. most likely, after the paper is formally published.

amenghra• 2 years ago

In 2002, a group of researchers presented a paper on Cyclone, a safe dialect of C [1]. While (manually) porting code from C to Cyclone, they found safety bugs in the C code.

These kinds of manual or automated conversation from C to <safer language> therefore have potential not only for increasing adoption of safer languages but also for uncovering existing bugs.

[1] https://www.researchgate.net/profile/James-Cheney-2/publicat...

als0• 2 years ago

Cyclone is no longer supported; the core research project has finished and the developers have moved on to other things. (Several of Cyclone's ideas have made their way into Rust.) Cyclone's code can be made to work with some effort, but it will not build out of the box on modern (64 bit) platforms).

http://cyclone.thelanguage.org

alkonaut• 2 years ago

If you used a naïve translation to Rust, wouldn’t you get parts that are safe and parts that are unsafe? So your manual job would need to be only verifying safety in the unsafe regions (same as when writing rust to begin with)?

Seems it would be a win even if the unsafe portion is quite large. Obviously not of it’s 90% of the end result.

CodesInChaos2• 2 years ago

A naïve translation would produce rust code which is almost entirely unsafe (using raw pointers instead of references everywhere). Translating to references is difficult, since C code isn't written with the restrictions of the Rust alias model / borrow-checker in mind.

Animats2• 2 years ago

Indeed, yes. Someone tried converting C OpenJPEG to low-level unsafe Rust using c2rust. OpenJPEG was known to segfault on a test case. I tried that test case on the Rust version. Segfaulted in the equivalent place in the Rust code.

At least it's compatible. But that approach is a dead end. To make any progress, translation must recognize the common idioms of the language and upgrade those to the ideomatic forms of the target language. Compiling into Rust generates awful Rust, full of calls to functions that do unsafe C-type pointer manipulation.

The big upgrading problems mostly involve pointers. The most promising result in this paper is that they figured out how to convert C pointer arithmetic into Rust slices. Slices can do most of the things C pointer arithmetic can do, and now someone automated the translation. Pointer arithmetic that can't be translated has to be looked at with deep suspicion.

A useful way to think about this is that raw pointers in C which point to arrays implicitly have a length associated with them. That length is not visible in C source code, but exists somewhere, as a function of the program state. It might be a constant. It might be the size requested back at a "malloc" call. It might be a parameter to a function. It's usually not too hard for maintenance programmers to find array lengths.

That could be an LLM kind of problem. Ask an LLM, "Examine this code. What is the length of array foo?" Then use that to guide translation to Rust by a non-LLM translator. If the LLM is wrong, the resulting Rust will get subscript errors or have an oversize array, but will not be unsafe. Array size info idioms are stylized enough in C that it should be possible to get it right most of the time. Especially since LLMs can read comments.

p0w3n3d• 2 years ago

I wonder, if a C library is working (i.e. is not formally proven to be not having problems, but works in most ways) why shouldn't we translate it using rust unsafe? I would say there is a value in it as rust lacks of libraries generally. And this would not be different from using a dll/so that was written in c and can be unsafe in some circumstances after all

dmezzetti• 2 years ago

Interesting concept. But for a working system in C, why do we need to "convert" it to Rust. Seems like an effort where juice isn't worth the squeeze. Probably will create more problems than we're fixing.

kelnos• 2 years ago

Ugh. They didn't compile any C to Rust. They modified the F*-to-C compiler to emit Rust instead. So they compiled F* to safe Rust. And they couldn't even do that 100% reliably; some valid F* constructs couldn't be translated into Rust properly. They could either translate it into Rust code that wouldn't compile, or translate it into similar-looking Rust code that would compile, but would produce incorrect results.

Flagged, this is just a lie of a title.

pizza2342• 2 years ago

I've ported some projects to Rust (including C, where I've used C2Rust as first step), and I've drawn some conclusions.

1. Converting a C program to Rust, even if it includes unsafe code, often uncovers bugs quickly thanks to Rust’s stringent constraints (bounds checking, strict signatures, etc.).

2. automated C to Rust conversion is IMO something that will never be solved entirely, because the design of C program is fundamentally different from Rust; such conversions require a significant redesign to be made safe (of course, not all C programs are the same).

3. in some cases, it’s plain impossible to port a program from C to Rust while preserving the exact semantics, because unsafety can be inherent in the design.

That said, tooling is essential to porting, and as tools continue to evolve, the process will become more streamlined.

LPisGood3• 2 years ago

because unsafety can be inherent in the design

I agree in principle, and I have strong feelings based on my experience that this is the case, but I think it would be illustrative to have some hard examples in mind. Does anyone know any simple cases to ground this discussion in?

nuancebydefault• 2 years ago

Suppose it is a dll that has exported functions returning or accepting unsafe strings. No way to make it safe without changing the API.

colejohnson66• 2 years ago

Maybe a JIT? Especially one that can poke back into the runtime (like dotnet).

int_19h• 2 years ago

automated C to Rust conversion is IMO something that will never be solved entirely

Automated conversion of C to safe fast Rust is hard. Automated conversion of C to safe Rust in general is much easier - you just need to represent memory as an array, and treat pointers as indices into said array. Now you can do everything C can do - unchecked pointer arithmetic, unions etc - without having to fight the borrow checker. Semantics fully preserved. Similar techniques have been used for C-to-Java for a long time now.

Of course, the value of such a conversion is kinda dubious. You basically end up with something like C compiled to wasm, but even slower, and while the resulting code is technically "safe", it is still susceptible to issues buffer overflows producing invalid state, dangling pointers allowing access to data in contexts where it shouldn't be allowed etc.

zozbot2343• 2 years ago

You can do a lot better than that. You can treat memory ranges coming from separate allocations as distinct segments, and pointers as tuples of a segment ID and a linear offset within the segment. This is essentially what systems like CHERI are built on, and how C and C++ are implemented on segmented architectures like the 8086 and 80286. The C standard includes a somewhat limited notion of "objects" that's intended to support this exact case.

pizza2342• 2 years ago

There is no point in doing such type of conversions.

protz• 2 years ago

Author here, I thought it'd be helpful to address a few of the points brought up in the various comment threads.

1. This is an academic paper that we posted on arxiv, not a release announcement for a new product where we claim we have solved C to Rust. We submitted to a PL conference, not an open-source meeting like e.g. FOSDEM -- this is not the same audience at all, and the expectations are very different.

2. Our story is simple. We start from the constraint of translating C to /safe/ Rust, and see what this entails: a small well-behaved subset of C, inference of slice splitting, a translation that may error out, and a program that may abort (plus a few other things described in the paper). We evaluate our ideas on what we have (C embedded in F*), and show that it scales decently with those constraints in mind, on a large-scale C library that is used in Firefox, Python, and many other pieces of mainstream software. We don't claim we can rewrite e.g. Firefox in Rust automatically.

3. This is how research works. We think we have an interesting point in the design space; we don't claim we solve every issue, but think this is an interesting idea that may unlock further progress in the space of C to Rust translation, and we think it's worth putting out there for others to take inspiration from. Who knows, maybe some existing tool will use this approach for parts the fit in the subset, and fall back to unsafe Rust for other parts that don't fit! This is a very active area: if we can contribute something that other tools / researchers can use, great.

4. This is not the final story, and again this is how research works. We are working on an actual C frontend via libclang, and are exploring how e.g. guarantee that the generated Rust does not generate out of bounds accesses, perhaps by emitting verification conditions to Z3 (speculating on future work here). If the reviewers think more work is needed, that's fine, and we'll resubmit with enhancements. If the reviewers think this is an active area and others could benefit from our ideas, and take the paper, even better.

Compiling C to Safe Rust, Formalized

Related Stories