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

Bear bear at sonic.net
Mon Jun 9 15:07:40 EDT 2014


On Mon, 2014-06-09 at 11:35 -0400, Jerry Leichter wrote:


> 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. 

We shall need to.  Many critical pieces of infrastructure already 
have a suite of "acceptance tests" - if you introduce a change and 
the result does not pass the acceptance tests, it does not become 
part of the code.  So that infrastructure is already there; the new 
bit is that the verification will have to be run as part of the
acceptance tests. 

> 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. 

I think that's a "layers of abstraction" problem.  You can verify an 
application at a higher level of abstraction by relying on verified
properties of lower levels. 

Things at a lower level of abstraction should be building barriers 
that things at a higher level of abstraction cannot breach.  Thus, 
if the "microkernel"  that does memory and process management is
verified to implement a memory protection policy that says so, then 
it should be the case that no memory written by one process ever 
becomes visible to another process without first being zeroed.  

Which doesn't completely defang something like Heartbleed, but at 
least limits what OpenSSL can leak to data owned by the process 
that OpenSSL is running in.  

With such barriers in place, building verifiable higher-level 
security that relies on those barriers ought to be relatively easy 
to achieve:  If the server starts a separate process to talk to 
each user, it can guarantee that none of those child processes 
can ever see data belonging to any other.  And at that point 
Heartbleed is starting to have trouble getting its hands on things
you need to protect.  

> 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. 

Indeed.  But it's also completely necessary at this point. 

				Bear




More information about the cryptography mailing list