Hello,
during some experimental work on Genode/seL4 and VM extensions, I
encountered the issue to trigger a kernel fault.
The symptom seems, that if a thread invokes seL4_VMEnter, but the actual
thread is not meant/supposed to run a VM, the kernel will (ever?/may?)
page fault with a nullpointer access - which effectively renders the
whole Genode system unusable.
A partial log is attached based on Genode on x86_64 with seL4 kernel
version 9.0.1.
The fault address points to [0], where the variable _expected_vmcs_ is
null and the kernel de-references it. I put a message before this line
and print the value of the variable (as visible in the log below).
The seL4 10.0.0 code looks similar, so I presume the same issue there .
(if the code is not verified - which according to the roadmap is not the
case [1] ?)
Cheers,
Alex B.
[0]
https://github.com/seL4/seL4/blob/0dd40b6c43a290173ea7782b97afbbbddfa23b36/s...
[1] https://sel4.systems/Info/Roadmap/home.pml
--
Alexander Boettcher
Genode Labs
https://www.genode-labs.com - https://www.genode.org
Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth
diff --git a/src/arch/x86/object/vcpu.c b/src/arch/x86/object/vcpu.c
index cf74fa4..68a1dca 100644
--- a/src/arch/x86/object/vcpu.c
+++ b/src/arch/x86/object/vcpu.c
@@ -1540,6 +1540,7 @@ restoreVMCS(void)
}
#ifndef CONFIG_KERNEL_SKIM_WINDOW
+ userError("opps expected_vmcs=%p", expected_vmcs);
if (getCurrentCR3().words[0] != expected_vmcs->last_host_cr3) {
expected_vmcs->last_host_cr3 = getCurrentCR3().words[0];
vmwrite(VMX_HOST_CR3, getCurrentCR3().words[0]);
Boot config: parsing cmdline '/boot/sel4 disable_iommu'
Boot config: console_port = 0x1808
Boot config: debug_port = 0x1808
Boot config: disable_iommu = true
Detected 1 boot module(s):
module #0: start=0xfd58000 end=0xffff330 size=0x2a7330
name='/boot/image.elf'
Parsing GRUB physical memory map
Physical Memory Region from 0 size 89400 type 1
Physical Memory Region from 89400 size 16c00 type 2
Physical Memory Region from d2000 size 2000 type 2
Physical Memory Region from dc000 size 24000 type 2
Physical Memory Region from 100000 size bb17c000 type 1
Adding physical memory region 0x100000-0xbb27c000
Physical Memory Region from bb27c000 size 6000 type 2
Physical Memory Region from bb282000 size dd000 type 1
Adding physical memory region 0xbb282000-0xbb35f000
Physical Memory Region from bb35f000 size 12000 type 2
Physical Memory Region from bb371000 size 81000 type 4
Physical Memory Region from bb3f2000 size 1d000 type 2
Physical Memory Region from bb40f000 size 60000 type 1
Adding physical memory region 0xbb40f000-0xbb46f000
Physical Memory Region from bb46f000 size 1f9000 type 2
Physical Memory Region from bb668000 size 80000 type 4
Physical Memory Region from bb6e8000 size 27000 type 2
Physical Memory Region from bb70f000 size 8000 type 1
Adding physical memory region 0xbb70f000-0xbb717000
Physical Memory Region from bb717000 size 8000 type 2
Physical Memory Region from bb71f000 size 4c000 type 1
Adding physical memory region 0xbb71f000-0xbb76b000
Physical Memory Region from bb76b000 size c000 type 4
Physical Memory Region from bb777000 size 3000 type 3
Physical Memory Region from bb77a000 size 7000 type 4
Physical Memory Region from bb781000 size 1000 type 3
Physical Memory Region from bb782000 size 9000 type 4
Physical Memory Region from bb78b000 size 1000 type 3
Physical Memory Region from bb78c000 size 13000 type 4
Physical Memory Region from bb79f000 size 60000 type 3
Physical Memory Region from bb7ff000 size 1000 type 1
Adding physical memory region 0xbb7ff000-0xbb800000
Physical Memory Region from bb800000 size 800000 type 2
Physical Memory Region from bc000000 size 4000000 type 2
Physical Memory Region from e0000000 size 10000000 type 2
Physical Memory Region from feaff000 size 1000 type 2
Physical Memory Region from fec00000 size 10000 type 2
Physical Memory Region from fed00000 size 400 type 2
Physical Memory Region from fed1c000 size 4000 type 2
Physical Memory Region from fed20000 size 70000 type 2
Physical Memory Region from fee00000 size 1000 type 2
Physical Memory Region from ff000000 size 1000000 type 2
Physical Memory Region from 100000000 size 38000000 type 1
Adding physical memory region 0x100000000-0x138000000
Multiboot gave us no video information
ACPI: RSDP paddr=0xf68e0
ACPI: RSDP vaddr=0xf68e0
ACPI: RSDT paddr=0xbb7f07a2
ACPI: RSDT vaddr=0xbb7f07a2
***WARNING*** SKIM window not enabled, this machine is probably
vulernable to Meltdown (https://www.meltdownattack.com), consider enabling
Kernel loaded to: start=0x200000 end=0xaa5000 size=0x8a5000 entry=0x201209
ACPI: RSDT paddr=0xbb7f07a2
ACPI: RSDT vaddr=0xbb7f07a2
ACPI: FADT paddr=0xbb7f0a00
ACPI: FADT vaddr=0xbb7f0a00
ACPI: FADT flags=0xc2ad
ACPI: MADT paddr=0xbb7feb45
ACPI: MADT vaddr=0xbb7feb45
ACPI: MADT apic_addr=0xfee00000
ACPI: MADT flags=0x1
ACPI: MADT_APIC apic_id=0x0
ACPI: MADT_APIC apic_id=0x1
ACPI: MADT_APIC apic_id=0x4
ACPI: MADT_APIC apic_id=0x5
ACPI: MADT_IOAPIC ioapic_id=1 ioapic_addr=0xfec00000 gsib=0
ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0
ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd
ACPI: 4 CPU(s) detected
ELF-loading userland images from boot modules:
size=0x110f000 v_entry=0x2000018 v_start=0x2000000 v_end=0x310f000
p_start=0x10000000 p_end=0x1110f000
Moving loaded userland images to final location: from=0x10000000
to=0xaa5000 size=0x110f000
Starting node #0 with APIC ID 0
Mapping kernel window is done
Starting node #1 with APIC ID 1
Starting node #2 with APIC ID 4
Starting node #3 with APIC ID 5
Booting all finished, dropped to user space
virtual address layout of core:
overall [0000000000002000,00000000c0000000)
core image [0000000002000000,000000000310f000)
ipc buffer [000000000310f000,0000000003110000)
boot_info [0000000003110000,0000000003112000)
stack area [0000000040000000,0000000050000000)
boot module 'timer' (113344 bytes)
boot module 'test-vmm_sel4' (9912 bytes)
boot module 'config' (609 bytes)
boot module 'ld.lib.so' (937616 bytes)
boot module 'init' (352672 bytes)
Genode sculpt_vc-2-ge2fd5e5
2909 MiB RAM and 261141 caps assigned to init
...
<