8 ms·

Quark: A secure Web Browser with a Formally Verified Kernel

296 points by hershel 13y ago

wslh 13y ago
How this secure approach benchmarks with Bromium micro hypervisor one?
- hershel 13y ago
  Don't know. bromium is interesting. Seems pretty similar to qubes-os. BTW qubes-os is freely available , and i think is partly open-source.
- X4 13y ago
  I initially thought that you were trolling, because Bromium sounds insincere, but it appears to be another startup funded by Andreessen Horowitz http://www.bromium.com/ http://www.bromium.com/ and it's not a Browser you've linked to, it's a hardware-software-policy solution for enterprises. Still interesting to know about.
  - wslh 13y ago
    Trolling? no, since I researched this market for my company and I found Bromium virtualization approach "unique", every new product following an innovative approach is interesting. Currently there are many different approaches to virtualization and I am bullish to application oriented approaches like App-V and ThinApp.
helloTree 13y ago
How does this work, if the kernel is supposed to be TM-complete?
- andor 13y ago
  1) The halting problem only states that you cannot create a program that can decide whether any given program will finish. It is possible for special cases, though. 2) They didn't automatically verify the kernel. Coq is a proof assistant.
  - DannyBee 13y ago
    The halting problem is also decidable for finite memory machine, like our real ones, so ...
    - cantankerous 13y ago
      Yes, but our memory is so big and our machines can have so many states that the problem is still intractable in the general case.
      - maaku 13y ago
        But still very much solvable in the specific domains of real world applications.
        cantankerous 13y ago
        You know what. I think I agree with you. I would actually go as far as to posit that most common applications don't require a Turing-Complete environment to run. If you could strip away the trouble spots and limit yourself to what you really need you can get a lot back in terms of software checking and assurance.
        shelf 13y ago
        http://www.cs.dartmouth.edu/~sergey/langsec/occupy/ http://www.cs.dartmouth.edu/~sergey/langsec/occupy/
        cantankerous 13y ago
        That's awesome. Thanks for sharing. It's nice to know that people a lot smarter than me are thinking about this already :).
- riffraff 13y ago
  I may be wrong, but AFAICT, the kernel in question is basically an API layer between the real browser and the OS. 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.
bsaul 13y ago
How long do you think it's going to take before program formal proof becomes the new standard in commercial applications quality standard? 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 ?
- hosay123 13y ago
  You should probably ask the people who've been promoting these ideas since at least the 70s :) "No time soon" is my best bet 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.
  - DebianUser 13y ago
    The theory which was promoted in the 70s (whatever it was) was certainly vastly different from what's used nowadays. Thierry Coquand (who conceived the original theory behind Coq) was only 9yo. In 1970.
- jbri 13y ago
  I think it's going to be a long time coming, since the negative effects of mostly-working-but-not-quite software tend to be borne by the purchaser and not the creator, which means the extra expense of formal verification is not commercially viable when compared to just having a rigorous (or not-so-rigorous) testing regime. 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.
  - 13y ago
alexanderri 13y ago
I don't really like that a "secure" browser run: 'xhost +' on my computer.
deleted 13y ago
[deleted]
s_q_b 13y ago
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."
- cliffu 13y ago
  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?).
  - mokus 13y ago
    > 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. [1] http://www.ertos.nicta.com.au/research/sel4/ http://www.ertos.nicta.com.au/research/sel4/
meta-coder 13y ago
The seL4 operating system microkernel also aims to be formally correct. http://www.ertos.nicta.com.au/research/l4.verified/ http://www.ertos.nicta.com.au/research/l4.verified/
RegEx 13y ago
Has anyone actually got this running yet? I'm using an Ubuntu 12 VM. I've spent about an hour trying to build this thing. The authors make it pretty clear in the INSTALL file that you're in for a fun time if things don't go according to plan. Maybe the process is seamless on Ubuntu 11. > 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 As for completing the rest of the install, you're on your own, as I was unable to get things working. The install script attempts to cd into some python-browser-8 directory which is supposed to have a makefile, but I never see it created or even attempted to be created.
- usethisonce 13y ago
  There is a Makefile in python-browser-8/.
  - RegEx 13y ago
    I did not see that directory at all. I tried to Grep to see if some process creates the directory, but I couldn't find it.
woah 13y ago
Does it support all the latest css3?
- Pitarou 13y ago
  Yes. Happy now?
sesm 13y ago
There is a typo in the paper, both 'Response Integrity' and 'Tab Non-Interference' are called 'second property'.
volokoumphetico 13y ago
is this like phantomjs fully headless?
deleted 13y ago
[deleted]

