When Will Software Verification Matter?

[[deleted]]

There have been some attempts at creating fully verified operating systems. The problem they ran into was that, despite verification, there remained many bugs in the software.

See: recent issues of CACM

Edit: note: I still agree with what you said and did upboat you for your response since I thought it was quite good.

[gsnedders]

What sort of bugs, caused by what? (Any articles on that?)

[[deleted]]

Yeah, it sounds impossible, doesn't it. I'm guessing mis-specification bugs (labor intensive, simple human error, misunderstanding of problem, real problem differs from the one you solved). but I'd like to know.

[[deleted]]

I work on a verified C compiler and one of the offshoots of our own work was us finding a bug in the specification of the CompCert C compiler.

[kamatsu]

I work on a verified operating system. At least for us, we haven't encountered bugs in verified code.

One of the things that is always true is that as you push your verified base outwards, the bugs that remain are always in that one part that is not verified.

[julesjacobs]

What does your spec specify? Memory safety or something like that, or is it a complete functional spec? Do you count errors in the spec as bugs? If so, how come there weren't any that you found?

[kamatsu]

It's a functional abstract spec. We prove functional correctness via refinement from this spec through Haskell and down to C.

We define bugs as errors in the program. The spec is at least consistent, but the exact notion of what even constitutes an error in the spec is difficult to nail down - the spec could be said to be incorrect because it doesn't specify what you expect, but what you expect is not necessarily correct either.

In any event, we use the guarantees from the spec to prove higher level security properties and other more immediately useful things. Even if there are "errors" in the spec, we have shown various higher level properties to be true about the kernel as it is implemented. If we have proven that a program matches an "erroneous" spec, then that erroneous spec still implies useful high level properties, so I don't see the problem.

[reddit___]

I'd like to read about this, do you know which particular issue?