July 2021 - Devel - lists.sel4.systems

Formally verified AES C code
by Hugo V.C. 20 Jul '21

20 Jul '21

Hi all, I don't want to use SSL/openssl in a project I'm working. Thus, I want to just use my own encryption at the app layer. As performance is not a problem (just very small data packets over a socket) I would like to have the most simple implementation possible of AES, preferably, formally verified. Is anyone aware of any public AES encrytion implementation in C that has been formally or semi-formally verified? Thank you!

5 10

Cannot reserve memory for camkes VM guest
by Alex Ling 17 Jul '21

17 Jul '21

Hi All, I'm trying to bring up camkes VM Linux guest on Firefly RK3399 board which is with a GICv3 ARMv8. I'm using the "rockpro64" target and my work is based on [1] and [2]. When I run the "capdl-loader-image-arm-rockpro64", there's error "Range not available at 0xfef10000, size 0x10000". Bootstrapping kernel Booting all finished, dropped to user space Undelivered IRQ: 132 Install gic v3 sel4utils_reserve_range_at_no_alloc@vspace.c:595 Range not available at 0xfef10000, size 0x10000 vm_reserve_memory_at@guest_memory.c:328 Failed to allocate vm reservation: Unable to create vspace reservation at address 0xfef10000 of size 65536 vm_install_vgic_v3@vgic_v3.c:87 Error installing vgic Assertion failed: !err (/mnt/data3/projects/rk3399/build/seL4/camkes-vm-app/projects/vm/components/VM_Arm/src/main.c: main_continued: 1098) Here's my projects/seL4_projects_libs/libsel4vmmplatsupport/plat_include/rockpro64/sel4vmmplatsupport/plat/devices.h content: #define GIC_VERSION_3 #define GIC_PADDR 0xfee00000 #define GIC_DIST_PADDR (GIC_PADDR + 0x00000000) #define GIC_DIST_SIZE 0x10000 #define GIC_REDIST_PADDR 0xfef00000 #define GIC_REDIST_SIZE 0xC0000 #define GIC_REDIST_SGI_PADDR (GIC_REDIST_PADDR + 0x00010000) #define GIC_REDIST_SGI_SIZE 0x10000 I think the problem is related to GIC_REDIST_SIZE. I set it to 0xC0000 according to the rockpro64 device tree file in kernel/tools/dts/rockpro64.dts interrupt-controller@fee00000 { compatible = "arm,gic-v3"; #interrupt-cells = < 0x04 >; #address-cells = < 0x02 >; #size-cells = < 0x02 >; ranges; interrupt-controller; reg = < 0x00 0xfee00000 0x00 0x10000 0x00 0xfef00000 0x00 0xc0000 0x00 0xfff00000 0x00 0x10000 0x00 0xfff10000 0x00 0x10000 0x00 0xfff20000 0x00 0x10000 >; interrupts = < 0x01 0x09 0x04 0x00 >; phandle = < 0x01 >; I tried to reduce it to 0x10000 and it can boot to VM guest but the guest Linux will fail in gic_iterate_rdists() because it cannot read from GIC's GICR_TYPER register correctly. Did I miss anything? Any suggestion is highly appreciated. Thank you very much! [1] https://github.com/seL4/seL4/pull/378 [2] https://github.com/seL4/seL4_projects_libs/tree/sylvain/gicv3 Regards, Alex

2 2

Passing caps through CAmkES procedures?
by Austin Appleby 14 Jul '21

14 Jul '21

Hi, I've got what seems like a simple task that I can't quite figure out how to implement - I am sketching out a key-value-store component where the "values" can be quite large (tens or hundreds of K). I would like clients of the component to pass caps to their own buffers in and out of this component's API to minimize copying and temporary buffer allocation and ensure that multiple clients can't see each other's data. In plain seL4 this would be done via the client passing a cap in its seL4_Call(), but I don't see an equivalent for this in CAmkES. Is there a way of declaring this in the .camkes syntax? If not, is there a way to build this component outside of CAmkES and still allow it to interact with existing CAmkES components? -Austin Appleby @ Google

1 0

