5 ms·

I did not say it was related to memory corruption. I said Go would be much safer than C (and it would be). When you remove an entire class of bugs, you can focu

by _wldu 7y ago

I did not say it was related to memory corruption. I said Go would be much safer than C (and it would be). When you remove an entire class of bugs, you can focus on other things... such as sound logic. I love OpenBSD and use it a lot. But this notion of C everywhere for everything is wrong.

newnewpdro 7y ago
That's great and all, but you'd create a host of new bugs unrelated to safety with a pile of new code in a largely unfamiliar language (for the openbsd devs, anyways). Rewriting the world in some safe language isn't a panacea, this meme is getting very old.
- pcwalton 7y ago
  The fact that memory-safe languages don't prevent every bug ever is not an argument against their use, any more than the fact that some people die in car accidents even when wearing a seatbelt is an argument that you shouldn't wear seatbelts.
  - newnewpdro 7y ago
    I'm not arguing against their use.
nanolith 7y ago
You also lose a lot of tooling that has been built up over the decades to help with C development, such as model checkers. Simply replacing one language for another doesn't help. It's silver bullet thinking. This isn't an issue of language or platform, but an issue of process. The OpenBSD team has one of the best overall software development processes out there, but it is still very much a manual process. The class of exploits that are currently being discovered are often discovered via tool-assisted analysis. Such tools can also be used during the software development process to find errors that can be exploited. There are a dozen or so of such tools available for C currently ranging from OSS to commercial. Typically, these tools rely on model checking or bounded model checking, and they are quite effective at reducing attack surfaces or entire classes of errors beyond what most languages can provide on their own. To take full advantage of model-guided development, however, requires a different software development process that is more difficult to adapt to older code bases overnight. Still, this adaptation is significantly less effort than, say, porting a C code base to Go or Rust. Model-guided development and other types of formal methods aren't silver bullets, and they aren't perfect. But, they are much more effective tools for building better systems than a language or compiler on its own. I suspect that the OpenBSD developers will adapt to using a model-guided approach. They make use of some static analysis tools already. I find this much more likely than the OpenBSD team switching to Go or Rust, as it is a much more pragmatic solution and a more powerful solution.
- na85 7y ago
  >The class of exploits that are currently being discovered are often discovered via tool-assisted analysis Which tools would I start googling if I wanted to learn more about this?
  - aaronmdjones 7y ago
    Clang's static analyzer and libfuzzer are fantastic, and the former has saved my bacon more than once. It also has lots of sanitizers (more than gcc) for run-time instrumentation, not that that would have helped in this case, but still.
- pcwalton 7y ago
  Can you elaborate as to what "model-guided approach" OpenBSD is going to use? I am skeptical of the claim that it is more "pragmatic" to adopt formal methods to achieve memory safety, as the number of projects that achieve memory safety through formal methods is multiple orders of magnitude smaller than the number of projects that achieve memory safety through just writing in a memory-safe language.
  - nanolith 7y ago
    If you read the article, this RCE had nothing to do with memory safety. But, a model checker does a great job of finding memory issues as well as logic errors, if you use it correctly. OpenBSD, AFAIC, has not announced any plans. But, there are plenty of tools out there that work. CBMC is a solid example and it is one I have used to great success with both systems programming and firmware development. As noted, this requires both a process change and a use of this tooling. Properly using assertions is a skill, but it can typically be cross-checked using existing manual processes with the added benefit of catching logic issues like the one that caused this RCE.
    - pcwalton 7y ago
      Many things, including Rust's type system, could theoretically prevent bugs like this if used properly too. The question comes down to compatibility of these tools with normal development practices. Formal methods are not known for their wide use in software like OpenSMTPD for many reasons, despite being around for decades. Until that changes, I have a hard time believing they are a "pragmatic" solution.
1over137 7y ago
Presumably, you could also build your C code with Address Sanitizer and use that in production, then most memory corruption would segfault. You'd have a performance hit of course, but could be worth it.

by _wldu 7y ago

newnewpdro 7y ago

That's great and all, but you'd create a host of new bugs unrelated to safety with a pile of new code in a largely unfamiliar language (for the openbsd devs, anyways). Rewriting the world in some safe language isn't a panacea, this meme is getting very old.

pcwalton 7y ago
The fact that memory-safe languages don't prevent every bug ever is not an argument against their use, any more than the fact that some people die in car accidents even when wearing a seatbelt is an argument that you shouldn't wear seatbelts.
- newnewpdro 7y ago
  I'm not arguing against their use.

nanolith 7y ago

You also lose a lot of tooling that has been built up over the decades to help with C development, such as model checkers. Simply replacing one language for another doesn't help. It's silver bullet thinking. This isn't an issue of language or platform, but an issue of process. The OpenBSD team has one of the best overall software development processes out there, but it is still very much a manual process. The class of exploits that are currently being discovered are often discovered via tool-assisted analysis. Such tools can also be used during the software development process to find errors that can be exploited. There are a dozen or so of such tools available for C currently ranging from OSS to commercial. Typically, these tools rely on model checking or bounded model checking, and they are quite effective at reducing attack surfaces or entire classes of errors beyond what most languages can provide on their own. To take full advantage of model-guided development, however, requires a different software development process that is more difficult to adapt to older code bases overnight. Still, this adaptation is significantly less effort than, say, porting a C code base to Go or Rust. Model-guided development and other types of formal methods aren't silver bullets, and they aren't perfect. But, they are much more effective tools for building better systems than a language or compiler on its own. I suspect that the OpenBSD developers will adapt to using a model-guided approach. They make use of some static analysis tools already. I find this much more likely than the OpenBSD team switching to Go or Rust, as it is a much more pragmatic solution and a more powerful solution.

na85 7y ago
>The class of exploits that are currently being discovered are often discovered via tool-assisted analysis Which tools would I start googling if I wanted to learn more about this?
- aaronmdjones 7y ago
  Clang's static analyzer and libfuzzer are fantastic, and the former has saved my bacon more than once. It also has lots of sanitizers (more than gcc) for run-time instrumentation, not that that would have helped in this case, but still.
pcwalton 7y ago
Can you elaborate as to what "model-guided approach" OpenBSD is going to use? I am skeptical of the claim that it is more "pragmatic" to adopt formal methods to achieve memory safety, as the number of projects that achieve memory safety through formal methods is multiple orders of magnitude smaller than the number of projects that achieve memory safety through just writing in a memory-safe language.
- nanolith 7y ago
  If you read the article, this RCE had nothing to do with memory safety. But, a model checker does a great job of finding memory issues as well as logic errors, if you use it correctly. OpenBSD, AFAIC, has not announced any plans. But, there are plenty of tools out there that work. CBMC is a solid example and it is one I have used to great success with both systems programming and firmware development. As noted, this requires both a process change and a use of this tooling. Properly using assertions is a skill, but it can typically be cross-checked using existing manual processes with the added benefit of catching logic issues like the one that caused this RCE.
  - pcwalton 7y ago
    Many things, including Rust's type system, could theoretically prevent bugs like this if used properly too. The question comes down to compatibility of these tools with normal development practices. Formal methods are not known for their wide use in software like OpenSMTPD for many reasons, despite being around for decades. Until that changes, I have a hard time believing they are a "pragmatic" solution.

1over137 7y ago

Presumably, you could also build your C code with Address Sanitizer and use that in production, then most memory corruption would segfault. You'd have a performance hit of course, but could be worth it.