4 ms·

Formal methods and "proving" "correctness" have not taken off because while they seem like a great idea, it's insanely expensive to do it for non-trivial softwa

Formal methods and "proving" "correctness" have not taken off because while they seem like a great idea, it's insanely expensive to do it for non-trivial software, and you end up with a provably correct piece of software that is still full of business logic bugs and which inevitably fails to keep up with ever-changing business processes. I agree that software is terrible, and programming language choice plays a big role in what sorts of mistakes you can make, but I'm skeptical that attempting to write provably correct programs is a remotely realistic goal. Sure, it's possible to prove an algorithm, but the real world software systems that need the help--certainly anything that involves more than one process on a single CPU--have complexity that goes well beyond what can be modeled or reasoned about, much less be proven.

Animats 8y ago
It's not that hard to automatically prove that a large piece of software has no buffer overflows and no null pointer dereferences. We had that working decades ago. Unless the code is in C. Then it's really hard.
- OnlyOneCannolo 8y ago
  Difficult, yes, but solved [1]. There exist sound static analyzers for C and C++. "Sound" meaning no false-negatives. [1] https://github.com/NASA-SW-VnV/ikos/blob/master/analyzer/README.md#checks https://github.com/NASA-SW-VnV/ikos/blob/master/analyzer/REA...
  - jakevn 8y ago
    If this has solved the issue of automatically proving that any C or C++ program has no buffer overflows, why do we still see CVEs for popular libraries and software that result from them?
    - lapinot 8y ago
      `Sound' does not mean `complete'. Don't forget that no false positive or negative isn't all, the solver might just give up.
    - nickpsecurity 8y ago
      Neither FOSS projects nor commercial software use proven methods most of the time. That's why you see the results you see. I described that here: http://www.ganssle.com/tem/tem372.html#article4 http://www.ganssle.com/tem/tem372.html#article4 The tools can also miss things. They miss more as complexity goes up. High-assurance systems used to structure things in a hierarchical way with simple functions and only call downs to aid the analysis. Basically, reduce combinatorial explosion. Most software isn't structured anything like that. It does combinatorial explosion with C not giving analyzer a lot of information to begin with. So, it causes tools to miss things. Rust might be easier to analyze due to the type system. Those labels become inputs and heuristics for future static analyzers.
    - fulafel 8y ago
      Because people can't resist chasing proven incorrect code ("find bugs"), instead of overhauling programs for proven correct code. Because the latter is a lot of work.
  - pcwalton 8y ago
    How does this deal with higher-order functions? This is usually where these analyzers fall down. If you don't allow higher-order functions, then you just forbade virtual methods, so your analyzer can't handle real-world C/C++ code.
    - pron 8y ago
      It's really not that hard, but it's important to remember that while these tools do guarantee no undefined behavior, they may require either adding annotations or changing the program a bit. Their goal is to guarantee lack of UB not for free, but at a cost that's drastically lower than a rewrite in a safe language, something they deliver on quite well. So, for example, suppose you have a higher order function that takes a function returning a pointer, calls it, and dereferences its return value. For simplicity, let's assume we only care about NULL dereferencing and not other kinds of invalid memory, but the idea is the same. You then have two options: either you annotate the argument to require that it cannot return NULL -- in which case the tool would attempt to prove that any function passed as an argument satisfies this (possibly with the help of further annotations) -- or you add a runtime check, in which case the automatic proof is simple.
    - OnlyOneCannolo 8y ago
      Off-hand, I don't know how it handles higher-order functions. It analyzes LLVM IR, not the source directly, so I guess it depends on how virtual methods are represented in LLVM IR and whether those instructions are supported or ignored by the tool. The tool doesn't claim to handle everything, and doesn't claim to be complete. You can absolutely write code that it can't analyze because it's either too complicated or you're using unsupported language features. If you want your code to be analyzable, then you have to write it that way. The tool isn't magic. Don't you think it's an over-statement to say that it can't handle real-world code if it doesn't support higher-order functions? Not all C++ code uses virtual methods, and C doesn't even have this feature in the language.
  - littlestymaar 8y ago
    No false negative sounds nice, but the problem is the amount of false positives. The Unix `true` command is also a static analyser with no false negative (but 100% false positive on perfect code). And a perfect static analyser with no false negative or false positive is equivalent to solving the halting problem. So what we need is a «good enough» solution working with existing code. But the amount of CVEs and the low adoption of such tools empirically shows that we are far from there.
    - OnlyOneCannolo 8y ago
      This particular tool lets you trade analysis time for accuracy (amount of false positives) depending on your choice of settings, which is pretty neat.
- sansnomme 8y ago
  Ada may vaguely resemble Lua but aerospace grade code (think SPARK) is about as fun to write as assembly. Rust is not perfect but it has momentum and tons of free tooling. At this point it would be easier to just try to add more safety features to Rust than push for the adoption of a language without the conveniences expected of a post-Y2K programming language.
atombender 8y ago
There's a engineering-oriented middle ground that doesn't prove everything mathematically from first principles like Coq. Languages like Ada and Haskell can get you a long way without formal proofs.
pas 8y ago
It's hard because most languages do not help with that. There's not an easy option to get all the potential unhandled error sites for a code base. Even in Rust you can sprinkle your code full of "?" and you transformed back into runtime errors. Which is okay, if you understand it. It'd be great if such programming decisions could be annotated, then when someone imports a library it'd be easy to get a human readable list of potential runtime errors (edge cases). But usually when it's time to just churn out yet another app, cost-benefit analysis indicates that fuck that, let's use pokemon error handling. And it's hard to blame anyone for such a decision when the alternative is going a few more days without the shiny new app/feature. The end of the financial quarter is coming. The app/feature must "work". And that's why it's not surprising that no one uses Coq and Idris for run of the mill business as usual apps.
- lultimouomo 8y ago
  I'd say it's a fundamentally hard problem, instead. See halting problem.
- giornogiovanna 8y ago
  ? doesn't transform anything back into a runtime error. It's explicitly saying "I don't know how to handle any errors that happen here, so give it back to the caller." The "potential unhandled errors" are all still perfectly listed inside the return type.
  - pas 8y ago
    Uh, thanks! You are completely right. I forgot that it's not just an unconditional unwrap. What I wanted to communicate is that I find that in many cases error handling is a sort of twilight zone. When the environment or context of the running program is not what it should be. (Eg file not found, lack of permission to write to it, not enough memory, something is not configured, missing runtime dependency; and all the state validation errors, etc.) And the errors that result from this are usually too low level, and there is rarely enough information in the error messages (types) themselves to help understand (and potentially work around) the condition causing the error.
woah 8y ago
Proving correctness is always an incremental win when executed correctly. Everything that can be proved correct is one more bug that your editor will underline in red, and often one less test to be written.

Animats 8y ago

It's not that hard to automatically prove that a large piece of software has no buffer overflows and no null pointer dereferences. We had that working decades ago. Unless the code is in C. Then it's really hard.

OnlyOneCannolo 8y ago
Difficult, yes, but solved [1]. There exist sound static analyzers for C and C++. "Sound" meaning no false-negatives. [1] https://github.com/NASA-SW-VnV/ikos/blob/master/analyzer/README.md#checks https://github.com/NASA-SW-VnV/ikos/blob/master/analyzer/REA...
- jakevn 8y ago
  If this has solved the issue of automatically proving that any C or C++ program has no buffer overflows, why do we still see CVEs for popular libraries and software that result from them?
  - lapinot 8y ago
    `Sound' does not mean `complete'. Don't forget that no false positive or negative isn't all, the solver might just give up.
  - nickpsecurity 8y ago
    Neither FOSS projects nor commercial software use proven methods most of the time. That's why you see the results you see. I described that here: http://www.ganssle.com/tem/tem372.html#article4 http://www.ganssle.com/tem/tem372.html#article4 The tools can also miss things. They miss more as complexity goes up. High-assurance systems used to structure things in a hierarchical way with simple functions and only call downs to aid the analysis. Basically, reduce combinatorial explosion. Most software isn't structured anything like that. It does combinatorial explosion with C not giving analyzer a lot of information to begin with. So, it causes tools to miss things. Rust might be easier to analyze due to the type system. Those labels become inputs and heuristics for future static analyzers.
  - fulafel 8y ago
    Because people can't resist chasing proven incorrect code ("find bugs"), instead of overhauling programs for proven correct code. Because the latter is a lot of work.
