Is Code Verification Finally Good Enough?

Jonathan asks: "As someone who has been following the development of software verification technology, a recent trend has intrigued me. It seems that the formal method people have finally come down off their high horse and are offering code verification as just another tool. This approach shows up in recent Java and C# based code verification tools that aren't aimed at 'proving correctness' so much as finding potential errors. Now it seems that such an approach is beginning to find its way into XP methods[pdf] as another verification tool to supplement unit tests. Given the current speed and effectiveness of tools like the Spec# verifier, is code verification via automated theorem proving finally going to make its way into the mainstream?"

Comments

For what?

[Control Group]

What does "good enough" mean? Good enough for it to be included as a general-use software development tool?Good enough to guarantee that released code is bug-free? Good enough to guarantee that released code has no glaring security-affecting errors?

It makes a difference which "good enough" you're asking for.

(The answers to those questions, to channel one Urban Chronotis, are yes, no, and maybe. Not necessarily in that order)

Not possible

[Intron]

The problem with any verification tool is that it can't know what you expect the program to do unless you tell it. Why should this be any more correct than the program itself? In other words, if you can write a description of what the program should do that is more accurate than the program, then that description should replace the source code.

Re:Not possible

[rblum]

That - in an other discipline - is called "double bookkeeping". You specify things twice, independently. Once in the actual source code, once in the description.

That way, you'll know when the two disagree. It doesn't prove that it does what you *intend* to do, but it proves that spec and source say the same thing. If they're written by different people, you can now have a fairly high degree of confidence.

Does it make your program bug-free? Only if you can write a bug-free spec. But it's a useful concept to reduce the likelihood of problems.

Re:Not possible

[Coryoth]

The problem with any verification tool is that it can't know what you expect the program to do unless you tell it. Why should this be any more correct than the program itself? In other words, if you can write a description of what the program should do that is more accurate than the program, then that description should replace the source code.

It is often easier to describe what a program has to do than it is to describe exactly how to do it. I can describe what a square root finding algorithm has to do: given x it has to find y such that y*y =x; without coming close to writing something that actaully finds the square root. All the prover then has to do is ensure that the code instructions really do produce a result that satisfies the stated constraint - which is potentially entirely possible. Writing contracts for code can be as easy (or easier) than writing unit tests for code. If you write a contract instead of a unit test then that potentially gives the prover all it needs to verify that the code will work for all possible test cases instead of your predefined unit test cases. If the prover can't manage that then just feed in some test data and if the contract fails you've found an error (that is, at worst you've got a unit test already). Working this way can be remarkably efficient at weeding out errors - you verify code when it works, and essentially do unit testing for the code that can't be verified. Perhaps if you actually tried it you'd see.

Re:Not possible

[l33td00d42]

Alice: "Try to get this concept through your thick skull: the software can do whatever I design it to do"
(pause)
user: "Can you design it to tell you my requirements?"

boy, that's easy:

print "This software is required to print this statement.";

Re:a chain of crutches

[chroot_james]

they already do! I came across this the other day:

private getThis() { return this; }

Re:a chain of crutches

[kirun]

Seems like sensible future-proofing to me. Sure, the variable this is called this right now, but who knows what tomorrow will bring?

Re:Excuse me, did any of you graduate yet?

[Fahrenheit 450]

Well, it's quite possible to do things like restrict the problem to a decidable subset of the original problem and only let your solution work on those subsets. Or you can work on problems that are undecidable in general, but in most typical cases are not only decidable, but efficiently solvable. For example, most type systems work in one of these two ways.

You see, you should have learned before you graduated that just because a problem is hard (or impossible) in general, that doesn't mean the average case is hard at all.

Yes, it works, but it's not easy

[Animats]

The main reason program verification didn't catch on was that it was hopeless for C and C++. The semantics of those languages were so messy that formalizing them was nearly hopeless.

Java and C#, however, are good enough. (So were Pascal, Modula, and Ada.)

Here's the manual for the Pascal-F verifier, a system written by a team I headed back in the early 1980s. This was a proprietary system done internally for Ford Motor Company. Take a look at the example real time engine control program beginning on page 155. It was painfully slow back then; it took 45 minutes of VAX 11/780 time (1 MIPS) to verify that program from a cold start. Today, it would take about a second.

What's being proved in that example? First, that there are no subscripts out of range or arithmetic overflows. Second, that all loops terminate. (Yes, you can prove that for most useful programs; the halting problem applies only to pathological programs.) Third, that the following constraints hold:

• fuelpumpon implies (tickssincespark < (1000*ms)); if fuel pump is on, spark must occur within 1 sec.
• (enginespeed < rpm(1)) implies (not fuelpumpon); fuel pump must be disabled if the engine is not rotating
• cylssincespark <= 1; a spark must be issued for each cylinder pulse

Useful stuff, the conditions needed to keep the engine running.

This is "design by contract" with teeth. Each function is checked to insure that it always satisfies its exit conditions if its entry conditions are satisfied by the caller, and that the function doesn't overflow, subscript out of range, or fail to terminate. Each call is checked to insure that its entry conditions are always satisfied. The end result is a guarantee that those properties hold for the whole program.

This is a very valuable check. It insures that caller and callee are in agreement on how to call each function. That's the cause of a huge number of software bugs - the caller made some incorrect assumption about the function being called, or the function didn't check for something which it needed to check. Both of those can be statically machine checked.

It's not easy to get a program through formal verification with a verifier like that one. The verifier does almost all the work on easy sections of code, but where correctness depends on anything non-trivial, you have to work with the theorem prover to get the proofs through. This isn't easy. The DEC Java checker and Microsoft's Spec# checker aren't as hard-line.

Re:Yes, it works, but it's not easy

[Animats]

What is the semantic difference between C and Pascal?

The big problems with C/C++ from a formal methods standpoint:

• void* (You lose all the type information)
• Too much casting. (Again, you lose all the type information)
• Array size information isn't carried along with arrays or passed through function calls. (Biggest design mistake in C).
• The "array is a pointer to the first element" convention. (Is this an array or a single object?)
• Pointer arithmetic semantics are ill defined. (Long story.)
• C++ iterators don't have an explicit tie to the collection, so detecting iterator invalidation statically is hard.
• Hard to detect aliasing. (A consequence of the free use of pointers.)
• Too much "undefined behavior" that isn't prohibited.

I would expect pointer arithmetic to be the source of problems, but if I recall correctly, Pascal's pointers have arithmetic as well.

No, they don't.

Pointer arithmetic really is obsolete. Compilers have been generating code for subscripting that's as good or better than pointer arithmetic code for well over a decade now.

Re:No :)

