[seL4] Re: Question about LionsOS

I totally agree with the notion that we want to be able to run sel4 in a virtualized environment for development, debug, testing, and perhaps even production scenarios where that makes the most sense. However, as Gernot seems to be stressing, sel4 is supposed to be *secure* and that means the most minimal possible codebase, footprint, and dependencies. There is a danger that sel4 takes a hit for being insecure because habits develop using it in insecure configurations while claiming the sel4 gives security in ways it cannot do. I took a brief look at the Trademark Guidelines and it seems to me that at least in the spirit of the guidelines you can't put together something whose operation is suspect and still claim that it is 'sel4'. I'm a total copyright and patent abolitionist, but trademarks have their place and this is a good example of that. https://sel4.systems/Foundation/Trademark/ On Thu, Apr 18, 2024 at 3:51 PM Demi Marie Obenour wrote:

...

On 18 Apr 2024, at 20:38, Hugo V.C. wrote:

The challenge that I probably didn't expressed correctly, is to integrate seL4 on top of other dynamic systems (in example to virtualize a browser), as seL4 needs to know in advance how much memory will have available... Running seL4 on bare metal is a "kids game" (don't want to offend anyone), the challenge is to integrate it on systems where resources are dynamically assigned.

I don’t think I understand. Running seL4 in any way other than on bare

On 4/18/24 07:12, Gernot Heiser via Devel wrote: metal makes no sense whatsoever.

...

Gernot

I think the point is that if a system needs dynamic resource allocation, _something_ needs to do it. Traditional systems do this in the kernel. seL4 declares this to be the responsibility of userspace, but I’m not aware of a userspace component that can actually do that job.

Also, running seL4 in a virtualized environment makes a huge amount of sense for testing and debugging, or if one is shipping a virtual appliance. -- Sincerely, Demi Marie Obenour (she/her/hers)

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

-- Bob Trower --- From Gmail webmail account. ---