I've used CBMC in large commercial projects ranging around half a million lines of code. The secret is to break down every one of those functions into small pieces that the model checker can analyze.

CBMC works best with a contract-based programming style, where contracts are enforced by assertions and shadow functions exist to simplify model checking.

A single reply on HN is hardly a place where idiomatic styles can be expounded, but it is quite possible to build a resource-oriented idiomatic style that is reinforced with CBMC.

I would love to hear more

In particular, one of the more important rules I made when using CBMC was to keep the search depth for each invocation as shallow as possible. If CBMC runs in less than five minutes, you're doing it right. If it takes more than that, then you're asking it to do too much.

This led to the creation of function contracts and shadow functions. When evaluating functions, we actually want any calls that it makes to go to shadow functions instead of real functions. When we write a function, we include a contract that includes anything it may return, any side-effects it may have, and any memory it may touch / allocate / initialize. We then write a twin function -- its shadow function -- that technically follows the same contract in the most simplified terms, randomly choosing whether to succeed or fail. From CBMC's perspective, it's equivalent enough for model checking. But, it removes additional stack depth or recursion.

A good example of this would be a shadow function for the POSIX read function. Its contract should verify that the descriptor it is passed is valid. It should also assert that the memory region it is passed is bounded by the size it is given. The shadow function picks a non-deterministic state based on how it should set errno and how it should return. This state follows the POSIX standard, but the underlying system calls don't matter. Likewise, depending on the return code, it should initialize a number of bytes in the read buffer with non-deterministic values.

I used this shadow read function to find a buffer overflow in networking code and also to find a DOS infinite loop error in a tagged binary file format reader we were using.

CBMC isn't perfect, but when coupled with a good linter and -Wall / -Werror / -Wpedantic, it is a very useful layer in a defense in depth strategy for safer software.

> CBMC isn't perfect, but when coupled with a good linter and -Wall / -Werror / -Wpedantic, it is a very useful layer in a defense in depth strategy for safer software.

I agree to a certain extent, but at what point are you putting in more effort than it would take to migrate to a stricter language that offers more safety by default?

I'm not aware of any language that can't be improved by this strategy. Amazon even added SMT solving tooling around Rust, because Rust's built-in safety guarantees aren't enough.

I'd say that the added effort is minimal. The compiler spits out more errors. We think a little more carefully about how we write functions so CBMC doesn't complain. There are no silver bullets.

>Satisfiability Modulo theories (SMT) is an area of automated deduction that studies methods for checking the satisfiability of first-order formulas with respect to some logical theory T of interest. It differs from general automated deduction in that the background theory T need not be finitely or even first-order axiomatizable, and specialized inference methods are used for each theory. By being theory-specific and restricting their language to certain classes of formulas (such as, typically but not exclusively, quantifier-free formulas), these specialized methods can be implemented in solvers that are more efficient in practice than general-purpose theorem provers.

>While SMT techniques have been traditionally used to support deductive software verification, they are now finding applications in other areas of computer science such as, for instance, planning, model checking and automated test generation. Typical theories of interest in these applications include formalizations of arithmetic, arrays, bit vectors, algebraic datatypes, equality with uninterpreted functions, and various combinations of these.

http://smtlib.cs.uiowa.edu/about.shtml

So it's probably best to consider it for unit and "small scale" aggregated functional testing then? This is actually the first time I've come across it. It seems like it would be good to consider it for new projects or new features but would be quite an ask to retrofit it on legacy code that wasn't already well "unit tested"?

One of the examples they gave was an HTTP client, which would be a surprisingly non-toy example, so I looked at what they actually did in the code (https://github.com/FreeRTOS/coreHTTP/tree/main/test/cbmc).

Not that I'm an expert in processing what exactly is being tested, but it basically looks only able to prove that an individual function doesn't overrun buffers. If you tell it to assume that integer overflows can't happen (!). So I'm not impressed.

If you only test buffer overruns, VC++ static analyzer + SAL2 can do an excellent job on this. Basically if you annotate every pointer with a length, the compiler can tell you if a pointer arithmetic is safe or not.

Non trivial example projects https://model-checking.github.io/cbmc-training/projects.html Some crypto, AWS common C, FreeRTOS. Other interesting applications https://www.cprover.org/cbmc/applications/

Frama-C is also very cool. Also Coq VST and however seL4 does it. I think out of all of these, CBMC requires the least expertise / has highest automation. I also don't see how it can scale beyond the unit test level, or patch together verification conditions into global properties. Perhaps this could be done by some meta framework plugging together calls to CBMC. Given the level of penetration of formal methods generally, I think the relatively low ambition of CBMC compared to these higher ceiling techniques is good.

Thanks, very interesting stuff!

Klee (another tool mentioned in TFA) was run successfully against unmodified versions of all GNU textutils (or maybe it was coreutils... in any case, except for GNU sort, which was tricky due to large dynamically allocated buffers), and found bugs in quite a number of them.

Actually these GNU tools are relatively simple, compared to the code we usually write as a C/C++ software engineer at daily work. For example, if you have a function that takes just one single protobuf object, Klee cannot help you. Because the input space is too large. Klee can only operate at unit test level, with special crafted code. It did a good job on GNU textutils because the inputs of the each tool are relatively independent, and most inputs are just boolean flags that are either true or false. Also, please be aware that klee cannot provide any kind of assurance. Normally it cannot give you a proof saying your code is 100% safe, because most code are too complex to reach that. I'm saying while it usually tries to find all the execution paths of your code and execute them symbolically, usually it is not possible to finish executing all the paths. Though Klee can support C++, you will find fuzzing C programs is much easier than C++, because C++ data structures are way more complicated. Like, a C-style string vs a C++ std::string. A C array vs a std::vector. So, in order to get a broader usage of Klee, we need to rewrite our code in a simpler way.