search

microsoft / openvmm

Home of OpenVMM and OpenHCL.
http://openvmm.dev/
MIT License
1.36k stars 59 forks source link

seL4 / CAmkES support #163

Open ohault opened 1 day ago

ohault commented 1 day ago

For OpenVMM, but especially OpenHCL, support of seL4 micro kernel could be worth to consider.

Reference : https://sel4.systems

daprilik commented 1 day ago

In the sense of running seL4 as a Guest OS? If so, can you share what sort of issues are currently preventing the OS from running within OpenVMM?

ohault commented 1 day ago

In the sense of running seL4 as a Guest OS? If so, can you share what sort of issues are currently preventing the OS from running within OpenVMM?

I was thinking about why not relying on seL4 microkernel in place of the Linux kernel currently used in OpenHCL.

jstarks commented 1 day ago

It's an interesting idea. Currently, I anticipate that the in-development COCONUT kernel is better aligned with OpenHCL's goals. But it would be interesting to hear more about what it would look like to leverage seL4 instead.

(From a practical perspective, we really need an environment with Rust std support. I can't tell if that's an eventual goal of the Rust-seL4 project.)

romank-msft commented 1 day ago

+1 to what John said. To add my one cent, folks who presented LVBS (https://lpc.events/event/17/contributions/1515/, running the Linux kernel in VTL1, here we have VTL2) looked into using Op-TEE, and decided to rely on the Linux kernel and our VSM patches for the time being as the dev tooling and perf testing tooling didn't look as evolved as in Linux.