I'm wondering if we should be redesigning all software around formally proven shims.
I've been thinking a lot about what a system would look like if we re-designed it from the ground up. Nothing as extreme as throwing out von Neumann architecture, but starting with our current hardware as the basis, and reconceptualizing the OS around security and stability.
Certainly it would be more distributed, more sandboxed, and more interface-agnostic. We've been running so much legacy code for so long that the abstractions are constraining our thinking about what's possible and desirable.
Clean-sheet redesign may be both impossible and a little extreme, but it's definitely time to fundamentally re-imagine the "personal computer."
But I think the cool thing is that they did NOT do a clean sheet redesign, right? They ARE running legacy code (they didn't write a million lines of code -- just the kernel).
They are using OS processes and sandboxing to enforce the fact that the legacy code can ONLY communicate via message passing. (Is that actually a good assumption? You can break out of sandboxes) And then you can prove that the kernel that manages the IPC does not do stuff like leak certain types of messages between processes.
I'm a big fan of running legacy code in restricted processes and using that to enforce information flow and security properties. That is a LOT more realistic than clean sheet redesign where you try to write everything in a different programming language and/or prove properties about milions of lines of new code.
Although I'm wondering if they are proving stuff about the "easy" part. Isn't it implementation bugs like sandboxing Flash and Java that lead to holes in Chrome?
I need to look at the details more, but I will bet that if their browser had all the features Chrome had, then its architecture with restricted processes + proven kernel would NOT have prevented most Chrome security issues, e.g.:
I vote yes. Formal verification has great benefits for software security and it's the "final form" (if you will pardon a redditism) of unit testing. It's one of the top skills I would like to learn.
You might be interested in L4; there's a variant that has been formally verified (but I think it's closed source?).
Formal verification allows you to prove that an implementation faithfully implements its specification. What does the formal specification for a web browser look like? I'm guessing that we're talking about thousands of pages of extremely dense math and code. How do you know that that specification is correct, or reasonable or what the user wants?
Now, maybe we don't want to do formal verification for correctness because it is too hard. So we settle for formally verifying that a program has some property of interest, like memory safety. But if you want memory safety, it is a lot cheaper to just use a language that gives you memory safety for free (haskell/scala/go/python) rather than trying to formally verify that your C++ program is memory safe.
> You might be interested in L4; there's a variant that has been formally verified (but I think it's closed source?).
You are probably thinking of seL4[1] unless there's another I don't know about. I believe you are correct that it's closed-source. That always bugged me though, since it seems to defeat the whole purpose of verifying such a critical part of a system's TCB. In my mind, the whole point is that I as a user don't need to just take anyone's word for it.
Unless I'm mistaken (and I'd love to find out that I am!), what we have with seL4 is a commercial vendor handing out an opaque binary blob and saying "we proved it's correct!" but providing no way for the user to verify that they really did prove anything. Frankly, these days I just don't trust any organization's assertions on such things no matter how thoroughly they claim they have proved it _to themselves_. It's certainly better than "we hit it with a hammer and it didn't break, most of the time!", but it still leaves open the possibility that the person asserting it's proved is lying, or that they did prove it's correct _except for the backdoor the NSA secretly coerced them into adding to the version they released_.
I wish I had the time to tackle something similar for the open-source world, but with 2 small kids around I barely have time for the small open-source projects I do manage. It's very cool too see this article's work being released in source form, and I really hope some open-source devs pick it up and run with it. I for one hope to be able to contribute in what time I do have.
I think you'll have a hard time persuading existing corporations and developers that this is worth doing; formal verification seems to be currently constrained to academia and safety-critical uses (say, Software Engineers that have been accredited by a local regulator and are working on shutdown routines for a nuclear power plant).
But perhaps if you built a formally proven shim around key pieces of software, you might be able to get someone else to adopt them and/or disrupt (usurp) an industry incumbent.
I think that's a matter of tool quality. If they're high quality tools/libraries/documentation, then it could just become another secondary skillset like writing good tests and using version control.
For motivation, talk to the folks worried about costs of substantial failures. This is really analogous to insurance. An unpleasant, but tolerable amount of overhead that gives you a maximal bound on how bad a failure can be.
> but starting with our current hardware as the basis, and reconceptualizing the OS around security and stability.
NB: Do NOT visit the code repository - it's governed by a copy-left proprietary license.
This has been done by Microsoft [1], although it was pure research (there were hints of them using it for something "real" eventually, though). Essentially it was an OS written in a variant of C# that had Eiffel-like contracts - static analysis was done by the OS when an application was installed.
Worth a read, as I said - make sure you keep away from the code.
I've been thinking a lot about what a system would look like if we re-designed it from the ground up. Nothing as extreme as throwing out von Neumann architecture, but starting with our current hardware as the basis, and reconceptualizing the OS around security and stability.
Certainly it would be more distributed, more sandboxed, and more interface-agnostic. We've been running so much legacy code for so long that the abstractions are constraining our thinking about what's possible and desirable.
Clean-sheet redesign may be both impossible and a little extreme, but it's definitely time to fundamentally re-imagine the "personal computer."