3 ms·

Nothing is perfectly memory-safe. Also, not sure I would see the point of this translation?

by shin_lao 4y ago

MaxBarraclough 4y ago
> Nothing is perfectly memory-safe. How about formally verified SPARK code?
- astrange 4y ago
  It’s strange that people think if they put the word “formal” in front of something it means it’ll work perfectly.
  - MaxBarraclough 4y ago
    The guidelines ask that you Please don't post shallow dismissals. Are you aware of the scope of SPARK's assurances? You can't accidentally dereference a NULL pointer in verified SPARK code, for instance.
    - astrange 4y ago
      Yes, but that's a quality of SPARK, not of the category of "formal methods" by default. For instance, if you write your own proof and then prove the program meets it, there could still be a logic error in your proof. Also, "in verified code" is a big loophole enough to leave security issues in - for instance a web browser (probably the thing you'd most like to prove security-issue-free) can still overwrite its own memory through things like OS image and font code, JavaScript JITs generating code to an insecure ABI you don't have a model for, syscalls to kernel code that can write back into your memory, etc. Believing "formal" makes things magically correct does seem to be a common problem; it also comes up when people say something has a "formal audit" or needs to get one from someone. How do they "formally" audit it? Are they wearing suits?
      - MaxBarraclough 4y ago
        > For instance, if you write your own proof and then prove the program meets it, there could still be a logic error in your proof. Sure. Even mathematics research journals sometimes publish erroneous proofs. Practical formal methods generally rely on automated provers. You're right though that software development using formal methods can still have a non-zero number of defects. AdaCore use the term ultra-low-defect software rather than bug-free software. For an interesting case-study see [0]. Unfortunately, even automated provers can have bugs. To my knowledge, all provers suitable for practical use are not themselves formally verified. I don't think this is often an issue in practice, though. It remains that formal methods have an excellent real-world track record. The 'problems' with formal methods aren't effectiveness, but effort/price, and perhaps scalability. > a web browser (probably the thing you'd most like to prove security-issue-free) can still overwrite its own memory through things like OS image and font code, JavaScript JITs generating code to an insecure ABI you don't have a model for, syscalls to kernel code that can write back into your memory, but not effectiveness. If you verify only certain parts of a software solution, then sure, you don't get formal assurances about its overall behaviour. > How do they "formally" audit it? Are they wearing suits? That's an entirely different use of the word, isn't it? [0] https://www.adacore.com/tokeneer https://www.adacore.com/tokeneer See page 59 of the (freely available) full report for Analysis section

Nothing is perfectly memory-safe. Also, not sure I would see the point of this translation?

MaxBarraclough 4y ago

> Nothing is perfectly memory-safe. How about formally verified SPARK code?

astrange 4y ago
It’s strange that people think if they put the word “formal” in front of something it means it’ll work perfectly.
- MaxBarraclough 4y ago
  The guidelines ask that you Please don't post shallow dismissals. Are you aware of the scope of SPARK's assurances? You can't accidentally dereference a NULL pointer in verified SPARK code, for instance.
  - astrange 4y ago
    Yes, but that's a quality of SPARK, not of the category of "formal methods" by default. For instance, if you write your own proof and then prove the program meets it, there could still be a logic error in your proof. Also, "in verified code" is a big loophole enough to leave security issues in - for instance a web browser (probably the thing you'd most like to prove security-issue-free) can still overwrite its own memory through things like OS image and font code, JavaScript JITs generating code to an insecure ABI you don't have a model for, syscalls to kernel code that can write back into your memory, etc. Believing "formal" makes things magically correct does seem to be a common problem; it also comes up when people say something has a "formal audit" or needs to get one from someone. How do they "formally" audit it? Are they wearing suits?
    - MaxBarraclough 4y ago
      > For instance, if you write your own proof and then prove the program meets it, there could still be a logic error in your proof. Sure. Even mathematics research journals sometimes publish erroneous proofs. Practical formal methods generally rely on automated provers. You're right though that software development using formal methods can still have a non-zero number of defects. AdaCore use the term ultra-low-defect software rather than bug-free software. For an interesting case-study see [0]. Unfortunately, even automated provers can have bugs. To my knowledge, all provers suitable for practical use are not themselves formally verified. I don't think this is often an issue in practice, though. It remains that formal methods have an excellent real-world track record. The 'problems' with formal methods aren't effectiveness, but effort/price, and perhaps scalability. > a web browser (probably the thing you'd most like to prove security-issue-free) can still overwrite its own memory through things like OS image and font code, JavaScript JITs generating code to an insecure ABI you don't have a model for, syscalls to kernel code that can write back into your memory, but not effectiveness. If you verify only certain parts of a software solution, then sure, you don't get formal assurances about its overall behaviour. > How do they "formally" audit it? Are they wearing suits? That's an entirely different use of the word, isn't it? [0] https://www.adacore.com/tokeneer https://www.adacore.com/tokeneer See page 59 of the (freely available) full report for Analysis section