4 ms·

I am not sure if you are serious or not. How does verification prevent buffer overflows? It can reduce their frequency, but you can never know you got them all

by sqeaky 9y ago

I am not sure if you are serious or not. How does verification prevent buffer overflows? It can reduce their frequency, but you can never know you got them all. They find issues in libCURL and openSSL that have existed for years. Very few people are better than the people working on those libraries. It is better to be safe by default then add risk only when you need it. I say this as a C++ developer, I think const should be the default state of all variables and one should have to opt out of that, and Rust did that right and C is so far from that I see no reasonable way to use plain old C safely. At least with C++ I can hide my stuff in classes and verify one thing at a time.

StavrosK 9y ago
It was probably the "Turing-incomplete" part that prevents buffer overflows. Easier to reason about/verify.
snakeanus 9y ago
Formal verification is not the same as a security audit. With formal verification you can prove that something is bug-free. > They find issues in libCURL and openSSL that have existed for years Neither of them are formally verified. https://github.com/seL4/seL4 https://github.com/seL4/seL4 however is formally verified.
- sqeaky 9y ago
  Please, step away from "formal verification" and come back to world the rest of us devs work in. I have never seen a formally verified piece of software even once. I don't know if its too hard to do to real software or if C doesn't allow for it, or if it is just too expensive. The simple matter is that is not an option for the vast majority of projects. Unless you can make it practical, I assert it has no place in a practical discussion about preventing software issues.
  - AnimalMuppet 9y ago
    Worse: "It's amazing how many bugs there can be in a formally verified piece of software." I forget who said it, but it's been a long time. (Maybe in connection with formal verification of an OS? Does anyone remember?) Formal verification only works if the formal verification was mistake-free. (And how are you going to prove that? With a formal verification? It's turtles all the way down...) Also, it only works for the aspects that were formally verified. Heartbleed, for example, could be regarded as a flaw in the specification; formally verifying that the code matches the spec won't save you from that.

by sqeaky 9y ago

StavrosK 9y ago

It was probably the "Turing-incomplete" part that prevents buffer overflows. Easier to reason about/verify.

snakeanus 9y ago

Formal verification is not the same as a security audit. With formal verification you can prove that something is bug-free. > They find issues in libCURL and openSSL that have existed for years Neither of them are formally verified. https://github.com/seL4/seL4 https://github.com/seL4/seL4 however is formally verified.

sqeaky 9y ago
Please, step away from "formal verification" and come back to world the rest of us devs work in. I have never seen a formally verified piece of software even once. I don't know if its too hard to do to real software or if C doesn't allow for it, or if it is just too expensive. The simple matter is that is not an option for the vast majority of projects. Unless you can make it practical, I assert it has no place in a practical discussion about preventing software issues.
- AnimalMuppet 9y ago
  Worse: "It's amazing how many bugs there can be in a formally verified piece of software." I forget who said it, but it's been a long time. (Maybe in connection with formal verification of an OS? Does anyone remember?) Formal verification only works if the formal verification was mistake-free. (And how are you going to prove that? With a formal verification? It's turtles all the way down...) Also, it only works for the aspects that were formally verified. Heartbleed, for example, could be regarded as a flaw in the specification; formally verifying that the code matches the spec won't save you from that.