4 ms·

Nice but can you run it on non-toy programs? I gave a talk about Frama-C a few years ago. It's very interesting technology, but not too useful at any scale (

by rwmj 3y ago

Nice but can you run it on non-toy programs? I gave a talk about Frama-C a few years ago. It's very interesting technology, but not too useful at any scale (http://oirase.annexia.org/tmp/2020-frama-c-tech-talk.mp4 http://oirase.annexia.org/tmp/2020-frama-c-tech-talk.mp4) One aim we had with Bounds Checking GCC back in '95 was to make it possible to use with real programs. Although it was quite slow, any open source program of the era could use it (https://www.doc.ic.ac.uk/~phjk/BoundsChecking.html https://www.doc.ic.ac.uk/~phjk/BoundsChecking.html).

philzook 3y ago
Non trivial example projects https://model-checking.github.io/cbmc-training/projects.html https://model-checking.github.io/cbmc-training/projects.html Some crypto, AWS common C, FreeRTOS. Other interesting applications https://www.cprover.org/cbmc/applications/ https://www.cprover.org/cbmc/applications/
- philzook 3y ago
  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.
  - rwmj 3y ago
    Thanks, very interesting stuff!
jcranmer 3y ago
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 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.
- snnn 3y ago
  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.
nanolith 3y ago
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.
- philzook 3y ago
  I would love to hear more
  - nanolith 3y ago
    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.
akoboldfrying 3y ago
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.
- snnn 3y ago
  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.

by rwmj 3y ago

philzook 3y ago

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

philzook 3y ago
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.
- rwmj 3y ago
  Thanks, very interesting stuff!

jcranmer 3y ago

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

snnn 3y ago
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.

nanolith 3y ago

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.

philzook 3y ago
I would love to hear more
- nanolith 3y ago
  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.

akoboldfrying 3y ago

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.

snnn 3y ago
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.