C program proofs with Frama-C and its weakest-precondition plugin [pdf] | Hacker News Reader

C program proofs with Frama-C and its weakest-precondition plugin [pdf]

allan-blanchard.fr

Interesting. Using a fully automatic SAT solver for the easy stuff and Coq for the things the SAT solver can't prove maker good sense. We did that 40 years ago in the Pascal-F system. The Oppen-Nelson cooperative decision procedure system (the first SAT prover) did the easy stuff - proofs that only need addition, subtraction, multiplication by constants, and logic. Beyond that you had to write a "rule" and prove it with the Boyer-Moore prover, which is a constructive system that uses induction. About 95% of the verification conditions were solved without adding new rules.

This group got about as far as we did - arrays, but not dynamic allocation, pointers, or objects. "WP cannot currently work with dynamic allocation, " they write. That's the point at which describing what "valid" means becomes difficult, and you get into specification languages separate from the program.

I notice they put in what they called "ghost code", code which has meaning only at proof time. We called that "proof code". It's written in the same language as the real code, and can look at values from the output, but can't change them. This is a programmer-friendly way to write specifications. It's easy to write code to check a sort or a lookup if you're not concerned about speed or space. Then you prove that the dumb check and the complex algorithm get the same result.

One big problem with proof of correctness systems is that they tend to be designed by people in love with the formalism. They need to be designed by people who hate and fear bugs. The Microsoft Static Driver Verifier is probably the best example of a system aimed squarely at preventing crash-type bugs. It's the main tool Microsoft used to prevent drivers from crashing Windows 7 and later.

I've read very little detail about the Static Driver Verifier other than that it's supposed to use an SMT solver. I don't know if MS is using the same tool for other products in their portfolio or not. I've used it a little bit (it's a pain to set up) but have little information about exactly what it does, since it doesn't rely on any special annotations or specification language. Can you shed any light on more technical details about it?

With F*, Dafny and the Lean theorem prover, it seems like Microsoft (at least the research division) is moving in the direction of formal verification but I hear very little about it's use on their commercial products. Trade secret, perhaps?

The Static Driver Verifier is something you can download if you're a Microsoft developer. There's not much of a secret about it. There are papers. It tries to verify that a driver can't crash the rest of the kernel. No bad pointers, no infinite loops, no setting up DMA into some memory it shouldn't, no driver API calls with wrong params, stuff like that. Doesn't mean the driver will talk to the device properly. It just proves that the driver stays in its lane and doesn't mess up the rest of the system. Huge win for Microsoft. Half of Windows crashes used to come from drivers.

(Yeah, yeah, undecidability makes proving halting impossible. No. It's easy to prove that most code finishes. If you're writing a kernel driver and there is any ambiguity about whether the code will finish, you're doing something very wrong. If it's hard to prove termination, you add a loop counter so that after N tries, it gives up.)

It would be nice if it verified stack usage or microsoft mitigated known garbage kernel modules, I spent a good part of a day setting up debug symbols and tearing out drivers without debug info till finding out a Sophos kernel driver was blue screening about 50 or so workstations with 50 or so angry people.. what fun.

There's been a long, long tradition of software verification at Microsoft; look for SLAM (the original research backing the Static Driver Verifier), Yogi (SDV backend V2), Slayer (generic memory safety) and Terminator (termination of system code). All of the research is out in the open, often with reference implementations.

The problem with all of these things (as with FramaC) is that they only work if you restrict the fragment of programs that you're looking at. Kernel modules work out surprisingly well, because they are not allowed to do a whole lot by convention.

So this system uses the spec language ACSL (I assume it's a formal spec language, FSL).

How widely used is it? I've heard of TLA+ being very popular. Then there is Z notation, and about half a dozen or more others.

If there is no standard FSL, do I have to learn a new FSL everytime I want to apply formal methods to a slightly different system I'm working with?

Formal methods is a hard enough area. Lack of standardization makes it harder.

ACSL is indeed a FSL. Making a standard FSL is a nigh impossible since it should encompass every programming language and its specific features.

For example, ACSL has built-in ways to talk about the side effects in C, labels, the validity of pointers, etc. and the semantic of those elements is tied to the C standard.

On the other hand, the syntax of ACSL is heavily inspired from JML (FSL for Java) which is pretty popular. So if you know JML, it's easy to learn ACSL (you just have to learn C-specific features)

I remember Frama-C for its slicing. I have recently become interested in Datalog driven approaches, such as Souffle, for static analysis of large codebases. Anyone with experience or thoughts along those lines?

Out of curiosity, are there known pros and cons to each approach? I’ve been experimenting with Z3’s CHC engine and Coq for modeling programs. I don’t know enough about both yet to fully understand how they compare.

I wasn't sure what WP stood for. My mind jumped to WordPress but that obviously wouldn't make sense.

Turns out it stands for Weakest Precondition.

Hmm, good point. We've put weak preconditions in the title above.

Reply on news.ycombinator.com