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

141–150 of 173 posts

Re: Compiling C to Safe Rust, Formalized

#141

Post by jeltz »

lou1306 wrote: post #84
light_hue_1 wrote: post #77

Earlier quoted context omitted.

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…

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

As someone who recently reviewed hubdreds of abstracts for a mid-sized open source conference: our committee would have declined that talk due to the misleading title. Has academia really that low standards?

Re: Compiling C to Safe Rust, Formalized

#142

Post by neonsunset »

LPisGood wrote: post #132
colejohnson66 wrote: post #131

Earlier quoted context omitted.

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

I know Unity game engine uses some transpiler called IL2CPP that manages to preserve some of the safety features of C# but still gets the speed of CPP, so one direction is definitely possible

Oh, it's mainly for platform compatibility. IL2CPP performance is really problematic since it still carries many issues of Mono, even if transpiled to C++: https://meetemq.com/2023/09/18/is-net-8-performant-enough/ (don't look at just the starting graph - make sure to scroll down to notes where RyuJITs code competes with other fast entries or even outperforms them).

Perhaps what you were looking for is NativeAOT? Either way C ports really well to C# since it supports a large subset of it "as is" and then some with generics and other features originating from C# itself.

Re: Compiling C to Safe Rust, Formalized

#143

Post by medo-bear »

keybored wrote: post #138
medo-bear wrote: post #134

Earlier quoted context omitted.

Your tendency to answer jokes so seriously is a symptom of the hype

Me being humorless (read: not just rolling with your cop-out) is a symptom of the Rust hype. Doesn’t even make sense.

you feeling the need to defend it at every jibe. chill. rust is not a cult

Re: Compiling C to Safe Rust, Formalized

#145

Post by SAI_Peregrinus »

immibis wrote: post #56
tonetegeatinst wrote: post #30

Earlier quoted context omitted.

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

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

> "Formally verified" means someone has written a correct mathematical proof that the code has no bugs

No, only that it complies with a formal specification. The code will have bugs if and only if the specification has bugs.

The difficulty of writing a bug-free formal specification is just as great as writing bug-free code. In some domains it's easier to write the specification, but not in most. Fully specifying what a program shoud do is often the hardest part of programming, after all.

Re: Compiling C to Safe Rust, Formalized

#146

Post by lambda »

johnisgood wrote: post #105
medo-bear wrote: post #98

Earlier quoted context omitted.

So no?

The answer is that it is not. It frustrates me more than it should, I admit, that people always mention Rust when they talk about safety, but never Ada / SPARK. You want formal verification? Use Ada / SPARK. It has been battle-tested. It has been used for critical systems for a really long time now. (And a compiler being formally verified vs. being able to write formally verified code means two different things.)

You also need to consider that formal verification is not the be-all/end-all of correctness.

Formal verification is verifying a mathematical model of the program correct, according to certain mathematical correctness properties. That model may not actually represent the real world, or the correctness properties may not actually be the properties that you want to guarantee. Famously, there was the formally verified Java LinkedList implementation that was buggy due to the formal model not taking into account integer overflow.

There are parts of the Rust language and standard library that have been formally verified. That helps provide confidence that the basic model, of having safety properties upheld by unsafe core functions, to be sound.

But the big advantage of Rust, especially for everyday open source code that the world widely depends on, is that it strikes a good balance between a language that people actually want to use, and which can provide good practical safety guarantees.

Rust is far, far safer than C and C++. Most other memory-safe languages also are, but trade that off for lower performance, while Rust provides a similar level of performance as C and C++. And additionally, it's a language that people actually want to use for writing a lot of the core infrastructure.

As far as I know, I have never use any open source software written in Ada/SPARK. People just don't do it. The only reason they generally do is if they need to for functional safety reasons, in a high-criticality system, and they find it easier to get their software certified by writing it that way.

And even in safety critical systems, most people find using a subset of C, with restrictive rules, static checkers to check those, code review, and extensive testing, done by independent teams and testing on real hardware with requirements based tests that achieve 100% coverage at the MC/DC level is considered to be the gold standard of verification.

Formal verification can not possibly provide some of the safety guarantees that testing on real hardware based on actual system level requirements can provide.

