sel4 / sel4_projects_libs

seL4_projects_libs

seL4 Projects Libraries

A collection of libraries for seL4. These libraries are compatible with seL4_libs.

Contributing

Contributions welcome!

See the CONTRIBUTING file for more.

sel4_projects_libs's Issues

libsel4vm: set VM_GUEST_ERROR_EXIT on vCPU index error?

I wonder, in

seL4_projects_libs/libsel4vm/src/arch/arm/vm.c

Lines 234 to 241 in 9de0630

	tag = seL4_Recv(vm->host_endpoint, &sender_badge);
	label = seL4_MessageInfo_get_label(tag);
	if (sender_badge >= MIN_VCPU_BADGE && sender_badge <= MAX_VCPU_BADGE) {
	seL4_Word vcpu_idx = VCPU_BADGE_IDX(sender_badge);
	if (vcpu_idx >= vm->num_vcpus) {
	ZF_LOGE("Invalid VCPU index. Exiting");
	ret = -1;
	} else {

shouldn't this also set

vm->run.exit_reason = VM_GUEST_ERROR_EXIT;

if vcpu_idx is invalid?

libvchan.h includes <linux/types.h>

libvchan.h includes <linux/types.h> which causes it to fail to compile in my environment. It seems like this include is only used to get size_t so it can be replaced by <stddef.h> instead.

delete merged branches

There are a lot of branches that look as if the work has been merged. Could you remove them here?

• missing-lincenses
• spdx
• spdx-syntax
• alyons-ppi
• kent/fix-style
• kent/rockpro64
• kent/remove-warning
• nomadeel/fdt-fix

github CI job 'trigger' should not run on forks

github CI job 'trigger' should not run on forks, as this fails when updating master there:

Run seL[4](https://github.com/axel-h/seL4_projects_libs/runs/5490887825?check_suite_focus=true#step:2:4)/ci-actions/trigger@master
/home/runner/work/_actions/seL4/ci-actions/master/js/../trigger/steps.sh
Need $INPUT_TOKEN for authentication.
Error: Action trigger failed.

libsel4arm-vmm: add support for decoding and emulating arm instructions

(Moved from: https://sel4.atlassian.net/browse/SELFOUR-793)
Currently libsel4arm-vmm provides basic support for decoding and emulating faults for the TK1. This works by relying on the HSR register providing a valid instruction syndrome.

From the armv7 manual:

"A valid instruction syndrome provides information that can help a hypervisor to emulate the

instruction efficiently. Instruction syndromes are returned for instructions for which such

accelerated emulation is possible."

The syndrome contains what register is used for the read/write, what the width of the data is, whether it needs to be sign extended. This makes the fault easy to decode and emulate which libsel4arm-vmm currently does.

However a valid syndrome only occurs for a subset of arm data instructions. For instructions outside of this the instruction needs to be decoded and properly emulated (such as handling register write back where the second register that holds the address of the lookup is updated with the immediate offset such as pop and push instructions). Currently this is not supported.

This only becomes a problem when the vmm wants to trap and emulate faults. Memory protection faults that result in needing to map a page into the mmu doesn't require decoding any instructions because the fault address is stored in a different register and the fault is normally handled by mapping in a page and then restarting the faulting instruction rather than advancing the fault instruction which requires the instruction to be emulated.

We currently use trap and emulation for providing more granular memory access control than the frame level. Up until now this lack of support hasn't been an issue but could become an issue in the future.

Investigate VMM issues with GCC8.4 at "-o3"

Follow-up from commit 0f9286d of #16 for libsel4vm/src/arch/x86/guest_x86_context.c:

/* Under release mode, this file will get built using -O3. Howerver on gcc 8.4,
 * the -O3 optimisation level is too aggressive and causes issues for the guest
 * VM. Hence, instead of using -O3 we use -O2 to avoid the issue. */

gic_dist_map define error, not work

truct gic_dist_map {
uint32_t enable; /* 0x000 /
uint32_t ic_type; / 0x004 /
uint32_t dist_ident; / 0x008 */

uint32_t res1[29];                                  /* [0x00C, 0x080) */

uint32_t irq_group0[CONFIG_MAX_NUM_NODES];          /* [0x080, 0x84) */
uint32_t irq_group[31];                             /* [0x084, 0x100) */
uint32_t enable_set0[CONFIG_MAX_NUM_NODES];         /* [0x100, 0x104) */
uint32_t enable_set[31];   

irq_group0, enable_set0 is not mean work muti core, this will not work OK
for examp:
For interrupt ID m, when DIV and MOD are the integer division and modulo operations:
the corresponding GICD_ISENABLER number, n, is given by n = m DIV 32
the offset of the required GICD_ISENABLER is (0x100 + (4*n))
the bit number of the required Set-enable bit in this register is m MOD 32.

Document difference between this repository and seL4_libs

It is not clear how this repository compares with seL4_libs. I know that seL4_libs is (or at least was) not considered to be of production quality, for example.

libsel4vmmplatsupport: virtio_net driver lacks support for IO control to change MAC address

Follow-up from https://lists.sel4.systems/hyperkitty/list/[email protected]/thread/YNTMEMTAUD5ZE6X7J4O4E75OELA6T345/

The error

Unhandled offset of 0x14 of size 1, writing 0x2
Assertion failed: !"panic" 
seL4_projects_libs/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c: emul_io_out: 109

Seem to indicate that the virtio_net driver of the libsel4vmmsupport does not support IO control for changing the MAC addess of the virtio net in the guest.

sel4vm: Switch to use ```seL4_LargePageObject``` in VM's RAM register to reduce the memory overhead

I was working around with the default vm_minimal for qemu-arm-virt 64bits platform and tried to allocate 2GB RAM for the VM linux and got some allocation fail error.

./simulate: QEMU command: qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -nographic  -m size=4096  -kernel images/capdl-loader-image-arm-qemu-arm-virt 
ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4
  paddr=[c1b39000..c2fa90d7]
No DTB passed in from boot loader.
Looking for DTB in CPIO archive...found at c1c94cc8.
Loaded DTB from c1c94cc8.
   paddr=[c0242000..c0243fff]
ELF-loading image 'kernel' to c0000000
  paddr=[c0000000..c0241fff]
  vaddr=[80c0000000..80c0241fff]
  virt_entry=80c0000000
ELF-loading image 'capdl-loader' to c0244000
  paddr=[c0244000..c173cfff]
  vaddr=[400000..18f8fff]
  virt_entry=408d88
Enabling hypervisor MMU and paging
Jumping to kernel-image entry point...

Bootstrapping kernel
Warning: Could not infer GIC interrupt target ID, assuming 0.
available phys memory regions: 1
  [c0000000..140000000]
reserved virt address space regions: 3
  [80c0000000..80c0242000]
  [80c0242000..80c0243ddc]
  [80c0244000..80c173d000]
Booting all finished, dropped to user space
<<seL4(CPU 0) [decodeUntypedInvocation/205 T0x813f813400 "rootserver" @4006f8]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>>
[email protected]:1332 Invalid 'num_vcpus' attribute setting: Exceeds maximum number of supported nodes. Capping value to CONFIG_MAX_NUM_NODES (1)
[email protected]:704 module name: map_frame_hack
[email protected]:704 module name: init_ram
ram_ut_alloc_iterator@guest_ram.c:304 Failed to allocate page
map_vm_memory_reservation@guest_memory.c:477 Failed to get frame for reservation address 0x8e83a000
Loading Kernel: 'linux'
Loading Initrd: 'linux-initrd'
Loading Generated DTB
vm_ram_touch@guest_ram.c:165 Failed to touch ram region: Not registered RAM region
32 bit ARM insts not decoded
--------
Pagefault from [vm0]: write fault @ PC: 0xffff0000083bd92c IPA: 0xbffff000, FSR: 0x92000046
Context:
x0: 0xffff7dfffe63b000
x1: 0x0
x2: 0xfc0
x3: 0x4
x4: 0x0
x5: 0x40
x6: 0x3f
x7: 0x0
x8: 0xffff7dfffe63b000
x9: 0x0
x10: 0x40000000
x11: 0x0
x12: 0x3
pc: 0xffff0000083bd92c
x14: 0x0
sp: 0xffff000008e00000
spsr: 0x40000085
x13: 0xffff000008f7b530
x15: 0x18
x16: 0x1800
x17: 0x8b0
x18: 0xffffffffffffffff
x19: 0xbffff000
x20: 0xffff000008e08000
x21: 0xffff000008e4b308
x22: 0xffff7dfffe800000
x23: 0xffff000008e08000
x24: 0x0
x25: 0x0
x26: 0x0
x27: 0x0
x28: 0x40a50018
x29: 0xffff000008e03e60
x30: 0xffff000008a56160
m--------
Assertion failed: rt >= 0 (/host/projects/seL4_projects_libs/libsel4vm/src/arch/arm/fault.c: fault_get_width: 620)

I found that it was caused by that the static memory pool of allocman was consumed up. Then I mentioned that the static memory pool was predefined default to 80MB size. (https://github.com/seL4/camkes-vm/blob/master/templates/seL4AllocatorMempool.template.c#L9)

I tried to add it to 140MB and VM Linux was boot successed. But 140MB / 2GB is an unexpected proportion to me.

Then I dived into the details of the related codes and found the default allocator for untyped frames is Buddy like and the RAM allocation is at a 4K granularity.
https://github.com/seL4/seL4_libs/blob/master/libsel4allocman/src/utspace/split.c

seL4_projects_libs/libsel4vm/src/guest_ram.c

Line 292 in 9736082

int page_size = seL4_PageBits;

With this, a 2GB RAM region will need (2GB / 4KB) * 2 * (sizeof(node) + overload) = 120MB memory.

Here we may switch to use seL4_LargePage in VM RAM register, and the allocation granularity is 2M, and reduce the memory overhead to 120MB / 512 size.

libsel4vmmplatsupport: unaligned PCI BAR address (x86, PCI pass-through)

Hi,

I think I may have found a bug in vmm_pci_helper_map_bars from libsel4vmmplatsupport/src/arch/x86/drivers/vmm_pci_helpers.c.

The PCI interface standard mandates that BAR addresses be naturally aligned, i.e. the address must be a multiple of the size. This is a requirement for the weird BAR size probing logic (save value, write 0xffffffff, read back size mask, restore value) to function properly. The vmm_pci_helper_map_bars function however calls vm_reserve_anon_memory to reserve memory in the guest space and this function does not (necessarily) returns naturally aligned addresses.

I ran into this using qemu. Simple CAmkES setup with a single Linux VM, with PCI pass-throughs for both a virtio-net and a e1000 network interfaces. At boot, the PCI bus is correctly scanned as such:

lib_pci_scan_dev found pci device 0 0
PCI :: 00.00.00 : intel Unknown device ID. (vid 0x8086 did 0x29c0) line0 pin0
lib_pci_scan_dev found pci device 0 1
PCI :: 00.01.00 : Unknown vendor ID. Unknown device ID. (vid 0x1234 did 0x1111) line0 pin0
    BAR0 : [ mem 0xfd000000 sz 0x1000000 szmask 0xff000000  prefetch ]
    BAR2 : [ mem 0xfebf0000 sz 0x1000 szmask 0xfffff000   ]
lib_pci_scan_dev found pci device 0 2
PCI :: 00.02.00 : Unknown vendor ID. Unknown device ID. (vid 0x1af4 did 0x1000) line11 pin1
    BAR0 : [ io 0xc080 sz 0x20 szmask 0xffffffe0 ]
    BAR1 : [ mem 0xfebf1000 sz 0x1000 szmask 0xfffff000   ]
    BAR4 : [ mem 0xfe000000 sz 0x4000 szmask 0xffffc000 64bit prefetch ]             /* size: 0x4000 */
lib_pci_scan_dev found pci device 0 3
PCI :: 00.03.00 : intel Unknown device ID. (vid 0x8086 did 0x100e) line11 pin1
    BAR0 : [ mem 0xfebc0000 sz 0x20000 szmask 0xfffe0000   ]                         /* size: 0x20000 */
    BAR1 : [ io 0xc000 sz 0x40 szmask 0xffffffc0 ]
lib_pci_scan_dev found pci device 0 31
PCI :: 00.1f.00 : intel intel_ich9_8 (vid 0x8086 did 0x2918) line0 pin0
lib_pci_scan_dev found multi function device 0 31
PCI :: 00.1f.02 : intel Unknown device ID. (vid 0x8086 did 0x2922) line10 pin1
    BAR4 : [ io 0xc0a0 sz 0x20 szmask 0xffffffe0 ]
    BAR5 : [ mem 0xfebf2000 sz 0x1000 szmask 0xfffff000   ]
PCI :: 00.1f.03 : intel intel_ich9_6 (vid 0x8086 did 0x2930) line10 pin1
    BAR4 : [ io 0x700 sz 0x40 szmask 0xffffffc0 ]

The issue shows up with BAR4 of PCI device 00.02.00 (virtio-net) as well as BAR0 of PCI device 00.03.00 which have sizes larger than one page. Here's what the guest Linux kernel finds:

[    0.190000] pci 0000:00:00.0: [5e14:0042] type 00 class 0x060000
[    0.190000] pci 0000:00:01.0: [1af4:1000] type 00 class 0x020000
[    0.200000] pci 0000:00:01.0: reg 0x10: [io  0xc080-0xc09f]
[    0.210000] pci 0000:00:01.0: reg 0x14: [mem 0x18001000-0x18001fff]
[    0.210000] pci 0000:00:01.0: reg 0x18: [mem 0x18002000-0x18003fff pref]          /* size: 0x2000 ! */
[    0.220000] pci 0000:00:02.0: [8086:100e] type 00 class 0x020000
[    0.230000] pci 0000:00:02.0: reg 0x10: [mem 0x18006000-0x18007fff]               /* size: 0x2000 ! */
[    0.230000] pci 0000:00:02.0: reg 0x14: [io  0xc000-0xc03f]

The address 0x18002000 is not legal to store a BAR of size 0x4000 (0x18002000 & (0x4000 - 1) != 0). Likewise address 0x18006000 is not legal to store a BAR of size 0x20000 (0x18006000 & (0x20000 - 1) != 0).

libsel4vm: Fault: support 64 bits fault data mask for aarch64

The function fault_get_data_mask() only produce the mask within 32 bits which meas it can't return a mask like 0xffffffff00000000 with 64 bits seL4_Word.

seL4_projects_libs/libsel4vm/src/arch/arm/fault.c

Line 494 in eb42051

mask <<= (addr & 0x3) * 8;

Thus for some data structures like GICD_IROUTER of gicv3 which is in 64 bits width, the mask and the related fault function fault_emulate() can't handler the access to the upper 32 bits correctly.

delete merged branch xu4_vmm_wip

delete branch xu4_vmm_wip, this has been merged already

libsel4vm: GIC: should the vcpu here be the irq's target vcpu when called from memory fault handler?

When vgic_dist_set_pending_irq() called from a write to pending_bits in emulated GIC distributor, the vcpu here to enqueue the vIRQ is the vcpu that performed the write operation.

seL4_projects_libs/libsel4vm/src/arch/arm/vgic/vdist.h

Lines 222 to 229 in eb42051

	/* Enqueueing an IRQ and dequeueing it right after makes little sense
	* now, but in the future this is needed to support IRQ priorities.
	*/
	int err = vgic_irq_enqueue(vgic, vcpu, virq_data);
	if (err) {
	ZF_LOGF("Failure enqueueing IRQ, increase MAX_IRQ_QUEUE_LEN");
	return -1;
	}

But according to the GIC refenerce, set pending_bits only moves the IRQ to the pending state, and the target vcpu of the IRQ is still specified by it's target_bits, which may not be the vcpu that the vIRQ was inserted into as the above code shows.

That' mean when an IRQ is set to route to the vcpu_0, a write to the pending_bit of the IRQ from vcpu_1 inserts the IRQ into vcpu_1 rather than vcpu_0.

do interrupt maintenance if interrupt is set pending (ie enqueued)

In vgic_dist_set_pending_irq() we enque an interrupt and then dequeue one

seL4_projects_libs/libsel4vm/src/arch/arm/vgic/vgic.c

Lines 581 to 602 in 9de0630

	/* Enqueueing an IRQ and dequeueing it right after makes little sense
	* now, but in the future this is needed to support IRQ priorities.
	*/
	int err = vgic_irq_enqueue(vgic, vcpu, virq_data);
	if (err) {
	ZF_LOGF("Failure enqueueing IRQ, increase MAX_IRQ_QUEUE_LEN");
	return -1;
	}
	int idx = vgic_find_empty_list_reg(vgic, vcpu);
	if (idx < 0) {
	/* There were no empty list registers available, but that's not a big
	* deal -- we have already enqueued this IRQ and eventually the vGIC
	* maintenance code will load it to a list register from the queue.
	*/
	return 0;
	}
	struct virq_handle *virq = vgic_irq_dequeue(vgic, vcpu);
	assert(virq);
	return vgic_vcpu_load_list_reg(vgic, vcpu, idx, virq);

Since there is no guarantee that we dequeue the same interrupt we have enqueued, I wonder if this should dequeue in a loop while there are interrupts in the queue and there are list registers available?

sel4vm: Remove vspace dependency

This is a breaking change but is probably worthwhile to consider:

Removing the vspace_t dependency from libsel4vm and libsel4vmmplatsupport
and interacting with the vspace objects directly mostly resolves a series of issues
and don't really introduce any significant new problems for guests or a client vmm
other than needing to update vmm drivers that expect to use the vspace objects.
It also provides a reasonably small stepping stone for eventually removing more of
sel4_libs as discussed recently (https://sel4.discourse.group/t/sel4-virtualization-support-current-efforts/665/3)

vspace_t is an abstraction that wraps seL4 vspace objects and provides
the following functionality:

1. Mapping intermediate page table objects automatically
2. reserving regions for future mapping
3. Helper functions for creating OS objects like ipc buffers and stacks
4. Tracking reserved regions in the address space like kernel window
   mappings
5. Unmapping vspace entries indexed by virtual address
6. Creating shared mappings from one VSpace into another vspace indexed
   by virtual address
7. Automatic placement of anonymous memory regions (eg mmap)
8. Automatic allocation and mapping of any internal book-keeping data
9. self-hosted or remote management of Vspaces where a vspace can refer
   to the current process address space or a different address space.
10. A way to iteratively and dynamically map frames from another vspace
    into the callers vspace and call a callback function with the mapped
    window as an argument. The mapping is then removed when the callback
    returns.

Unfortunately there are the following issues:

• The book-keeping data allocation can only happen through a vspace_t
  instance. For book-keeping a VM's vspace, the host must then also
  have a vspace_t for managing its own vspace, a host may not want this
  level of dynamism
• The book-keeping data doesn't currently do anything clever for large
  frames and still keeps a unit of data for every 4k range of memory
  used in the vspace. So a 2MiB mapping would have 512 duplicate
  book-keeping entries, and a 1GiB would have 51251216bytes = 4MiB
  overhead.
• Encouraging implementations to use the shared-memory iterator leads to
  very inefficient emulated drivers as mapping and unmapping are usually
  more expensive than short memcpys and dominate the operation time.

The VMM only really needs features 1, 2 and 9, and it already implements
its own version of region reservations (2) separately. There's also some
helper functions in libsel4utils that implement just 1. and depend on a
vka_t interface that the VMM also already has a copy of.

As for 6. the vmm does need a more efficient copyin/copyout mechanism
that would be somewhat system specific and shouldn't create new mappings
on each access.

libsel4arm-vmm: non 32-bit faults handled incorrectly

8-bit and 16-bit read and write faults do not seem to be handled correctly. For example, if a VM performs a 8-bit read and the fault is set to return 0, it will instead return a 32-bit value with garbage in the upper 24-bits and 0x00 in the lower 8-bits.