296 points by hershel 13y ago

wslh 13y ago

How this secure approach benchmarks with Bromium micro hypervisor one?

hershel 13y ago
Don't know. bromium is interesting. Seems pretty similar to qubes-os. BTW qubes-os is freely available , and i think is partly open-source.
X4 13y ago
I initially thought that you were trolling, because Bromium sounds insincere, but it appears to be another startup funded by Andreessen Horowitz http://www.bromium.com/ http://www.bromium.com/ and it's not a Browser you've linked to, it's a hardware-software-policy solution for enterprises. Still interesting to know about.
- wslh 13y ago
  Trolling? no, since I researched this market for my company and I found Bromium virtualization approach "unique", every new product following an innovative approach is interesting. Currently there are many different approaches to virtualization and I am bullish to application oriented approaches like App-V and ThinApp.

helloTree 13y ago

How does this work, if the kernel is supposed to be TM-complete?

andor 13y ago
1) The halting problem only states that you cannot create a program that can decide whether any given program will finish. It is possible for special cases, though. 2) They didn't automatically verify the kernel. Coq is a proof assistant.
- DannyBee 13y ago
  The halting problem is also decidable for finite memory machine, like our real ones, so ...
  - cantankerous 13y ago
    Yes, but our memory is so big and our machines can have so many states that the problem is still intractable in the general case.
    - maaku 13y ago
      But still very much solvable in the specific domains of real world applications.
      - cantankerous 13y ago
        You know what. I think I agree with you. I would actually go as far as to posit that most common applications don't require a Turing-Complete environment to run. If you could strip away the trouble spots and limit yourself to what you really need you can get a lot back in terms of software checking and assurance.
        shelf 13y ago
        http://www.cs.dartmouth.edu/~sergey/langsec/occupy/ http://www.cs.dartmouth.edu/~sergey/langsec/occupy/
        cantankerous 13y ago
        That's awesome. Thanks for sharing. It's nice to know that people a lot smarter than me are thinking about this already :).
riffraff 13y ago
I may be wrong, but AFAICT, the kernel in question is basically an API layer between the real browser and the OS. 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.

bsaul 13y ago

How long do you think it's going to take before program formal proof becomes the new standard in commercial applications quality standard? 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 ?

hosay123 13y ago
You should probably ask the people who've been promoting these ideas since at least the 70s :) "No time soon" is my best bet 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.
- DebianUser 13y ago
  The theory which was promoted in the 70s (whatever it was) was certainly vastly different from what's used nowadays. Thierry Coquand (who conceived the original theory behind Coq) was only 9yo. In 1970.
jbri 13y ago
I think it's going to be a long time coming, since the negative effects of mostly-working-but-not-quite software tend to be borne by the purchaser and not the creator, which means the extra expense of formal verification is not commercially viable when compared to just having a rigorous (or not-so-rigorous) testing regime. 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.
- 13y ago

alexanderri 13y ago

I don't really like that a "secure" browser run: 'xhost +' on my computer.

deleted 13y ago

[deleted]

s_q_b 13y ago

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

cliffu 13y ago
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?).
- mokus 13y ago
  > 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. [1] http://www.ertos.nicta.com.au/research/sel4/ http://www.ertos.nicta.com.au/research/sel4/

meta-coder 13y ago

The seL4 operating system microkernel also aims to be formally correct. http://www.ertos.nicta.com.au/research/l4.verified/ http://www.ertos.nicta.com.au/research/l4.verified/

RegEx 13y ago

Has anyone actually got this running yet? I'm using an Ubuntu 12 VM. I've spent about an hour trying to build this thing. The authors make it pretty clear in the INSTALL file that you're in for a fun time if things don't go according to plan. Maybe the process is seamless on Ubuntu 11. > 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 As for completing the rest of the install, you're on your own, as I was unable to get things working. The install script attempts to cd into some python-browser-8 directory which is supposed to have a makefile, but I never see it created or even attempted to be created.

usethisonce 13y ago
There is a Makefile in python-browser-8/.
- RegEx 13y ago
  I did not see that directory at all. I tried to Grep to see if some process creates the directory, but I couldn't find it.

woah 13y ago

Does it support all the latest css3?

Pitarou 13y ago
Yes. Happy now?

sesm 13y ago

There is a typo in the paper, both 'Response Integrity' and 'Tab Non-Interference' are called 'second property'.

volokoumphetico 13y ago

is this like phantomjs fully headless?

deleted 13y ago

[deleted]