"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). 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... Just an idea... hope it helps. El mar., 18 oct. 2022 22:30, Gernot Heiser escribió:

On 9 Oct 2022, at 19:51, James Hillman wrote:

...

Hi Sel4 developers,

I am new to this forum and hoping this is the right place to bounce my project idea off. I typically use FPGA to enforce security in my products but there are lots of reasons why FPGAs are not suitable for all use

...

I have also used low end microcontroller where one can review all the code to understand the security risks.

My latest project however involves two USB processes (one for each

...

connection) with high throughput expectations. And to pass data streams at high typical throughput between them. Due to the wide range of USB type of devices I fear this would be too much code to review - it feels very OS like. Note, I don't need a GUI, it's headless.

So I'm interested in sel4 as I could run the processes in Linux VMs if I understand sel4 correctly. And whilst it's not the smallest processors I think they need to be more powerful to support the speeds. So this is fine . I am unsure how much of this project is already done, mainly thinking

cases. physical the

...

usb driver perspective.

encapsulating drivers/protocol stacks into VMs is a standard design pattern. The seL4 Device Driver Framework will explicitly support this for Linux drivers, but it’s not going a high-performance approach…

Gernot

_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

Hi Marie! "GUI and data rendering are not toys." Ok, maybe "toys" was not the best word. But from my point of view (attacker side) GUIs are (usually) almost impossible to be secured due to it´s complexity and so I tend to see real all life implementations as "toys" that can be broken easily. " 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 (...)" Yes, I know Qubes OS, is my default OS for sensible stuff (best option nowadays IMHO). Anyway, as you probably remember, I hacked Qubes last year and forged information flowing from one VM to another VM: "Qubes File transfer tamper" https://www.youtube.com/watch?v=gcEq2hAvKSM of course this has nothing to do with forging information i the GUI of Dom0 or GUI VM (i new versions of Qubes OS), but is shows how easy is to forge information in a VM GUI. In the above example we have a file transfer between 2 VMs whose content is forged in real time. Here the "hack" was just a simulation where I artificially manipulated the file transfer mechanism but it is enough to show that (nowadays) GUIs of standard OSs can´t be trusted. No matter how much effort you put in there. If you harden the file transfer, then the file can be manipulated at the end point, either its contents or either it´s presentation (I hope no one dares to "prove" security of Xorg or any other common X window system... it is impossible that humans deal with such monsters). So, what the end user "sees" in the screen nowadays is just a joke as everything can be manipulated. As far I have learned, if you want to secure what humans "see" in a screen, then you need a very simple presentation schema. When you go for complex representations of information then the game is over because no matter how much you protect the source and the channel, whenever the information is processed in a non verified big OS then there are many ways to forge information because the are many bugs in such big OS that can be exploited. The easiest way explain this is: figure out how you can secure rendering software for: PDFs, docs in all its formats..., images, videos,.... too many people in the party so it becomes impossible. I can accept that you can try to build a "secure Linux GUI system" where, in example, you just set up kernel + Xorg + your own PDF renderer/"transformer" (transforming to image is becoming a trend). Anyway, even in such ideal system, still kernel and Xorg are out of your control and I hope you don´t user tcp/ip stack for nothing and just build your own VMs transfer mechanism (like in Qubes OS). "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." I would never use a generic OS with a a generic software/interface to video output to say "system is armed", instead I would make it as simple as possible. In example red/green light activated via GPIO. El mié, 19 oct 2022 a las 1:34, Demi Marie Obenour () escribió:

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)

"My intention was to use a minimum image with no UI but importantly the USB drivers/stack." Sure. This is a common approach and default VMs examples of seL4 tutorials are exactly that: a kernel + busybox, so no UI. Still this is just Linux with a very big kernel... El mié., 19 oct. 2022 6:37, escribió:

Thanks everyone, really enjoy reading the discussion. Sorry for the lazy untargetted use of the word Linux. My intention was to use a minimum image with no UI but importantly the USB drivers/stack.

I guess the key issue is what the best data rate I could hope for between the VMs. _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

" So I was assuming the isolation between VMs are more assured using sel4." Yes. isolation is what is guaranteed and proved by seL4. This is the "magic" of having it´s code formally verified and what makes the difference with any other solution, in terms of isolation. "In itself I am not worried if the VM is compromised." Then go ahead. But remember that if VM is compromised then the solution is compromised. So if you need to sell/distribute this solution you will need to argue to your customers/users why you don´t care about VM compromise... "Perhaps I could get usb stack ported natively... " Anything you strip down from the VMs and port it to native code you get a giant improvement in terms of security. El mié, 19 oct 2022 a las 7:54, escribió:

Hugo V.C. wrote:

...

"My intention was to use a minimum image with no UI but importantly the USB drivers/stack."

Sure. This is a common approach and default VMs examples of seL4 tutorials are exactly that: a kernel + busybox, so no UI. Still this is just Linux with a very big kernel...

El mié., 19 oct. 2022 6:37, <james.hillman07(a)gmail.com> escribió:

...

Thanks everyone, really enjoy reading the discussion. Sorry for the lazy untargetted use of the word Linux. My intention was to use a minimum image with no UI but importantly the USB drivers/stack.

I guess the key issue is what the best data rate I could hope for between the VMs. _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems

So I was assuming the isolation between VMs are more assured using sel4. In itself I am not worried if the VM is compromised. Perhaps I could get usb stack ported natively...

---

Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

"I think my use case the system gets reset (read only os) on every use and a typical use time is perhaps a few minutes." Nice. Read only systems are better than those who allow permanent changes. Anyway (and excuse me, I really don´t want to look pedant) from attackers point of view, this is almost irrelevant. Moreover, those read only systems are usually perfect systems for exploits as are static so debug and development of exploits is easier than dynamic systems. I mean, I agree read only is better than writable as every reboot is a new clean environment. Anyway.... when you plan an attack (talking from my own experience) if you have a read only static system then you know you need to create a one shot exploit or chain-exploit "fire and forget"... that is, it must autonomously and blindly work and in the time windows you have. Here the time window is the critical point and every scenario will be different. Again, anyway, in computing "few minutes" is an entire life... unless the attacker plans to steal 100GB of data, leaking documents can be done in a matter of seconds. Remember an exploit is not a VNC/RDP where attacker do things manually, it is code that runst as fast as CPU allows, so if the attack is targeted and well planned, minutes are a glorious amount of time (in the past I´ve been fighting in terms of milliseconds in some race conditions exploits....). I just give you some information and excuse me in advance if I misunderstood some details of your specific environment, it is difficult to evaluate stuff in a so generic explanation. "In terms of minimising the impact of comprimise I'm thinking of using three VMs - insecure/comprimise exposed, a "between states" VM which would enforce data flow syntax/packet checking between the other two VMs, and a secure/trusted VM." Without details of the implementation I can´t say too much about this even if I guess that what you are trying sounds good. It all depends on the design... My only advice is to get as much info you can from offensive profiles, think out of the box, minimize the attack surface and makes things as simple as possible. And if things must be ugly to be secure then make them ugly. El mié, 19 oct 2022 a las 10:00, escribió:

...

" So I was assuming the isolation between VMs are more assured using sel4."

Yes. isolation is what is guaranteed and proved by seL4. This is the "magic" of having it´s code formally verified and what makes the difference with any other solution, in terms of isolation.

"In itself I am not worried if the VM is compromised."

Then go ahead. But remember that if VM is compromised then the solution is compromised. So if you need to sell/distribute this solution you will need to argue to your customers/users why you don´t care about VM compromise...

"Perhaps I could get usb stack ported natively... "

Anything you strip down from the VMs and port it to native code you get a giant improvement in terms of security.

El mié, 19 oct 2022 a las 7:54, <james.hillman07(a)gmail.com> escribió:

...

Hugo V.C. wrote: "My intention was to use a minimum image with no UI but importantly the USB drivers/stack."

Sure. This is a common approach and default VMs examples of seL4 tutorials are exactly that: a kernel + busybox, so no UI. Still this is just Linux with a very big kernel...

El mié., 19 oct. 2022 6:37, <james.hillman07(a)gmail.com> escribió:

...

Thanks everyone, really enjoy reading the discussion. Sorry for the lazy untargetted use of the word Linux. My intention was to use a minimum image with no UI but importantly the USB drivers/stack.

I guess the key issue is what the best data rate I could hope for between the VMs. _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems

So I was assuming the isolation between VMs are more assured using sel4. In itself I am not worried if the VM is compromised. Perhaps I could get usb stack ported natively... _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems

Thanks for confirming and continuing the discussion. I think my use case

Hugo V.C. wrote: the system gets reset (read only os) on every use and a typical use time is perhaps a few minutes. In terms of minimising the impact of comprimise I'm thinking of using three VMs - insecure/comprimise exposed, a "between states" VM which would enforce data flow syntax/packet checking between the other two VMs, and a secure/trusted VM. _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems