Hello! Operating system noob here, I understand that in most mainstream
operating systems (Linux, BSDs, MacOS, Windows) drivers are part of the kernel.
And in micro kernel operating systems like Minix and seL4, drivers are part of
user space. But Minix is a lot closer to a traditional POSIX kernel, and seems
to implement some of that (IE posix threads, IPC) in the kernel, which makes
the environment for a driver programmer a bit more familiar. How do drivers
work in seL4, then? How does a driver obtain permission for hardware access
from the kernel? I imagine it works with a capability delegated by the root
task, but how do you solve chicken and the egg type problems, like loading
driver code, without driver code already loaded? Is it an initramfs like
Linux/Unix? Also, what if seL4 is being used _as_ the firmware/bootloader?
Obviously it can load the seL4 kernel and user space OS components from a file
system to put them in the booting OS’ memory, but how does it load drivers for
itself? I’m assuming there’s some low level platform specific code, but is that
code verified or part of the proofs?
_______________________________________________
Devel mailing list -- [email protected]
To unsubscribe send an email to [email protected]
