Thank you Ivan! All that info sounds like what I was looking for. I'll do some experiments following your hints and if successful will let you know so maybe some one else can improve or take profit. I think Rust unikernels may be a good marriage for seL4... Best, El lun., 18 dic. 2023 1:38, Ivan Velickovic escribió:

Hello Hugo

There's a couple of things that could change from virtualising Linux to another kernel/OS.

The first goal would probably just to get the kernel booting, and for that you would want to know the conditions Hermit needs to be in before it can boot (e.g where in RAM it needs to be placed, does it expect any other artefacts such as a DTB or initrd to be placed in certain areas). Another point is that Linux expects its TCB to be setup with certain registers set to particular values before booting. For the specific conditions I believe Linux documents them (e.g https://www.kernel.org/doc/Documentation/arm64/booting.rst for ARM64).

If the conditions are different to Linux you would need to change the CAmkES VMM source code yourself. Looking at what the Hermit loader does might be a good first step.

At Trustworthy Systems we are using libvmm (https://github.com/au-ts/libvmm) and for fun I thought I'd try to get Hermit virtualised using it but I got stuck pretty quickly because I could not build Hermit, see https://github.com/hermit-os/hermit-rs-template/issues/51. In libvmm you can see what it's doing to setup Linux here https://github.com/au-ts/libvmm/blob/main/src/arch/aarch64/linux.c and here https://github.com/au-ts/libvmm/blob/main/src/guest.c#L6.

Thanks, Ivan

On 17/12/23 23:50, Hugo V.C. wrote:

...

[Some people who received this message don't often get email from skydivebcn@gmail.com. Learn why this is important at https://aka.ms/LearnAboutSenderIdentification ]

Hi all,

I'm wondering if someone could forward me to the path I must follow to achieve booting a Hermit unikernel ( https://github.com/hermit-os/hermit-rs) via CAmkES VMM. I know CAmkES VMM are "virtualised Linux guests on seL4 for ARM and x86 platforms" but I think that being able to boot a Rust based unikernel opens the door to a fascinating World... (no more dependency on "fat/buggy" Linux kernel).

Any help where I need to start? Does it require to modify CAmkES VMM to add such functionality?

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