3 ms·

> No chance. CBMC is amazing, but have you actually tried formally verifying a "real" program? Yes. Every day. It's actually quite easy to do. Write shadow met

> No chance. CBMC is amazing, but have you actually tried formally verifying a "real" program? Yes. Every day. It's actually quite easy to do. Write shadow methods covering the resources and function contracts of called functions, then verify the function. Repeat all of the way up and down the stack. It adds about 30% overhead over just TDD development.

PhilipRoman 2y ago
Last time I tried CBMC, it ended up running out of memory for relatively small programs, do you encounter any resource usage issues with it? I'm learning Frama-C and I find it more predictable, although the non-determinism of solvers shocked me when I first tried to prove non-trivial programs. I guess ideally I would like something even more explicit than Frama-C.
- nanolith 2y ago
  CBMC works best on functions, not programs. You want to isolate an individual function, then provide shadows of the functions it calls. The shadows should have nondeterministic behavior (cover every possible error condition) and otherwise follow the same memory and resource rules as the original function. For instance, if shadowing a function that reads a buffer, the shadow should ensure full buffer access as part of its assertions. The biggest issue you will run into with bounded model checking is recursion and looping. In these cases, you want to refactor the code to make it easier to formally verify outside of the loop. Capture and assert on loop variants / invariants, and feed these forward in assertions on code. There's no way I can capture all of this in an HN comment, but to get CBMC to work, you need to break down your code.
  - PhilipRoman 2y ago
    Thanks, that was really helpful. Relying on getting shadow functions right does seem icky, but I guess the improved productivity of CBMC should make up for it. Definitely going to give it another chance!
    - nanolith 2y ago
      You're welcome. I've been meaning to write a blog article on the subject, because it is a subtle thing to get working. Think of shadow functions as the specifications that you are building. Unlike proof assistants or Frama-C, you write specifications in C itself, and they work similarly to code. Often, the same contracts you write in these specifications can be shared by both the shadow functions and the real functions they shadow. I take a bottom-up approach to model checking. I'll start by model checking the lowest level code, then I'll shadow this code to model check code that depends on it. In this way, I can increase the level of abstraction for model checking, focusing just on the side effects and contracts of functions I shadow, and move up the stack toward more and more general code.
- KsassPeuk 2y ago
  What do you mean by "non determinism of solvers"? AFAIK, unless your proof finishes really close to the timeout, it is pretty uncommon that a failed PO suddenly succeeds and vice-versa if the code/the annotation are not modified.

PhilipRoman 2y ago

Last time I tried CBMC, it ended up running out of memory for relatively small programs, do you encounter any resource usage issues with it? I'm learning Frama-C and I find it more predictable, although the non-determinism of solvers shocked me when I first tried to prove non-trivial programs. I guess ideally I would like something even more explicit than Frama-C.

nanolith 2y ago
CBMC works best on functions, not programs. You want to isolate an individual function, then provide shadows of the functions it calls. The shadows should have nondeterministic behavior (cover every possible error condition) and otherwise follow the same memory and resource rules as the original function. For instance, if shadowing a function that reads a buffer, the shadow should ensure full buffer access as part of its assertions. The biggest issue you will run into with bounded model checking is recursion and looping. In these cases, you want to refactor the code to make it easier to formally verify outside of the loop. Capture and assert on loop variants / invariants, and feed these forward in assertions on code. There's no way I can capture all of this in an HN comment, but to get CBMC to work, you need to break down your code.
- PhilipRoman 2y ago
  Thanks, that was really helpful. Relying on getting shadow functions right does seem icky, but I guess the improved productivity of CBMC should make up for it. Definitely going to give it another chance!
  - nanolith 2y ago
    You're welcome. I've been meaning to write a blog article on the subject, because it is a subtle thing to get working. Think of shadow functions as the specifications that you are building. Unlike proof assistants or Frama-C, you write specifications in C itself, and they work similarly to code. Often, the same contracts you write in these specifications can be shared by both the shadow functions and the real functions they shadow. I take a bottom-up approach to model checking. I'll start by model checking the lowest level code, then I'll shadow this code to model check code that depends on it. In this way, I can increase the level of abstraction for model checking, focusing just on the side effects and contracts of functions I shadow, and move up the stack toward more and more general code.
KsassPeuk 2y ago
What do you mean by "non determinism of solvers"? AFAIK, unless your proof finishes really close to the timeout, it is pretty uncommon that a failed PO suddenly succeeds and vice-versa if the code/the annotation are not modified.