13 ms·
Compiling C to Safe Rust, Formalized
- ljlolel 2y agoI wonder how well O3 can do just compiling C to rust in one shot
- saagarjha 2y agoProbably pretty bad.
- ojosilva 2y agoFunny, 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 2y agoI 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 2y agoThere'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.
- rustacular 2y ago[flagged]
- Alifatisk 2y agoc2rust.com, but it uses things like libc::c_int
- wffurr 2y agoNote 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.
- deleted 2y ago[deleted]
- tonetegeatinst 2y agoWhat is the main difference? Can compiler flags force compliance?
- nickpsecurity 2y agoFormal 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-later/ https://cacm.acm.org/research/a-few-billion-lines-of-code-la...
- LPisGood 2y agoMy 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.
- thunkingdeep 2y agoTypical term is “Oxidized”. I think they feel clever when they do the RiiR thing and say that.
- 2y ago
- jtrueb 2y agoInteresting how higher optimization levels didn’t really help speed up rust in the O level comparison
- vlovich123 2y agoAs 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
- jtrueb 2y agoYes, I’m just saying how it kicks in basically immediately (O1).
- pizlonator 2y agoCompiling 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 2y agoIt can be good as an interface language. Good for bindings.
- pornel 2y agoRust'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.
- bloppe 2y agoIs 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.
- orf 2y agoYou’ve misread the comment. The ownership model is close enough, but the way that model is expressed by the developer is completely arbitrary (and thus completely nuts).
- ActorNightly 2y ago[flagged]
- jedisct1 2y ago[flagged]
- CoastalCoder 2y agoWould you mind expanding on this? It sounds interesting, but I'm not tuned into either community enough to know what parallels you see.
- ActorNightly 2y agoHaskell philosophy is basically asumming that programmers were really bad at parallelism and thread saftey, and thus it was made to address this concern. However because that overarching idea is ideological in nature (i.e not true as a statement about programmers as a whole), the community was prevalent with ideology, using a lot of lambda calculus notation to set itself apart, and making coding in it cumbersome. As a result, nobody bothered to really do anything with it. Rust has largely the same problem. You see bits of use of it here and there, but its also based in ideology that programmers are bad at managing memory. From a technical viewpoint, Rust doesnt offer anything that doesnt already exist, while providing a more cumbersome way to code. Which is why its a days are numbered.
- tome 2y agoHaskell was most certainly not made to address a concern about programmers being really bad at parallelism and thread safety.
- ActorNightly 2y agoIt absolutely has. The functional programming paradigm is designed specifically to describe a program withoilut side effects, so you can be sure that execution is deterministic (and thus scalable and parallelizable). There are no other advantages to functional programming.
- nickpsecurity 2y agoThe 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.
- DonaldPShimoda 2y 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 2y 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.
- dboreham 2y ago[flagged]
- dang 2y agoMaybe so, but please don't post unsubstantive comments to Hacker News. Edit: it looks like you've been doing this a lot lately. Can you please not? We're trying for something more interesting here.
- zoom6628 2y agoI 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_ 2y agoMaybe because zig isn't memory safe.
- ChristianJacobs 2y 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.
- DonaldPShimoda 2y 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.
- mbana 2y agoCan 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.
- zozbot234 2y 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 2y agoIn 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/publication/220880915_Cyclone_A_safe_dialect_of_C/links/0c96052b83cd45e39f000000/Cyclone-A-safe-dialect-of-C.pdf https://www.researchgate.net/profile/James-Cheney-2/publicat...
- als0 2y 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 http://cyclone.thelanguage.org
- alkonaut 2y agoIf 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.
- CodesInChaos 2y agoA 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.
- Animats 2y agoIndeed, 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 2y agoI 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 2y agoInteresting 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 2y agoUgh. 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.
- deleted 2y ago[deleted]
- pizza234 2y agoI'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.
- LPisGood 2y 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 2y agoSuppose it is a dll that has exported functions returning or accepting unsafe strings. No way to make it safe without changing the API.
- tatref 2y agoIn Rust, there is no unsafe String, only blocks of code can be unsafe, no?
- whytevuhuni 2y agoThey likely mean a char* pointer to a null-terminated string, or a char* pointer and a length, as is usual for C. If Rust was forced to expose such an API (to be on par with C's old API), it would have to use `*const u8` in its signature. Converting that to something that can be used in Rust is unsafe. Even once converted to &[u8], it now has to deal with non-UTF8 inputs throughout its whole codebase, which is a lot more inconvenient. A lot of methods, like .split_ascii_whitespace, are missing on &[u8]. A lot of libraries won't take anything but a &str. Or they might be tempted to convert such an input to a String, in which case the semantics will differ (it will now panic on non-UTF8 inputs).
- protz 2y agoAuthor 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.