4 ms·
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 verifie
by _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 agoSee also: https://github.com/QubesOS/qubes-issues/issues/4318 https://github.com/QubesOS/qubes-issues/issues/4318.
- als0 6y agoThe 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.