3 ms·

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

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