On 4/17/24 18:02, Isaac Beckett wrote: > Sorry, I should clarify. I meant making a dynamic OS that uses the sDDF. Not > on Microkit, since it’s not meant for that. But something that is more > flexible at runtime, designed for general purpose use so that it can load > components when they’re needed instead of having a fixed set of components > running at all times. > > So like, detecting a device being attached, and loading drivers for it from > the disk. Or loading an emulation layer/OS personality for another operating > system, like for Linux or Windows programs. > > While I was thinking of that I also got another idea. Some graphics cards > support technology similar to hardware virtualization extensions on CPUs, > such that they can be configured (with appropriate drivers, of course) to > behave as multiple logical devices on one physical device. The term for this > I believe is SR-IOV. > > Support for this is patchy, from what I hear, since this feature was > originally marketed for enterprise customers and not made available to > individuals, so setting it up involved (or used to involve) hacks to trick > the driver and/or firmware into allowing those features to be used. > > So I was thinking, it may make sense to write a smaller, simpler native > driver for seL4 that does very little but configure logical/virtual devices, > and then those can be given to either native drivers written from scratch, or > to ported Linux code, or to Linux VMs. Of course this doesn’t consider the > possibility (probably very likely) of hardware side channels in the GPU, but > then again neither does seL4.
If you are going to be using seL4 for serious work on an out-of-order CPU vulnerable to Spectre, and are not able to ensure that all memory containing potentially-sensitive data is marked as device memory, I recommend consulting with an expert on the CPU architecture in question to ensure that seL4 properly implements mitigations. Time protection is a principled solution to side-channel attacks, but it requires that the time consumed by operations on sensitive data is not observable. This may or may not be practical for a given workload. -- Sincerely, Demi Marie Obenour (she/her/hers) _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
