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)