Quark: A secure Web Browser with a Formally Verified Kernel
goto.ucsd.edu
goto.ucsd.edu
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."
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.:
http://blog.chromium.org/2012/05/tale-of-two-pwnies-part-1.h...
That is, these attacks aren't about message flow or corruption in the browser kernel.
You might be interested in L4; there's a variant that has been formally verified (but I think it's closed source?).
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 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.
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.
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.
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.
> Quark has been tested on Ubuntu 11.04. A basic installation process is automated in ./install_module.sh file, and you can execute the installation script to install most of the requied packages and compile Quark itself. If any of the required jobs fails because of some conflicts in your system, you have to open the installation script, and track down what went wrong manually. As future work, we have a plan to implement a fully functional installation script.
The installation script involves creating "tab" users(tab0-tab9), but the install script doesn't check to see if these users exist before attempting to create them. If the installation fails after the user creation section, the install script will error out when it attempts to create users that already exist.
Here's what I did to save you about 2 minutes of brainpower
for i in {0..9}
do
if id -u tab$i >/dev/null 2>&1;
then
echo "user 'tab$i' already exists"
else
echo "creating user tab$i"
execcomm "sudo useradd tab$i"
fi
done
if id -u output >/dev/null 2>&1;
then
echo "user 'output' already exists"
else
execcomm "sudo useradd output"
fi
Today is focused on unit-testing and test code coverage, but formal proof seems really even better.
I only have heard about Coq , which i think implies code has to be written in OCaml , but i suppose the same kind of tool exists / could be done for Haskell or Scala. What about less strict and more used languages like C or Java ?
Formal proofs (and type systems too) can only prove that your programs and formal specifications are internally consistent. The overwhelming largest set of failures in commercial software development are in requirements solicitation!
"Mathematics may be defined as the subject in which we never know what we are talking about, nor whether what we are saying is true." - Bertrand Russell
There is a very high initial and maintenance cost to proofs and it would be a mistake to insist that people pay that cost when better cost/benefit trade offs exist for most needs.
Automated proof checking and derivations systems have been under development and research for a long time now. It's almost just an engineering problem to introduce them in a way that commercial companies can use them.
The aerospace industry (ex Boeing) has been doing this for a long time, and they make it work quite well for them.
Sure, and Microsoft has been using formal methods for eliminating all manner of security holes since at least the XP SP2 days. I didn't say that formal methods were always a bad trade off. I said that they are very expensive and implied that they are a bad default tradeoff for general purpose tools to make.
I am especially interested in the history leading to software verification in avionics, the involvement of insurance companies and government regulation.
thx
If we were able to get rid of the 'THIS SOFTWARE IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED OR IMPLIED' thing that graces virtually every software license agreement, so that software publishers were actually liable to some extent for the software they produced, that would help to improve things. I don't see that happening any time soon though.
Then once one popular code lib or framework starts doing it, we all know the rest will follow and the trend will be set.
1. This is one of those things where you want it to be all-or-nothing. "30% formally proved" is completely useless; it just means that the inevitable bug or security hole is in the other 70%.
2. You're limited to writing constructs that can be formally verified. (My understanding is that this means that it's a bit more difficult than "let's formally verify Ruby and then run all the Ruby programs on our verified Ruby"; some programs will need to be rewritten and others will simply not be verifiable.)
3. We still have to solve the politics problems that already are pervasive in some of these environments (e.g. people who intentionally leave easy bugs in their code and then fix them later so that they look like they made more changes as measured by a KLOC count).
But what I really wanted to talk about is the exciting stuff going on in languages like Idris where programming is paramount and proving is just there for support. In a situation like this, your goal is less to arrive at 100% formally proven systems, but instead steal 90% of the power of a proof assistant to build more maintainable, powerful code. In this case, you're quite likely to only prove 30% of your code, the skeleton perhaps, and leave the rest. The result is often however that when you do this, the remaining 70% of the code is so restricted by your design that there are only a handful of ways to continue and they're likely all the right behavior.
A great example of this is Ur/Web which uses just a little bit of dependent typing to ensure that the names in your forms, domain, and databases all match up. It means you design your entire system around those names (your domain) and prove it to be formally consistent. Then the remaining design space is tiny and it's easy to write a good program.
... Or even to augment that skeleton with a security policy and have static flow control analysis "for free".
(That said, Ur/Web is a prototype system with minimal documentation, so I won't recommend it as an actual "system of the future"... just a glimpse.)
That said, each of them is far more similar to OCaml/Haskell than say, C.
They are all based to some degree or another on Martin Löf's Intuitionistic Type Theory which is a wonderful unification of mathematical logic and straightforward functional programming in the same vein as the Curry-Howard Isomorphism.
Generally, much of the forward research is aimed at making the proofs more automatic and easier to use. The problem is wildly intractable by brute force, so much cleverer tricks must be employed. Some of these are quite wonderful and suggest new ways of programming as a dialogue between a human and an intelligent compiler that I really hope become more common in the future, though the industry will be unlikely to drive it. See the literature on Epigram for some talk about this.
There's also an important distinction between proof systems and "dependently typed languages" where proof systems restrict their power greatly so as to ensure the things which are proved in them are mathematically consistent while dependently typed languages which are more "practical" seek only to provide proof-like heuristic support to programming. In the former, you'll likely see a complex way of describing group theory in the language of program types and the program itself is irrelevant because its mere existence is sufficient for logical purposes. In the latter, you'll see a strong synthesis of a program and its internal logic as expressed by its types which ensure that invalid programs are wildly difficult to write as you'll likely have to abuse some crazy flaw in intuitionistic logic in order to do so.
The most canonical example is the fixed-length vector where you can write things like "append takes two vectors and results in one that's the sum of their lengths" and thus track (statically!) that you have no out of bounds errors possible in your program. It's also incredibly useful for getting nice properties like "this vector-of-vectors representation of a matrix is not ragged" confirmed at compile time... something that even an advanced non-dependently typed language like Haskell or OCaml is (mostly) strictly in the domain of runtime checking.
But, to solidify, mafribe is much more correct than my comment and there's, as far as I'm aware, a much larger menagerie of other type theories. The recent Homotopy Type Theory publication—which was on HN as notable due to its publication process—was yet another step in this direction.
The part i didn't get in the equivalence between program and proof, is that a function can be seen as a proof that provided the input parameters are of a given type, the output type is going to be that one. Quite simple in fact, but it only clicked right now :)
edit edit edit ./src/Browser
maybe annotate it with some smth
./verify some-property ./src/Browser.ml && echo 'seems OK, ship it!'
coq proof.coq > ./src/Browser.ml
How long do you think it's going to take before program formal proof becomes the new standard in commercial applications quality standard?
Long enough
As I understand it, creating a proof becomes increasingly more complex in proportion to program size. You'll notice in this project, their proof only covers a few hundred lines of code. That's not because their program just happened to be a few hundred lines of code, but because they designed it to allow a practical proof.
Isabelle/HOL - Coq competitor like GCC and LLVM (http://www.cl.cam.ac.uk/research/hvg/Isabelle/)
ATS - C with proof assistant (http://www.ats-lang.org/)
KeY - Java with verification annotations (http://www.key-project.org/)
https://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet
300,000 lines of code, still unfinished.
there already exists a system for verifying C, Astree (http://www.absint.com/astree/index.htm). Airbus, volkswagen, and similar companies use astree (they are, as I understand it, required to by EU law) to verify safety-critical software in their airplanes and cars. though astree has some large limitations on the C code it can verify, for example, no dynamically allocated memory or recursion.
investigating why it has these limitations is a good way to begin investigating what our current limitations are when formally reasoning about computer programs, and why C is so terrible to assure...
If I am not mistaken, Smallfoot is the basis for a professional product being developed by Monoidics (http://www.monoidics.com). Interestingly, the company was recently acquired by Facebook :)
Update: Here's a link with a list of related tools: http://www0.cs.ucl.ac.uk/staff/p.ohearn/Invader/Invader/Frie...
There's currently an attempt to formalize a subset of C, with an axiomatic semantics, all the way from specification down to machine language: http://vst.cs.princeton.edu/
Even if languages designed to abet formal proofs, like SPARK, were commonly used, proving anything but the most trivial properties requires a completely different mindset, significant additional training and experience. This puts formal proofs outside the abilities of the average engineer (including myself).
Finally, useful properties, like termination (lack of infinite loops/recursion), let alone termination within a time bound, or correctness with respect to non-trivial requirements is extremely difficult even for those with extensive experience in the area.
In addition to the difficulty of creating proofs, it is amazingly difficult to state non-trivial requirements formally and verify that the stated requirements are the right ones: often the source of the requirements (customers/users, supervisors, marketing) have neither motivation nor interest to state them formally or review formally stated requirements.
Are they OK with it, or do they just not see that they have a viable alternative at present?
I can think of numerous cases where from a personal and/or professional point of view I would have happily spent real money on upgraded/alternative software to what I've got if it fixed bugs that waste my time or make the results I get worse than they should be. Obviously some people will just rip off software whatever you do, but for paying customers, I'd be very surprised if quality alone couldn't drive a significant movement in a market, other things being equal.
I think it's all the unrelated things that aren't equal that are holding back that kind of competition. An interesting question is therefore at what point the willingness to use good software to develop more good software could cost less than putting up with poor quality incumbents, given that the real cost of both strategies is high. Even as a glass-half-full kind of guy, believing that a relatively small part of the industry could begin to pull that off without requiring the entire mainstream to shift, it would still have to involve far, far more people than are involved at the moment if we're going to create a sufficiently comprehensive foundation of development tools and essential libraries to bootstrap a whole quality-first ecosystem. The good news is that if you can establish that foundation, everything you do afterwards is easier in quality-first world has that advantage over the quick and dirty status quo, so momentum is on your side.
Just make better tools for Chrissakes.
Do you have a citation for this? Having spent plenty of time working around bugs in the older era of software development which took years to fix, I think your statement reflects nostalgia or inexperience. Those long, deliberative development cycles weren't some bygone golden age – and any codebase from that era has the thicket of "#ifdef BROKEN_SUNOS_FEATURE" blocks to prove it.
Having programmers use proof checkers to write proofs about their own software and then prove them is still very far away, if it'll ever happen at all. One can always dream happy dreams about the Curry-Howard Isomorphism, though.
The connection to formal verification is that dependent types (depending on how you do them) let you stuff custom computations into the type checking phase. The two coolest uses of dependent types (IMO) are to verify your code and, surprisingly, synthesize boilerplate.
(Btw, the guy making Ur/Web is quite important in the Coq community and Ur is one of his research vehicles for these ideas.)
Currently formal verification is complicated, expensive, and can only be used for verifying small amounts of code. And if you look at the places where it's highly valuable , i.e. security,hardware design and critical/medical systems - i don't see a wide deployment there. So not good signs.
And i heard of formal verification tools for c#, ada, and c/c++.
So, if they are similar pursuits, I can't help but imagine complete formal verification of large modern codebases would also be essentially computationally impossible.
What you may see more of is the approach taken in this project: Formally prove a tiny kernel that mediates system access, and sandbox everything else.
Though arguably, we're on our way to make that much easier through increasing support for varying levels of virtualization and finer grained authorisation (capabilities etc.), which means this approach will be able yield benefits even for software without a formal proof for the part that mediates system access.
BTW qubes-os is freely available , and i think is partly open-source.
Currently there are many different approaches to virtualization and I am bullish to application oriented approaches like App-V and ThinApp.
2) They didn't automatically verify the kernel. Coq is a proof assistant.
The point of the exercise is to prove that something like a file read cannot be invoked with bad files and cannot cause buffer overflows etc..
That doesn't require turing completeness.
Happy now?