Formal verification is one tool in a toolbox. It is useful for providing certain guarantees. But it's less important than many other factors for the actual improvements in safety that Rust can provide; by actually being used, in critical software that is exposed to potential network based exploitation, a memory-safe language like Rust makes a much better foundation than C or C++, and more people will actually use it in such a context than Ada/SPARK.

Re: Compiling C to Safe Rust, Formalized

#147

Post by safercplusplus »

lambda wrote: post #129
safercplusplus wrote: post #61

Earlier quoted context omitted.

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 = Box::new(x); 3 y[0] = 1; 4 assert!(x[0] ==…

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 p…

Thanks for clarifying. The issue is what code would be rejected for auto-translation, not the correctness of an "accepted" translation (as my comment may have implied).

The point of noting that the example translation quietly does the wrong thing, is that that is the reason that it would have to be ("unconditionally") rejected.

While the paper does suggest that their example translation would be rejected:

> If the original C program further relies on x, our translation will error out

note that precisely determining whether or not the program "further relies on x" statically (at compile/translation-time) is, in general, a "Halting Problem". (I.e. Cannot be reliably done with finite compute resources.) So they would presumably have to be conservative and reject any cases were they cannot prove that the program does not "further rely on x". So it's notable that they choose to use a (provisional) translation that has to be rejected in a significant set of false positive cases.

And at least on initial consideration, it seems to me that an alternative translation could have, for example, used RefCells or whatever and avoided the possibility of "quietly doing the wrong thing". (And thus, depending on your/their requirements, avoid the need for unconditional rejection.) Now, one might be an a situation where they'd want to avoid the run-time overhead and/or potential unreliability of RefCells, but even then it seems to me that their translation choice does not technically avoid either of those things. Their solution allocates on the heap which has at least some theoretical run-time overhead, and could theoretically fail/panic.

Now I'm not concluding here that their choice is not the right one for their undertaking. I'm just suggesting that choosing a (provisional) translation that has to be rejected with significant false positives (because it might quietly do the wrong thing) is at least initially notable. And that there are other solutions out there that demonstrate translation of C to a (high-performance, deterministic) memory-safe language/dialect that don't have the same limitations.

Re: Compiling C to Safe Rust, Formalized

#148

Post by mardifoufs »

chillingeffect wrote: post #114
johnisgood wrote: post #108

Earlier quoted context omitted.

At this point, I think that would be better, yes, just because people think Rust is "fully" safe, which is just incorrect. I think the problem was the Rust hype and repeated statements of it being very safe, so we have some undoing to do. For example if someone on GitHub sees that the project is written in Rust, they are automatically going to assume it is safe, incorrectly so. I do not blame them though.

Rust is to safe as Tesla is to autopilot.

Judging by the facts, are you saying that Tesla has a safe auto pilot? Rare to see on HN :^)

Re: Compiling C to Safe Rust, Formalized

#149

Post by keybored »

medo-bear wrote: post #143
keybored wrote: post #138

Earlier quoted context omitted.

Me being humorless (read: not just rolling with your cop-out) is a symptom of the Rust hype. Doesn’t even make sense.

you feeling the need to defend it at every jibe. chill. rust is not a cult

A jibe is some sort of playful banter based on a literal or exaggerated truth. Since your comment does not lampoon any real deficiency except when being hypocritical, there is nothing to defend.

Maybe you should wear a sign on your torso: will make irrational points and then complain about persecution when that is pointed out. I don’t know. It’s just one more idea for when we decide to put all the anti-Rust people in camps.

Re: Compiling C to Safe Rust, Formalized

#150

Post by keybored »

woodruffw wrote: post #119
medo-bear wrote: post #115

Earlier quoted context omitted.

The point, I think, was that "safety" presumptions about Rust are often exaggerated or poorly misunderstood due to hype. That could certainly lead to problems

I don’t think Rust’s actual safety properties aren’t overhyped, although they may be subject to misunderstanding about their exact extent. Concretely: spatial and temporal memory safety are good things, and Rust achieves both. It’s not unique in this regard, nor is it unique in not having a formal definition.

Double negation makes things ambigious.
Post reply on HN