Hacker News Reader

Comment by accelbred | Hacker News Reader

This is false; with formal analysis tools like CBMC, you can prove the memory safety properties of your C code. You can even statically prove lack of integer overflows and that asserts are unreachable. I'll agree this is uncommon in general, but CBMC is used for various C codebases where I work. Though this tooling is also available for Rust with Kani.

View on HN

Is CBMC usable, directly, on any project? Or do you need to write your code in a certain way, using certain patterns, etc.? Or does the CBMC tooling need to be taught various things about how memory management works in your project?

Regardless, the fact that it's not used regularly/routinely with the Linux kernel (or any project that I'm aware of) suggests that it's either not suitable, doesn't catch enough issues to be worth the effort, or is just such a pain to deal with that no one has the patience to put up with it.

Rust gives you much (sure, not all) of what CBMC provides, in the compiler. That is a huge win, IMO.

Yet it's still not used in most C codebases. Where was it for Heartbleed?

We all understand that things can be done better. The problem is that they often are not.

Rust and other tools help by not giving people the choice to do sloppy work at all. History has proven many times that defaults matter.

That’s the crux of it. I think I can write safe C. So do many other people who, surely like me, cannot. I know I’ve written safe Rust because I had to fix my code until it was able to compile.

CBMC is truly wonderful technology. Rust is still more powerful and easier to use at scale.

If your project has 100k lines of code, would you rather use CBMC or Rust? What about if your project has a million? 10 million? 100 million?

The fundamental issue is that SMT-based verification scales quite poorly. The optimal use of SMT-based verification is proving local properties of small chunks of code independently, and using the type system's encapsulation to scale up to global correctness.

I think the issue with such formal analysis tools is that in order to make the analysis succeed you often end up writing code that doesn't look like normal C anymore and arguably at that point you're not writing C anymore.

---

As an aside, does CBMC check temporal memory safety and thread safety? It seems it checks for out-of-bound accesses, null pointer access and double-free, but I could not find a mention of use-after-free and data races.

Reply on news.ycombinator.com