12 ms·

The C bounded model checker: criminally underused

• gaudat 3y ago
  I miss this kind of stuff in computer programming languages. In hardware design, verification is done simultaneously with design, and semiconductor companies would be bankrupt if they did not verify the hell out of their designs before committing millions in manufacturing these chips. Even among hobbyists this is getting traction with yosys.perhaps its time for programmers to adapt this kind of tooling so there will be less buggy software released...
  • vacuity 3y ago
    There are probably orders of magnitude in difference between hardware design output and programming output. At least at the time, seL4's verification was quite impressive for a codebase on the order of 10,000 lines. But we should work towards the goal of improved formal modelling and checking all the same.
• 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.
• WalterBright 3y ago
  Unfortunately, int main(){ char buffer[10]; buffer[10] = 0; } are so rare they are hardly worth bothering with. The more usual case is: int get(char* buffer) { return buffer[10]; } void test() { char buffer[10]; get(buffer); } I.e. the array bounds for buffer get lost in the function call. I have proposed a fix: https://www.digitalmars.com/articles/C-biggest-mistake.html https://www.digitalmars.com/articles/C-biggest-mistake.html that is compatible with existing code. And yet, nobody cares. Oh well! Instead, we have overly complex solutions like this: https://developers.redhat.com/articles/2022/09/17/gccs-new-fortification-level https://developers.redhat.com/articles/2022/09/17/gccs-new-f...
  • philzook 3y ago
    Your example does not pass the verifier cbmc /tmp/walter.c --bounds-check --pointer-check --function test ... [get.pointer_dereference.5] line 3 dereference failure: pointer outside object bounds in buffer[(signed long int)10]: FAILURE ... There are many footguns. People love their guns. Makes them feel powerful.
    • WalterBright 3y ago
      int get(char* buffer, int i) { return buffer[i]; } #include <stdio.h> void test() { char buffer[10]; get(buffer, getc(stdin)); }
      • nanolith 3y ago
        CBMC's default contract for getc returns a non-deterministic integer value. A non-deterministic integer value basically counts as "pick a value that would cause this de-reference to crash the machine model". So, it will find a counter-example.
        • philzook 3y ago
          Yes, it returned the same "FAILURE" along with a couple new checks about getc that do pass.
• obl 3y ago
  Weird that this treats uninitialized variables as unknown values. For example in ex3.c, the program int main(){ int x; if (x <= 42){ assert(x != 12345); } } is of course UB in C, even though under a "uninitialized is random" model the program is valid and does not assert (as the model checker concludes). (even in O1 clang gets rid of the whole function, including even the ret instruction, I'm surprised it does not at least leave an ud2 for an empty function to help debugging since it would not cost anything https://godbolt.org/z/eK8cz3EPe https://godbolt.org/z/eK8cz3EPe )
  • philzook 3y ago
    I see the calling an undefined prototype style more often, perhaps for this reason. You are probably right this is undefined behavior, but it's subtle. https://stackoverflow.com/questions/11962457/why-is-using-an-uninitialized-variable-undefined-behavior https://stackoverflow.com/questions/11962457/why-is-using-an... I suspect CBMC just picks some concrete behavior for undefined behavior. It may not be a good detector for that. I'm not sure. This gets into shaky territory of understanding for me.
    • jcranmer 3y ago
      Speaking as a compiler writer: Any invocation of undefined behavior should be considered an assertion failure as far as any model checker should be concerned. Compilers can--and will--treat undefined behavior as license to alter the semantics of your program without any constraint, and most instances of undefined behavior are clearly programmer error (there is no good reason to read uninitialized memory, for example). Reading an uninitialized variable is not "subtle" undefined behavior. It's one of the most readily accessible examples not only of what undefined behavior can exist, but also the ways compilers will mutilate your code just because you did it. To be honest, if something as simple as the consequences of reading uninitialized memory are shaky understanding for someone trying to prove code correct, that will completely undermine any trust I have in the validity of your proofs.
      • philzook 3y ago
• IshKebab 3y ago
  This is also the backend for Kani - Amazon's formal verification tool for Rust. https://github.com/model-checking/kani https://github.com/model-checking/kani
• deleted 3y ago
  [deleted]
• jvanderbot 3y ago
  > however runs all possible executions, No, it does not. It probably does constraint based verification or looks for "proofs" of possible error conditions or asserts. In the case shown, an uninitialized variable is trivial to prove that it could equal the asseted value.
  • philzook 3y ago
    Yes, correct. It does not and could not _actually_ run all possible executions unless the program state space is quite small. But from a user's perspective, it is similar. I have tried this pedagogical approach to describing verifiers like these as "infinite" unit tests before (to mixed results). It feels to me that what symbolic or constraint based reasoning (algebraic identities, programs, integrals, what have you) in general is doing is finding a way to finitely reason about a very large or actually infinite number of concretized cases.
  • lou1306 3y ago
    Technically speaking it a) unrolls all loop up to their length (if it can be statically determined) or to a given verification bound; b) transforms the code into SSA; c) transforms the SSA into a SAT formula. If the SAT formula is satisfiable, its certificate is a counterexample to the property under verifecation. Of course the toy example is a toy, and of course it does not "run" anything, but this is a sound technique: if there is an execution that violates a property, it will be found. I highly suggest reading the paper that introduced it [1], it is remarkably clear! [1] Edmund Clarke, Daniel Kroening, and Flavio Lerda. 2004. A Tool for Checking ANSI-C Programs. In 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (LNCS), 2004, Barcelona, Spain. Springer, 168–176. https://doi.org/10.1007/978-3-540-24730-2_15 https://doi.org/10.1007/978-3-540-24730-2_15
• p0w3n3d 3y ago
  I believe valgrind shows uninitialised variables
  • skitter 3y ago
    Valgrind can only detect this for single executions, not for all possible ones.
• kazinator 3y ago
  The most important thing about this: int x; if (x < 42) { assert (x != 12345); } isn't to have a checker is clever enough to know that the assert will not go off, but to be informed that the automatic variable x is being accessed without being initialized!!!
  • mort96 3y ago
    To repurpose an old meme... Intelligence is knowing that the assert will never go off. Wisdom is knowing that it might.
    • kazinator 3y ago
      Wisdom is knowing that the entire block may be treated by your compiler as if it were __builtin_unreachable().
  • lou1306 3y ago
    Come on, that kind of check is almost trivial to implement. Anyway, there you go: extern int nondet (void); int x = nondet(); if (x < 42) { assert (x != 12345); }
    • kazinator 3y ago
      There are trivial cases of the use of an uninitialized variable that elementary data flow analysis will uncover. When the variable definition and its use are together in the same basic block, it's immediately obvious that the variable has a next-use on entry into the block, and that its definition hasn't supplied it with a value. From there it gets complicated. GCC has a history of emitting overly zealous diagnostics in this area, warning about possibly uninitialized variables that can be proven not to be. The difficulty is equivalent to the halting problem: void f() { int x; if (invokes_undefined_behavior(f)) x = 'A'; putchar(x); }