[Cryptography] Yet more formal methods news: seL4 to go open source

[Perry E. Metzger]

On Mon, 9 Jun 2014 11:35:31 -0400 Jerry Leichter <leichter at lrw.com>
wrote:
> Workable formal verification is going to have significant effects
> on the whole programming ecosystem. 
> 
> Consider the interaction between verification and open source. If
> you make *any* changes to a verified piece of code, you lose the
> verification.

Yes, so one has to make sure changes re-verify.

Note if one uses a system like Coq to write the verified
code in the same system that is doing the verification, there is no
meaningful distinction between the proof and the source code to the
system.

If, on the other hand, one writes the code in a separate language and
merely uses Coq (or Isabelle or what have you) as a proof system,
then one needs to distribute both the code for the system and the
formal specification/verification code.

> So just what does having access to the source buy you?

The same thing it does now.

> Perhaps we can get to a world in which anyone who changes the code
> is expected to update the verification. With the state of the tools
> we have now, that seems unworkable - it's just too hard and
> specialized.

Have you tried? Indeed, if you write your code in a dependently typed
style within Coq or what have you, how does one meaningfully update
the code *without* updating the proof? (There are quite interesting
artifacts written with Coq itself -- CompCert, for example.)

I think that, unfortunately, many people with strong opinions on this
topic have not done any work with modern tools. They are still
operating on memories of what things were like in the bad old days.
Things have changed.

> If a product says it uses, say, OpenSSL, will we ask for a proof
> that the version being used is a verified one?

Ultimately that will be necessary, yes, though infrastructure for
doing this is pretty straightforward in the open source world.
Note that *verifying* a proof is much easier than *constructing* a
proof. Proof checking can be quite fast.

It is harder in closed source, since the user doesn't have the source
code to verify the proof, but as a verified compiler (like CompCert)
can also generate a specification of the original code in logic (see
Andrew Appel's work), it may be possible for a user to check the
proof on the object code without having the source.

(Expanding on this latter point: keep in mind that a certified
compiler is proven to maintain observational equivalence of the
source and object, so it should be possible to mechanically transform
a proof about the properties of the source into a proof about the
object, given changes to the compiler of course. Such work is, again,
quite related to Appel's recent research.)

> At a fundamental level, moving to verified code requires changing a
> "whatever" work culture into a true engineering culture. It will be
> wrenching for many. 

Likely. Of course, most code need not be verified for verification to
have an impact. Quark and similar systems point at the method for
dealing with this -- you can verify a cage around the unverified code
and still get assurance without needing to verify the whole system.
Quark is quite impressive in that it provides assurance for Webkit
without needing to prove anything about Webkit code directly.

> Please don't take any of this as a critique of or a complaint about
> formal verification!  If will be a great tool to have. (I say "will
> be" because while we are now at the point where we can see
> practical application, the tools aren't there yet for broad
> adoption.)

Maybe, maybe not. What is "broad"? I would argue we're certainly at
an inflection point, comparable to what happened decades ago when
high level languages first became practical tools.

> But nothing comes without costs and side-effects. 

Naturally.

Perry
-- 
Perry E. Metzger		perry at piermont.com