Hello,
I am the maintainer of the Qubes + Whonix project...
https://www.whonix.org/wiki/Qubes
Which is the port of Whonix OS (think a more secure Tor proxied VM) to Qubes OS, which has upstream integration into the Qubes codebase now.
I am very interested in secure minimal kernels and hypervisors, and have been discussing these topics publicly and privately with other interested developers and investors recently.
And I am also positioning to bring development resources to low-level projects that can achieve a more optimal (and verifiable) secure TCB than bloated Linux-based systems, as Qubes Dom0 is currently based upon.
Actually being able to read through and know all the code that is running on a mission critical machine, a novel thought, huh. ;)
I am most interested in this Qubes blurb on the seL4 website...
https://sel4.systems/GettingStarted
"Qubes is an open source operating system designed to provide strong security for desktop computing using virtualisation to provide isolation. Qubes is based on Xen. seL4 is a much better fit for Qubes. The project is to port Qubes to seL4 (or develop an alternative Qubes-like system for seL4)."
I absolutely agree with this and would like to know more about what Qubes development project might already underway be in the seL4 community in order to consider the opportunity of providing some real assistance in the future.
What's the status of this seL4 Qubes port project and who can I get in touch with to talk more about accomplishing it?
Thanks! :)
WhonixQubes
Hi WhonixQubes, I don't have too much to add, but I wanted to throw in my support: I'm very interested in seeing qubes or something very much like it on top of sel4.
There is another, similar project using genode which places virtualbox on top of the nova ukernel to have VMs run with a smaller TCB in isolated processes. Though thats still a bit different than what qubes gives you, and although the TCB is smaller, none of it is proven.
On Wed, Mar 18, 2015 at 4:35 AM, WhonixQubes whonixqubes@riseup.net wrote:
Hello,
I am the maintainer of the Qubes + Whonix project...
https://www.whonix.org/wiki/Qubes
Which is the port of Whonix OS (think a more secure Tor proxied VM) to Qubes OS, which has upstream integration into the Qubes codebase now.
I am very interested in secure minimal kernels and hypervisors, and have been discussing these topics publicly and privately with other interested developers and investors recently.
And I am also positioning to bring development resources to low-level projects that can achieve a more optimal (and verifiable) secure TCB than bloated Linux-based systems, as Qubes Dom0 is currently based upon.
Actually being able to read through and know all the code that is running on a mission critical machine, a novel thought, huh. ;)
I am most interested in this Qubes blurb on the seL4 website...
https://sel4.systems/GettingStarted
"Qubes is an open source operating system designed to provide strong security for desktop computing using virtualisation to provide isolation. Qubes is based on Xen. seL4 is a much better fit for Qubes. The project is to port Qubes to seL4 (or develop an alternative Qubes-like system for seL4)."
I absolutely agree with this and would like to know more about what Qubes development project might already underway be in the seL4 community in order to consider the opportunity of providing some real assistance in the future.
What's the status of this seL4 Qubes port project and who can I get in touch with to talk more about accomplishing it?
Thanks! :)
WhonixQubes
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
On 2015-03-18 16:32, Tim Newsham wrote:
Though thats still a bit different than what qubes gives you, and although the TCB is smaller, none of it is proven.
Which, just to nitpick, it is neither for seL4. Unless you plan to run your code on an "imx31 platform, arm1136jf-s CPU, ARMv6 architecture" [0]. I'm not sure that this is feasible for any serious workload.
I'm just saying as people tend to forget that and expect the proof to hold for all platforms and all systems. This is not the case.
- Marcus
"Which, just to nitpick, it is neither for seL4" -- a fine nit to pick
and I don't think seL4 should be over-sold... But I do think there is great benefit to formal verification beyond just the certificate at the end. Although various ports might have introduced subtle flaws that have not been shaken out by formal verification (yet?), at least large portions of the code base have been through the verification process. And that process has removed bugs from that code. The lack of memory corruption issues, integer overflows, undefined C behaviors, etc. in that code should benefit even the unproven ports.
On Wed, Mar 18, 2015 at 8:59 AM, Marcus Hähnel marcus@mh-development.info wrote:
On 2015-03-18 16:32, Tim Newsham wrote:
Though thats still a bit different than what qubes gives you, and although the TCB is smaller, none of it is proven.
Which, just to nitpick, it is neither for seL4. Unless you plan to run your code on an "imx31 platform, arm1136jf-s CPU, ARMv6 architecture" [0]. I'm not sure that this is feasible for any serious workload.
I'm just saying as people tend to forget that and expect the proof to hold for all platforms and all systems. This is not the case.
- Marcus
[0] http://sel4.org/FAQ/#whichcode
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
On 19/03/15 02:59, Marcus Hähnel wrote:
On 2015-03-18 16:32, Tim Newsham wrote:
Though thats still a bit different than what qubes gives you, and although the TCB is smaller, none of it is proven.
Which, just to nitpick, it is neither for seL4. Unless you plan to run your code on an "imx31 platform, arm1136jf-s CPU, ARMv6 architecture" [0]. I'm not sure that this is feasible for any serious workload.
I should point out that while the current proofs for seL4 hold only for this platform, that "porting" them to similar platforms we know will be relatively straightforward.
Gerwin Klein can elaborate if needed, but I think we can say with confidence that moving the proofs over to e.g. the SABRE Lite (imx6, ARMv7 platform) would require relatively little effort -- it's just not a high priority for us at the moment.
We do expect to move the proofs to a newer ARM platform in the future.
Moving to another architecture, like x86, is of course another matter altogether.
Cheers
Toby
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
On 19 Mar 2015, at 2:01 am, Toby Murray Toby.Murray@nicta.com.au wrote:
On 19/03/15 02:59, Marcus Hähnel wrote:
On 2015-03-18 16:32, Tim Newsham wrote:
Though thats still a bit different than what qubes gives you, and although the TCB is smaller, none of it is proven.
Which, just to nitpick, it is neither for seL4. Unless you plan to run your code on an "imx31 platform, arm1136jf-s CPU, ARMv6 architecture" [0]. I'm not sure that this is feasible for any serious workload.
I should point out that while the current proofs for seL4 hold only for this platform, that "porting" them to similar platforms we know will be relatively straightforward.
Gerwin Klein can elaborate if needed, but I think we can say with confidence that moving the proofs over to e.g. the SABRE Lite (imx6, ARMv7 platform) would require relatively little effort -- it's just not a high priority for us at the moment.
In fact, we expect to be able to release the proof for imx6 later this year.
Cheers, Gerwin
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Well great to receive such info and encouragement. :)
Yup, I am very aware of what's happening on the Qubes end with R3 HAL, etc.
And thanks for the status overview on the components. That gives me a better sense of things.
I'm going to start playing with seL4 on my machine soon, and will orient myself further with things in the seL4 project.
Also saw that x64 support has been worked on, but maybe not not currently active.
I am continuing to position things for a future micro-Qubes-like project of this kind, with dev funding associated. So something will probably happen on my end in the future that may end up complimenting or integrating with the current work on seL4.
Thanks!
WhonixQubes
Hi,
This past (southern hemisphere) summer at NICTA we've had a student start work on a port of Qubes to seL4 . This work mainly focussed on providing the seL4 backend support needed for the Qubes R3 Hypervisor-Abstraction-Layer (see [1][2][3] for some info about the HAL and backend support it requires). The status of the project at the moment is that we have support for inter-VM communication using vchan and qrexec, and a very simple libvirt wrapper (that doesn't do much yet).
However there is still a bunch work to do in getting much of the libvirt functionality (managing VMs including creating and destroying VMs at runtime) working, and then getting the rest of Qubes running based on this backend support.
Ihor
[1] http://theinvisiblethings.blogspot.com.au/2013/03/introducing-qubes-odyssey-... [2] http://theinvisiblethings.blogspot.com.au/2013/06/qubes-os-r3-alpha-preview-... [3] http://theinvisiblethings.blogspot.com.au/2014/11/qubes-r3odyssey-initial-so...
-
Gerwin Klein -
Ihor Kuz -
Marcus Hähnel -
Tim Newsham -
Tim Newsham -
Toby Murray -
WhonixQubes