An unhackable computer?

Bluesun emails to point out this development:

The software that kept the helicopter’s computer secure was at the heart of its operating system, and it could be just what the world needs to make everything from pacemakers to insulin pumps and power stationsto cars immune to hacking.

“My hope is that in 10 years’ time, anything that is security critical is running on our system or some other one built on the principles we’ve established,” says Gernot Heiserfrom the newly formed Australian national research agency, Data61. One of its predecessors developed the crucial component of the “unhackable” operating system – its kernel.

...

Known as seL4, the kernel has a few highly secure properties: it can only do what it is designed to do; its code can’t be changed without permission; and its memory and data transfers can’t be read without permission. An earlier version of it, called OKL4, is now in millions of smartphones.

Heiser says that two features underpin seL4’s security, one of which is a new way of isolating data inside the kernel. But the key development was making the code capable of being checked mathematically. Other kernels might have these properties too, but it is impossible to know for sure without mathematical proof, says Heiser.

As devout Catholics say about miracles, that would be something.  Color me skeptical.

There has been a desire for provably secure operating systems for decades.  The first formalized efforts were captured in what was called the Orange Book, which defines what is required to do this.

The Orange Book pre-dates my 30+ career in computer security.  I've personally been involved in Orange Book evaluations of commercial products.  It was not a happy experience.  Lots of time spent, even more money spent, no return on the investment.

The problem is that what the security people want (security, duh) is not what the people budgeting for the computer want (functionality).  Sometimes the security people can impose standards that products have to meet (welcome to the Defense Department alphabet soup of FISMA, FEDRAMP, and JITC), but in the long run the security team will always lose the battle to the end users.

And this makes sense.  Just imagine if in 1950 the government established the Department of Computer Design, and all computers had to come from there.  Do you think you'd have an iPhone today?

And so my skepticism goes far beyond whether this truly is mathematically provably secure - I don't have the skills to really address that, although there's an old saying in cryptography that everyone knows enough to design a cipher that they can't crack (which doesn't mean that someone else can't).

My skepticism goes deeper - if this kernel is as secure as is claimed, then it can only be so because functionality is severely restricted.  If you restrict functionality, you make your end users very unhappy.  If some of these have stars on your uniform, you are unlikely in the extreme to be able to force them to use your system.

"My hope is that in 10 years’ time, anything that is security critical is running on our system or some other one built on the principles we’ve established"

Sorry, you don't get 10 years of reduced functionality - likely at significantly higher cost (those Computer Science PhDs don't pay for themselves).  Your users won't stand for it, or wait for you.

And so while an unhackable computer would be very nice indeed, this almost certainly isn't it.  Oh well, mustn't grumble - more work for Internet Security folks ...