CI infrastructure outage
by Peter Chubb 09 Jul '21

09 Jul '21

Hi Folks, Our continuous integration testing infrastructure is being relocated from CSIRO to UNSW premises this weekend. Because Sydney is in COVID lockdown, and because we're reworking the system not to rely on commercial software we no longer have a licence for (Atlassian Bamboo), we will probably not have everything working again for two or three weeks. The upshot for you is that any pull request that needs extensive testing will not be merged for at least two weeks, possibly longer. Peter C -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW

1 0

gic v2 vs gic v3
by Chris Koziarz 09 Jul '21

09 Jul '21

Hi all, I'm trying to port camkes-arm-vm to a different platform, that supports gic-v3 In the process, I hit a compilation error: Building C object kernel/CMakeFiles/kernel_all_pp_...rapper_temp_lib.dir/ kernel_all_pp_prune_wrapper_temp.c.obj FAILED: kernel/kernel_all_pp_prune_wrapper_temp.c In file included from /home/chris/camkes-tqma8xqp- vm/kernel/src/arch/arm/object/vcpu.c:15: /home/chris/camkes-tqma8xqp-vm/kernel/include/arch/arm/arch/machine/gic_v2.h:23: error: "IRQ_MASK" redefined [-Werror] 23 #define IRQ_MASK MASK(10u) In file included from kernel/gen_headers/plat/platform_gen.h:23, from /home/chris/camkes-tqma8xqp-vm/kernel/include/plat/ default/plat/machine.h:8, from /home/chris/camkes-tqma8xqp- vm/kernel/include/machine.h:9, from /home/chris/camkes-tqma8xqp- vm/kernel/include/api/syscall.h:10, from /home/chris/camkes-tqma8xqp- vm/kernel/src/api/faults.c:10: /home/chris/camkes-tqma8xqp-vm/kernel/include/arch/arm/arch/machine/gic_v3.h:30: note: this is the location of the previous definition 30 #define IRQ_MASK MASK(16u) which is an indicative that both gic_v3.h & gic_v2.h headers have been included, which is an error because said headers are not compatible: kernel/include/arch/arm/arch/machine/gic_v3.h:#define IRQ_MASK MASK(16u) kernel/include/arch/arm/arch/machine/gic_v2.h:#define IRQ_MASK MASK(10u) So my question is: how can I configure the build to avoid such a conflict? I can grepp the relevant configuration option in CMakeCache.txt: build_tqma8/CMakeCache.txt:CONFIGURE_INTERRUPT_CONTROLLER:INTERNAL=arch/machine/gic_v3.h but cannot see it in ccmake gui because it's "INTERNAL" What is the solution? - replace this option somehow to use gic_v2 and have my HW use gic v.2, or - change compilation options to use gic_v3 everywhere Thanks for any help, Chris.

4 5

Re: gic v2 vs gic v3
by Alex Ling 凌云 08 Jul '21

08 Jul '21

Hi All, What is the status of virtualization support on ARM SOCs with GICv3? According to section “FAQ and Implementation Notes” of [1], seems it is still under development. Any plan or progress on this? Thank you very much. [1] https://docs.sel4.systems/projects/camkes-arm-vm/ Regards, Alex

1 0

Re: Tutorial Problem
by Kent Mcleod 08 Jul '21

08 Jul '21

