4 ms·

I love qubes my only gripe is that they use the zen hypervisor instead of a minimal formally verified os such as sel4 which I think would go a long way in stren

by _kbh_ 6y ago

I love qubes my only gripe is that they use the zen hypervisor instead of a minimal formally verified os such as sel4 which I think would go a long way in strengthening the isolation between “domains/containers/etc”.

simonebrunozzi 6y ago
Xen, not Zen.
fsflover 6y ago
What are your problems with Xen? They explain their choice very well: https://www.qubes-os.org/faq/#why-does-qubes-use-xen-instead-of-kvm-or-some-other-hypervisor https://www.qubes-os.org/faq/#why-does-qubes-use-xen-instead....
- _kbh_ 6y ago
  SEL4 would be a better choice because it is formally verified, there is a much smaller chance of vulnerabilities in SEL4 vs Xen because of this.
  - fsflover 6y ago
    From the above link: What about safe languages and formally verified microkernels? In short: these are non-realistic solutions today. We discuss this in further depth in our Architecture Specification document: https://www.qubes-os.org/attachment/wiki/QubesArchitecture/arch-spec-0.3.pdf https://www.qubes-os.org/attachment/wiki/QubesArchitecture/a....
    - _kbh_ 6y ago
      Interestingly enough they only mention it being unreasonable for x86, it would be interesting to see SEL4 supported for ARM (of which SEL4 already has a verified kernel for).
      - fsflover 6y ago
        See also: https://github.com/QubesOS/qubes-issues/issues/4318 https://github.com/QubesOS/qubes-issues/issues/4318.
      - als0 6y ago
        The paper discusses more fundamental issues than just x86 architecture: * Usermode drivers need to be formally verified to prevent malicious DMA. Adding IOMMU/SMMU to the microkernel will complicate the current proofs. * All user processes that manage resources, like filesystem, network and memory management, must also be formally verified. These are currently unproven.