[Control Group]

The steps in his methodology are counter-intuitive and therefore stupid

I agree with your general statement, but this isn't good evidence. Plenty of things are counterintuitive, yet correct and useful.

I present exhibit A: the whole of statistics. It is counterintuitive that after the tenth straight "heads" result, the eleventh flip still has even odds of coming up heads - despite the fact that the odds of eleven straight flips coming up heads are 2048:1. It is counterintuitive that you should always switch doors in the Monty Hall problem.

Or, if you're scientifically minded, I give you relativity. It is counterintuitive that no matter how fast you're moving relative to a light source, the speed of the light from your point of view will never change.

It is counterintuitive that gravity causes hot air balloons to rise, or that the way to escape Earth orbit is to accelerate along it, not away from Earth.

Counterintuitive doesn't necessarily mean that something's incorrect.

To quote Knuth

[dargaud]

"Beware of bugs in the above code; I have only proved it correct, not tried it." —Donald E. Knuth.

Re:a chain of crutches

[neutralstone]

Regardless of the poor decisions of some recruiters, I've found this to be true: the most competent and disciplined engineers tend to use as many checking techniques as possible (e.g., regression tests, unit tests, multiple static analysis tools, etc.). They use these techniques not as a substitute for a disciplined approach to design or to implementation (that would be foolish), but as a sanity check on a finished product. They use multiple checking techniques because they know they're human, and humans -- even the most skilled, most experienced, most disciplined ones -- make mistakes, and they want to do everything they reasonably can to catch mistakes before a product ships.

So to that end, model checkers (and other forms of checking) are Good Things(TM). The possibility that some will misconstrue checking facilities as a substitute for competent and disciplined engineers is a separate issue, and it's not the fault of the checking scheme. The *organizational* problem of poor recruiting cannot be solved by getting rid of model-checking systems, and if your recruiters think that talent can be replaced by a "verification" system, you've got bigger problems than merely the shoddy designs that will come down the pike.

(Please note that I prefer to use the term "check" rather than "verify", because the latter term, when used to describe a program, too easily connotes the notion that a "verified" program is free of any bugs (which is, needless to say, always a dubious claim). "Check" on the other had usually connotes the idea that there is a specific bug (or set of specific bugs) that is tested for. Of course, TFA mentions they don't want to imply that (verification == no bugs). But IMHO too many people make that mistake.)

logic bug

[hey]

How could a program ever find this bug:

if (vote == "democrat")
{
        republican++;
}

Verification gets a boost from managed langs

[icepick72]

Verification is speeding along because of managed languages. Verification for managed languages like Java and C# is easier to implement. Not so much for C/C++ where pointers are raw. (Note: C# allows unmanaged code but by default it's managed and I assume most developers work in C# in managed mode, except where performance or interopability is required)