[_wldu]

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.

[nanolith]

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.

[pcwalton]

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]

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]

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.

[tptacek]

People say this all the time, but in practice, no, Rust's type system will not be used to prevent logic bugs, any more than model-checked C will be used to prevent random bugs in OpenBSD's C code. This simply isn't a bug that's in Rust's remit to address. It's a logic bug. Your language has those as much as anyone else's.

The libraries people write to prevent bugs like these from happening (at a low level, in the "keep metacharacters out of the command line" sense, not in the "don't accidentally put a conditional in the wrong place" sense which is the proximate cause of this bug) work in most languages, probably even C. By way of example: Ruby has a solid command line wrapping gem.

I think "you could use type checking to break that logic bug" shares a lot of structure as an argument to "the key to security is input validation". It's true-ish at a superficial level but almost totally useless in practice, because it depends on foreseeing what the exploitable bugs will be. If your proposed defense relies on a catalog of possible bugs, it's not a real defense.

Solid, ambitious type systems are a good thing. For other reasons.

[pcwalton]

> People say this all the time, but in practice, no, Rust's type system will not be used to prevent logic bugs, any more than model-checked C will be used to prevent random bugs in OpenBSD's C code.

I know that's your hobby horse, and I said "theoretically" specifically to head off this argument. I am also skeptical that type systems will prevent logic bugs like this in practice. I'm skeptical of formal methods for the same reason. (Of course, type systems are just simple formal methods.)

[nanolith]

OpenBSD's development process already incorporates linters and other static analysis tools, as well as code reviews.

Decomposing logic using Hoare triplets and properly incorporating assertions as hints to a model checker wouldn't significantly add time to the development process. There is a lot of misinformation about the supposed overhead of formal methods or the assumption that they must be total. A lot of this is due to the fact that formal methods are typically used in projects where serious harm or death could result from an error, and thus, the cost of verifying the project must exceed the potential risk for failure. An incremental approach is pragmatic and yields results. It does not require the totality of classical formal methods projects.

I have not noticed a significant increase in time for my own development efforts while incorporating model checking into my own software development process. That's anecdotal, but up until the past 10 years, there haven't been many OSS model checkers to choose from. In turn, the cost for using these tools have made it harder to have peer reviewed cost analysis. If using a commercial tool, it's because you were required to do so via FAA or similar. Hence, the adoption curve hasn't yet been wide enough to have the wide adoption you've alluded to. With both the availability of these tools and the increased tool-assisted nature of red team analysis, it'll come.

Language can't fix these problems alone. Not even Rust is a silver bullet here. But, the incorporation of formal methods is an additional layer in a good defense-in-depth strategy.

[pcwalton]

> Decomposing logic using Hoare triplets and properly incorporating assertions as hints to a model checker wouldn't significantly add time to the development process.

Yes, it would.

[na85]

>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]

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.

[newnewpdro]

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]

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]

I'm not arguing against their use.

[1over137]

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.