[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.)

[tptacek]

I would call it more of a professional horse.

[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.

[nanolith]

I do it today; your assumption that "it would" is incorrect.

    void z(value* x) {
        /* preconditions. */
        MODEL_ASSERT(valid_value_ptr(x));
    
        /* do operation. */

        /* postconditions. */
        MODEL_ASSERT(z_postcondition(a, b));
    }

In practice:

    z(NULL); /* model failure. */
    z(&uninitialized_value_on_stack); /* model failure. */

It works, and the model checker runs in seconds.