On 6/14/24 12:52, Peter Relich via Devel wrote:
Hello,
I am a researcher at Intellisense Systems, Inc. We are a small business that performs R&D for the U.S. Military. We have an active contractor to build a hypervisor for a microkernel. We recently selected Sel4 as the microkernel and I learned that the Army (our customer) used a camKes implementation of a VMM to host a fork of Ubuntu, but the limitations prompted them to try another approach. I think since that time, microkit has developed quite a bit and I saw the trustworthy systems has even been developing an operating system on the Sel4 microkernel. However, LionOS appears to be developed for ARM systems as the use case.
For the Army use, we are using a Nuvo7000LP: https://www.neousys-tech.com/Resource/Product_Document/Nuvo-7000LP/Nuvo-7000... Which is an X64 architecture.
I just started learning microkit through your available tutorials and I am aware that building a comprehensive VMM is no easy task. However, I was wondering if you had some intuition or if you could provide me an estimate of the libraries in the LionOS that I would need to adjust/redesign to make an X64 architecture fork? Is this even a feasible approach? It looks like I just need to swap out the aarch64 libraries with compatible x64 libraries and do some testing. Before I commit, I just wanted to get some advice on the endeavor.
Is forking LionOS to an X64 architecture feasible, or should I start at a lower level (i.e., redesigning the vmm?)
Do you need confidentiality? If so, kernel changes will be needed to mitigate speculation problems, unless you: 1. Enable IBPB on context switch. 2. Mark all memory that may contain sensitive data as device memory, therefore keeping it out of the kernel’s address space. This also means that kernel objects should not contain sensitive data. -- Sincerely, Demi Marie Obenour (she/her/hers)