- pcwalton 8y ago
  How does this deal with higher-order functions? This is usually where these analyzers fall down. If you don't allow higher-order functions, then you just forbade virtual methods, so your analyzer can't handle real-world C/C++ code.
  - pron 8y ago
    It's really not that hard, but it's important to remember that while these tools do guarantee no undefined behavior, they may require either adding annotations or changing the program a bit. Their goal is to guarantee lack of UB not for free, but at a cost that's drastically lower than a rewrite in a safe language, something they deliver on quite well. So, for example, suppose you have a higher order function that takes a function returning a pointer, calls it, and dereferences its return value. For simplicity, let's assume we only care about NULL dereferencing and not other kinds of invalid memory, but the idea is the same. You then have two options: either you annotate the argument to require that it cannot return NULL -- in which case the tool would attempt to prove that any function passed as an argument satisfies this (possibly with the help of further annotations) -- or you add a runtime check, in which case the automatic proof is simple.
  - OnlyOneCannolo 8y ago
    Off-hand, I don't know how it handles higher-order functions. It analyzes LLVM IR, not the source directly, so I guess it depends on how virtual methods are represented in LLVM IR and whether those instructions are supported or ignored by the tool. The tool doesn't claim to handle everything, and doesn't claim to be complete. You can absolutely write code that it can't analyze because it's either too complicated or you're using unsupported language features. If you want your code to be analyzable, then you have to write it that way. The tool isn't magic. Don't you think it's an over-statement to say that it can't handle real-world code if it doesn't support higher-order functions? Not all C++ code uses virtual methods, and C doesn't even have this feature in the language.
- littlestymaar 8y ago
  No false negative sounds nice, but the problem is the amount of false positives. The Unix `true` command is also a static analyser with no false negative (but 100% false positive on perfect code). And a perfect static analyser with no false negative or false positive is equivalent to solving the halting problem. So what we need is a «good enough» solution working with existing code. But the amount of CVEs and the low adoption of such tools empirically shows that we are far from there.
  - OnlyOneCannolo 8y ago
    This particular tool lets you trade analysis time for accuracy (amount of false positives) depending on your choice of settings, which is pretty neat.
sansnomme 8y ago
Ada may vaguely resemble Lua but aerospace grade code (think SPARK) is about as fun to write as assembly. Rust is not perfect but it has momentum and tons of free tooling. At this point it would be easier to just try to add more safety features to Rust than push for the adoption of a language without the conveniences expected of a post-Y2K programming language.

atombender 8y ago

There's a engineering-oriented middle ground that doesn't prove everything mathematically from first principles like Coq. Languages like Ada and Haskell can get you a long way without formal proofs.

pas 8y ago

It's hard because most languages do not help with that. There's not an easy option to get all the potential unhandled error sites for a code base. Even in Rust you can sprinkle your code full of "?" and you transformed back into runtime errors. Which is okay, if you understand it. It'd be great if such programming decisions could be annotated, then when someone imports a library it'd be easy to get a human readable list of potential runtime errors (edge cases). But usually when it's time to just churn out yet another app, cost-benefit analysis indicates that fuck that, let's use pokemon error handling. And it's hard to blame anyone for such a decision when the alternative is going a few more days without the shiny new app/feature. The end of the financial quarter is coming. The app/feature must "work". And that's why it's not surprising that no one uses Coq and Idris for run of the mill business as usual apps.

lultimouomo 8y ago
I'd say it's a fundamentally hard problem, instead. See halting problem.
giornogiovanna 8y ago
? doesn't transform anything back into a runtime error. It's explicitly saying "I don't know how to handle any errors that happen here, so give it back to the caller." The "potential unhandled errors" are all still perfectly listed inside the return type.
- pas 8y ago
  Uh, thanks! You are completely right. I forgot that it's not just an unconditional unwrap. What I wanted to communicate is that I find that in many cases error handling is a sort of twilight zone. When the environment or context of the running program is not what it should be. (Eg file not found, lack of permission to write to it, not enough memory, something is not configured, missing runtime dependency; and all the state validation errors, etc.) And the errors that result from this are usually too low level, and there is rarely enough information in the error messages (types) themselves to help understand (and potentially work around) the condition causing the error.

woah 8y ago

Proving correctness is always an incremental win when executed correctly. Everything that can be proved correct is one more bug that your editor will underline in red, and often one less test to be written.