On 10/18/22 18:09, Hugo V.C. wrote:
"So I'm interested in sel4 as I could run the processes in Linux VMs"
Sure, you can do it, but then the Linux Kernel becomes the weakest point and you have little or no control over it.
Ideally, I would not pass any sensible data flow to Linux, more over if there's any potential interaction with humans or something that can be manipulated by humans in any way. Any. Instead, use seL4 native app to do the sensible job and just use Linux for the "toys" (GUI, data rendering to human format, etc).
GUI and data rendering are not toys. In Qubes OS, the GUI is one of the core features, and a lot of work goes into making it secure. Control over the GUI allows presenting arbitrary forged information to the user and forging arbitrary user input (either directly or by tricking the user into entering it). This is a tremendous amount of control, and is often nearly equivalent to complete system compromise. Imagine a security system saying that the system was armed when it really was not, or a control station saying that everything is fine when something is about to explode.
In my security designs I do all sensible stuff in native seL4 apps then I have an spartan and very controlled interface with Linux VM. Don't let Linux handle sensible data flows... If you are dealing with humans, your options are either to give Linux control over the GUI or implement the entire GUI natively on seL4. If you choose the first route, you cannot prevent the Linux VM from being in a privileged position, but you can* make it very, *very* hard to attack. -- Sincerely, Demi Marie Obenour (she/her/hers)