On Wed, Jun 30, 2021 at 11:53 AM Michael Neises <neisesmichael(a)gmail.com> wrote: > > Kent, > > > > I tried using those extra arguments and got the same error regarding kvm I reported a few minutes ago: > > > > ./simulate: qemu-system-x86_64 -machine q35,accel=kvm,kernel-irqchip=split -cpu Nehalem,+vme,+pdpe1gb,-xsave,-xsaveopt,-xsavec,-fsgsbase,-invpcid,+syscall,+lm,enforce,+vmx -nographic -serial mon:stdio -m size=2G -enable-kvm -device intel-iommu,intremap=off -net nic,model=e1000 -net tap,script=no,ifname=tap0 -kernel images/kernel-x86_64-pc99 -initrd images/capdl-loader-image-x86_64-pc99 Could not access KVM kernel module: No such file or directory > > qemu-system-x86_64: failed to initialize KVM: No such file or directory > There are instructions on how to setup KVM and nested virtualization on the tutorial that I've pasted here: "Note if you are using QEMU it is important to ensure that your host machine has VT-x support and KVM (https://www.linux-kvm.org/page/Main_Page) installed. You also need to ensure you have enabled nested virtulisation with KVM guests as described here (https://www.linux-kvm.org/page/Nested_Guests)" A quick way to check if nested virtualization is enabled (and therefore supported) on your host is to run `cat /sys/module/kvm_intel/parameters/nested`. `Y` should be returned if it's enabled. It may be easier to run the image on an actual machine instead of in qemu. The images produced can be loaded by a multiboot loader such as grub or pxelinux. (https://docs.sel4.systems/Hardware/VMware/#add-grub2-option-to-run-sel4) has an example grub config.

4 7

seL4 Linux guest mmap() crashes the VM
by Hugo V.C. 02 Jul '21

02 Jul '21

Hi, my seL4 Linux VM box just crashed when trying to access a memory address. Basically I simply wanted to use "devmem" tool to just print the content of a specific address in memory and looked like seL4 was unable to handle the guest OS mmap() correctly. Below the console log: # ls /proc/283/maps /proc/283/maps # cat /proc/283/maps 00400000-00532000 r-xp 00000000 00:02 6023 /bin/lighttpd 00541000-00543000 r--p 00131000 00:02 6023 /bin/lighttpd 00543000-00546000 rw-p 00133000 00:02 6023 /bin/lighttpd 00546000-0054d000 rw-p 00000000 00:00 0 0bd0b000-0bd2d000 rw-p 00000000 00:00 0 [heap] 0bd2d000-0bd91000 rw-p 00000000 00:00 0 [heap] ffff82084000-ffff82085000 r--p 00000000 00:00 0 [vvar] ffff82085000-ffff82086000 r-xp 00000000 00:00 0 [vdso] ffffe6c58000-ffffe6c79000 rw-p 00000000 00:00 0 [stack] # devmem 0xffffe6c58000 8 _utspace_split_alloc@split.c:266 Failed to find any untyped capable of creating an object at address 0xffffe6c58000 map_page@mapping.c:68 Failed to map page at address 0xffffe6c58000 with cap 396187, error: 1 sel4utils_map_page_pd@vspace.c:153 Error mapping pages, bailing: 1 map_vm_memory_reservation@guest_memory.c:477 Failed to map address 0xe6c58000 into guest vm vspace vm_map_reservation@guest_memory.c:510 Failed to map vm reservation: Error when mapping into VM's vspace -------- Pagefault from [Linux]: read fault @ PC: 0x414c38 IPA: 0xffffe6c58000, FSR: 0x93020004 Context: x0: 0xffff9cfe6000 x1: 0x0 x2: 0x0 x3: 0x1 x4: 0x3 x5: 0xffffe6c58000 x6: 0x5 x7: 0x20 x8: 0xde x9: 0xffffe539cf54 x10: 0xffff9cfe8050 x11: 0x1 x12: 0x436 pc: 0x414c38 x14: 0xffffffff sp: 0xffffe539bb70 spsr: 0x60000000 x13: 0x1 x15: 0x3 x16: 0xffff9cf486c8 x17: 0x4c3870 x18: 0x0 x19: 0x8 x20: 0x0 x21: 0x4c3000 x22: 0xffffe539bd98 x23: 0xffffe6c58000 x24: 0x0 x25: 0x0 x26: 0x0 x27: 0x0 x28: 0x0 x29: 0xffffe539bc60 x30: 0x414bac m-------- main_continued@main.c:1134 Failed to run VM Halting... My three concerns here are: 1) Why this guest mmap() is crashing the VM? Memory address is valid (just guest user space process stack). 2) Is it possible to have some kind of "dump and reboot VM" when a VM and/or guest OS crashes? 3) Are there any plans to formally verify the seL4's VM camkes code? Thank you!

2 6

Camkes SerialServer and util_libs/libplatsupport with ODROID-C4
by Robert Reid 01 Jul '21

01 Jul '21

Hi everyone Summary - trying to get util_libs/libplatsupport going for a HardKernel ODROID-C4, using the camkes serialserver_polling app - but not having any luck with mapping the UART. I'd welcome any explanations of what you think is happening here. The background and my progress follows. I thought I'd dive into the seL4 world and do some experimenting. I thought a good place to start would be the UNSW AOS project (17 years after I first did it) - but with no more ODROID-C2, got a hold of an ODROID-C4 and figured that would be a good project in itself (and well timed with a Sydney lockdown). So - good news: The peripheral devices we need are all very similar to a C2, so by getting a new DTS file and updating a few addresses it starts off fairly happily. sel4-test builds and runs (All is well...); so does the camkes adder app; and with some mods to provide enough slots (maybe because it has 4GB rather than 2GB) I have got the AOS milestone 0 stub to run (including the uart initialisation). (More work to actually finish m0 and keep going, but a job for later) But then: I moved onto the util_libs / libplatsupport project to try and port over as much of the device settings as possible; and using the camkes app serialserver_polling, under the hood using SerialServer, I can't get the uart to initialiise (or more strictly can't get the uart address to map). chardev_map / ps_io_map fails, returning a vaddr of 0. I've added a bunch of debug prints to the process; and for comparison also run it on QEMU emulating a Sabre board. On odroidc4 hardware: ## Starting application at 0x01080000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A55 r1p0 paddr=[95e000..d5710f] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at a86de8. Loaded DTB from a86de8. paddr=[23f000..24afff] ELF-loading image 'kernel' to 0 paddr=[0..23efff] vaddr=[ffffff8000000000..ffffff800023efff] virt_entry=ffffff8000000000 ELF-loading image 'capdl-loader' to 24b000 paddr=[24b000..563fff] vaddr=[400000..718fff] virt_entry=408e48 Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Booting all finished, dropped to user space pre_init@serial.c:501 About to init port, io_ops=0x487cf0 ps_cdev_init@chardev.c:46 About to init_fn 3 ps_cdev_init@chardev.c:47 dev_defn[3].paddr: 0xff803000, size 1000 uart_init@serial.c:51 about to chardev_map: dev=0x473948, defn->id=3, defn->padd r=0xff803000 chardev_map@chardev.h:26 ops->io_mapper=0x487be0 &(ops->io_mapper)=0x442728 dev- >paddr=0xff803000 dev->size=0x1000 uart_init@serial.c:56 chardev_map mapped page_vaddr 0 plat_pre_init@plat.c:64 Failed to initialise character device plat_pre_init@plat.c:65 PS_SERIAL_DEFAULT: 3 On Sabre QEMU: ./simulate: qemu-system-arm -machine sabrelite -nographic -serial null -serial mon:stdio -m size=1024M -kernel images/capdl-loader-image- arm-imx6 ELF-loader started on CPU: ARM Ltd. Cortex-A9 r0p0 paddr=[106fc000..10aa98e3] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 107fe33c. Loaded DTB from 107fe33c. paddr=[1003d000..10047fff] ELF-loading image 'kernel' to 10000000 paddr=[10000000..1003cfff] vaddr=[e0000000..e003cfff] virt_entry=e0000000 ELF-loading image 'capdl-loader' to 10048000 paddr=[10048000..10300fff] vaddr=[10000..2c8fff] virt_entry=187f8 Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Warning: Could not infer GIC interrupt target ID, assuming 0. Booting all finished, dropped to user space pre_init@serial.c:501 About to init port, io_ops=0x69cf0 ps_cdev_init@chardev.c:45 About to init_fn 1 ps_cdev_init@chardev.c:46 dev_defn[1].paddr: 0x21e8000, size 1000 uart_init@serial.c:224 about to chardev_map: dev=0x7f8c8, defn->id=1, defn->paddr=0x21e8000 chardev_map@chardev.h:26 ops->io_mapper=0x69cf0 &(ops->io_mapper)=0x1f328 dev->paddr=0x1f654 dev->size=0x4ebc4 uart_init@serial.c:226 chardev_map mapped vaddr 0xbb000 pollcli: Hello Serial Server! pollcli: abc This has me confused - it's good it works, but I can't follow in the flow how the paddr gets changed from the value supplied to chardev_map (ie 0x21e80000 becomes 0x1f654), yet in that case it works. Or is it a complication of using QEMU? A similar kind of test with AOS on odroidc4 - particularly the success of "*uart_init@uart.c:35 Mapped uart paddr:ff803000 size:1000 vaddr:b0000000*" ## Starting application at 0x01080000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A55 r1p0 paddr=[88a000..c2b10f] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 9f3068. Loaded DTB from 9f3068. paddr=[247000..252fff] ELF-loading image 'kernel' to 0 paddr=[0..246fff] vaddr=[ffffff8000000000..ffffff8000246fff] virt_entry=ffffff8000000000 ELF-loading image 'sos' to 253000 paddr=[253000..48cfff] vaddr=[400000..639fff] virt_entry=4172e0 Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Booting all finished, dropped to user space SOS Starting... <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> uart_init@uart.c:35 Mapped uart paddr:ff803000 size:1000 vaddr:b0000000 SOS Started! test_cspace@tests.c:59 Test cspace run_tests@tests.c:174 Root CSpace test passed! test_cspace@tests.c:59 Test cspace run_tests@tests.c:182 Single level cspace test passed! test_cspace@tests.c:59 Test cspace cspace_alloc_slot@cspace.c:335 Cspace is full! run_tests@tests.c:195 Double level cspace test passed! run_tests@tests.c:199 DMA test passed! run_tests@tests.c:203 Frame table test passed! Network init dwmac.b0002000 Waiting for PHY auto negotiation to complete........ done Speed: 1000, full duplex Protocol ethernet registered (layer: 2). Protocol ipv4 registered (layer: 3). Protocol ipv6 registered (layer: 3). Protocol icmp4 registered (layer: 4). Protocol icmp6 registered (layer: 4). Protocol igmp registered (layer: 4). Protocol udp registered (layer: 4). Protocol tcp registered (layer: 4). Assigned ipv4 0.0.0.0 to device sos picotcp DHCP client: update link Assigned ipv4 192.168.200.125 to device sos picotcp DHCP client: renewal time (T1) 43200 DHCP client: rebinding time (T2) 75600 DHCP client: lease time 86400 DHCP client: netmask 255.255.255.0 DHCP client: gateway 192.168.200.4 Timer init Start first process Starting ttytest at 0x4001c8 SOS entering syscall loop aos: Error attempting syscall 29 task: Hello world, I'm tty_test! handle_syscall@main.c:128 Unknown syscall 1 <<seL4(CPU 0) [receiveIPC/148 T0xffffff803fff8400 "SOS:root" @407a48]: Reply obj ect already has unexecuted reply!>> In this case it has worked, sos_map_device works as expected (although the spurious interrupts are another task to figure out). But trying to understand what's really going on underneath ps_io_map and ultimately why libplatsupport won't work for me has got me confused. Any ideas would be appreciated. Regards Rob

2 4

camkes-vm-linux kernel example
by Hugo V.C. 01 Jul '21

01 Jul '21

Hi, just a simple question: why this tutorial: https://docs.sel4.systems/Tutorials/camkes-vm-linux.html shows this output: Welcome to Buildroot buildroot login: root Password: # grep poke /proc/devices # figure out the major number of our driver 244 poke # mknod /dev/poke c 244 0 # create the special file # echo > /dev/poke # write to the file [ 57.389643] hi -sh: write error: Bad address # the shell complains, but our module is being invoked! I'm not getting the shell complain error, just this: # grep poke /proc/devices 247 poke # mknod /dev/poke c 247 0 # echo > /dev/poke [ 138.946905] TOC TOC NEO... # FYI: my kernel is a custom compiled one but same version as the pre-compiled you provide: # uname -a Linux buildroot 4.9.189 #4 SMP Thu Jun 24 00:16:49 CEST 2021 aarch64 GNU/Linux Any hint? Cheers,

2 2