Hacker News Reader

Comment by IshKebab | Hacker News Reader

> I think a far better and more mature process is to update C to modern C and use a model checker such as CBMC to verify memory, resource, and integer math safety.

No chance. CBMC is amazing, but have you actually tried formally verifying a "real" program?

I agree replacing with a hand-architected Rust version is clearly the better solution but also more expensive. I think they're going for an RLBox style "improve security significantly with little-to-no effort" type product here. That doesn't mean you shouldn't do a full manual rewrite if you have the resources, but it's better than nothing if you haven't.

View on HN

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

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.

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.

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!

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.

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.

Reply on news.ycombinator.com