The first thing about L4.verified is that formal verification, while admirable, doesn't really matter, at least not in a world where exploits are commodities, exploitation a continuous process: if a program is only a few thousand lines long and written with attention to security, the number of vulnerabilities can at worst be counted on one hand, and attackers will find them all for you in short order. If you're Iran and have an attacker capable of pouring millions of dollars into a single hack, it might make a difference; if you're Microsoft, not so much.

The second thing is that while a microkernel (if used with an IOMMU to prevent a malicious driver from DMAing all over your code) appealingly prevents an attacker from exploiting a malloc overflow in some random network driver and immediately gaining full access to anything (the current state of kernel security!-- but performance is key), it doesn't prevent an attacker from using that network driver pwn to hijack the user's Facebook session; full access is appealing, but in a complex system there are many, many "lesser targets" that are just as bad from a user's point of view.

Microkernels and their little cousin sandboxing can help, but the resulting trusted computing base is still much, much larger than we can formally verify in the foreseeable future.

(A sibling of this comment mentioned Singularity, but that's a fairly different beast: instead of proving that fast code is safe, you try to make obviously (memory) safe code fast. The only reason Singularity is able to make interesting performance claims is that it uses verification to completely avoid system calls: pretty cool, but a NaCl-like kernel could do something fairly similar for C; it doesn't really change the correctness/performance tradeoff.)

There's still role based access control and similar models that you can apply. As well as trusted path execution for binaries.

While none of this is bullet proof, it does add a very customizable kernel-level "sandbox". If you can't run your exploit for example, even thus the kernel is vulnerable, well, too bad.

Now for dreaming out loud, let's go code an OS in Rust that mimics most of Singularity and adds some RBAC on top for good measure (even thus its a much lighter version than on traditional OSes due to the system call avoidance and inherent sandboxing of all apps, as well as the contracted messages.)

You have many strong and valid points, But I think it's possible to engineer a world where "Memory corruption related exploits" cease to exit. There are many high-level programming techniques that can be used to prevent those, and I was making a point that we can fix the low-level ones also, most likely formal verification is not the way there, but it does exist as a possibility.

That is a very far cry from saying we can live in a world with perfect security, which I think is the point you are trying to make.

The L4 microkernel was verified that it faithfully implemented the system specification. The system specification is written in (executable) Haskell. http://en.wikipedia.org/wiki/L4_microkernel_family#Current_r... So, how do they know the Haskell specification is correct???

I guess it's turtles all the way down. http://en.wikipedia.org/wiki/Turtles_all_the_way_down

Well, they don't know whether specification is correct, but verification, while proving correctness, also proved (because you need these to prove correctness) no buffer overflow, no null pointer dereference, no unintentional integer overflow, etc.

So it's not useless.

I agree that is is not useless, however its usefulness is limited to the implementation level, verifying the translation from the Haskell specification to assembly/C/blub implementation is correct.

The higher level question is whether the Haskell specification fully and correctly specifies the desired behavior. In my 30-odd years of experience in Mil/Aerospace, I have never seen a fully and correctly specified set of requirements that could be transliterated into correct executable code. If nothing else, they all have had implicit assumptions. That is the Achilles heel of the IBM "Master Programmer" method, reborn as "outsourcing".

Since the specification is executable Haskell, that implies they wrote Haskell test programs to show that the specification implements the desired behavior.

Writing a program to verify the specification that another program implements... and then claiming a formal proof of correctness of the system is now recursive. Turtles all the way down.

I am quite aware of the problem of specification.

For others: I learned a lot from reading the book "Mechanizing Proof". No knowledge of formal methods is needed (but you will learn something about formal methods while reading). I can't recommend the book highly enough.

http://www.amazon.com/Mechanizing-Proof-Computing-Inside-Tec...

L4 was verified to the tune of about $4.6 million dollars, or $500 per line of code. And that's for a microkernel under 10 KLOC. And that's assuming no changes are made. Ever.

The idea of having a small kernel that is properly verified, and properly run user-level code in a memory-protected manner isn't absurd. And when put into the context of Operating System budgets, 4.6 Million dollars is completely reasonable. Again, we're also talking about a hypothetical 2040 OS. not something we're going to have working tomorrow.

I didn't mean to imply it's not possible, or won't be possible in the future, just that I don't think it's on the immediate horizon for anything but small kernels. 4.6 million dollars may be reasonable, but if you have to add on another million dollars and another month of verification time for every patch release... it's just not practical yet.