7 ms·

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.

• deleted 2y ago
  [deleted]
• tonetegeatinst 2y ago
  What is the main difference? Can compiler flags force compliance?
  • nickpsecurity 2y 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-later/ https://cacm.acm.org/research/a-few-billion-lines-of-code-la...
  • LPisGood 2y 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.
    • thunkingdeep 2y ago
      Typical term is “Oxidized”. I think they feel clever when they do the RiiR thing and say that.
  • immibis 2y 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.
    • swiftcoder 2y ago
      > I'm not sure what it has to do with translating the code to Rust. Formally verified C programs typically have had all their undefined behaviour already stamped out during the verification process. That makes mapping it over to Rust a lot simpler.
      • tjoff 2y ago
        Translating undefined behavior is the easy part.
        • swiftcoder 2y ago
          Maybe, but only if you know the specifics of the environment in which it is executing (i.e. which compiler/architecture-specific behaviours the code actually relies on)
          • Filligree 2y ago
            Correctly written C programs don’t have undefined behaviour, so a translator can operate assuming there is none.
        • deleted 2y ago
          [deleted]
    • DonaldPShimoda 2y ago
      In this case specifically, two separate aspects are being referred to with regard to "formal verification". The first is that the translation function (from C to Rust) has itself been formally verified. In other words: if you give it a C program that obeys certain necessary pre-conditions, it will give you a safe Rust program. I believe the title of the paper is primarily using "Formalized" with regard to this characteristic. The second is that the set of programs the authors evaluate their tool on are C programs that have themselves been formally verified. I only barely skimmed the introduction and didn't see it addressed directly there, but I would assume that this is because the pre-conditions necessary for their translation to work are most easily (only?) met by formally verified C programs, where of course the verification has been rendered with respect to properties that would be relevant here (e.g., memory use).
• safercplusplus 2y 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.
  • lambda 2y 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.
    • safercplusplus 2y ago
      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 RefCell<>s 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 RefCell<>s, 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.
• jokoon 2y ago
  What is formally verified C? Why isn't there more of it?
  • PhilipRoman 2y 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.
    • zozbot234 2y ago
      Arguably, generating verified C from a low-level focused subset of F* (Low*, used in the HACL project) is close enough to count as a "similar tool".
• light_hue_1 2y 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"
  • lou1306 2y 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 2y ago
  Is Rust formally verified? Not that I know of
  • PartiallyTyped 2y ago
    You can always run model checkers like Kani, though even that is limited.
    • medo-bear 2y ago
      So no?
      • johnisgood 2y ago
        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.)
        • deleted 2y ago
          [deleted]
        • medo-bear 2y ago
          I think a disclaimer like this should be written with every Rust application, like health warnings on cigarette packets
          • johnisgood 2y ago
            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.
• medo-bear 2y 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)
  • gpm 2y 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.
    • medo-bear 2y ago
      Good luck with both of that. Otherwise people whose dayjob is rewritting everything in Rust will soon be out of a job
• cushychicken 2y ago
  Woof. Major unspoken caveat in the title!