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

[Jerry Leichter]

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. So just what does having access to the source buy you?  Keep in mind that such things as checking for unexpected functionality would be much better done as part of the spec that's verified than by looking for carefully hidden code traps. 

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. 

If a product says it uses, say, OpenSSL, will we ask for a proof that the version being used is a verified one?  The question of how to safely interface verified with unverified is a difficult one - a special case of the general composability problem. 

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. 

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.)  But nothing comes without costs and side-effects. 

                                          -- Jerry