At 2019-11-08T14:09:14+0800, 李庚 wrote: Hi Andrew! It's no bother--the mailing list is here to help people. I don't have any experience with VMWare but I suspect what you're seeing is not related to VMWare. The Docker page you mentioned first guides the reader through the build and execution of an seL4 project using the "sel4test" userspace. It is difficult to evaluate an operating system kernel, especially a microkernel, without giving it some tasks to run. sel4test is a userspace task whose job is to exercise the system and check whether it is operating successfully. sel4test produces a lot of output, and many diagnostic measures are emitted as the userspace code attempts to do many impossible things, like attempt to gain a capability to more memory than physically exists on the system, or prohibited things, like invoking a capability that does not exist. Many of these tests are present to (informally) verify the security properties of the system. The bottom line is that you will see many error messages; not all of them are failures per se. Similarly, you would not expect at a Unix shell session for an unpriviled user to be able to run superuser commands or inspect the memory of processes that belong to other users. The literal bottom line is that when sel4test is done running, you should see some output like this: Starting test 120: Test all tests ran Test suite passed. 120 tests passed. 48 tests disabled. All is well in the universe If you see "All is well in the universe" (as I just now confirmed on a build for the sabre platform with simulation enabled, so I could test the platform using QEMU instead of real hardware), then there is no reason to be alarmed by the error messages you are seeing--the system is working. I haven't deployed seL4 on a physical x86_64 machine myself, but seL4 supports that target and I've run sel4test and sel4bench (a benchmarking userspace) on QEMU-simulated x86_64 hardware many times. seL4 supports (U)EFI. Try having a look at https://docs.sel4.systems/GettingStarted.html . That page will take through an x86_64 build and run of sel4test. Regards, Branden