> which provides secure isolation of each individual driver
seL4 is great and all, but this is simply not possible as long as hardware devices can access memory. For example, a graphics driver can program the GPU to overwrite arbitrary system memory, regardless of how drivers are "isolated" by the kernel.
Comments
> which provides secure isolation of each individual driver
seL4 is great and all, but this is simply not possible as long as hardware devices can access memory. For example, a graphics driver can program the GPU to overwrite arbitrary system memory, regardless of how drivers are "isolated" by the kernel.
Unless there's a hardware IOMMU configured by Genode, Xen, etc, http://transpute.github.io/test1/related/