June 2024 - Devel - lists.sel4.systems

seL4 test on x86
by Yevgeny Lavrov 29 Jan '25

29 Jan '25

Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm trying to run seL4 test suite or simple hello world task from seL4 tutorials on the real hardware. So far I had no problems compiling seL4 test suite and running via QEMU for both x32 and x64 platforms. However, when I try to run it on the actual hardware following Running on real hardware tutorial for x86 I end up with no output at all and no error msgs that can give me a clue on where something went wrong. After compiling seL4test for x86, I ended up with two images in sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created a new GRUB2 entry that looks like this menuentry “seL4 test suite” --class os { load video insmod gzio insmod part_msdos insmod ext2 set root=’(hd0,msdos5)’ multiboot /boot/sel4/kernel-ia32-pc99 module /boot/sel4/sel4test-driver-image-ia32-pc99 } update grub, restart and select the new entry from GRUB menu. I end up with blinking cursor on the top-left side of the screen. Please advise.

4 3

Stuck during invalidate local TLB in Tx2
by Muneeswaran Rajendran 15 Oct '24

15 Oct '24

Hi seL4 Dev team, Can someone explain the reason (share the reference) to invalidate the local TLB during kernel vspace activation as part CPU initialisation. The Tx2 board stuck while performing this operation. As per my understanding both Tx1 and Tx2 are using same A57 core. so the TLB initialisation and invalidation remain same for Tx2 and should not stuck during invalidation.Please correct me if anything wrong here. I understand from that instruction (tlbi vmalle1) which is invalidating stage 1 entries associated to the current VMID. Also from arm mmu code the seL4 setting up (TCR_EL1) TCR register addressing space as 48bit, ASID as 16bit and page table setup 4k granular size. I am using MRS macro to dump the spsr_el1 and dspsr_el0 register to see the state of processor but its throwing synchronous exception. Do we have any other option to dump all the register content to see the state of processor like we have one in 'sel4debug_dump_registers' which is used in sel4test code. Regards, Muneeswaran R

3 4

Gpu passthrough
by Hugo V.C. 15 Aug '24

15 Aug '24

Hi all, here a simple question: is there any example/tutorial off gpu passthrough to a Linux guest? Best,

4 6

Build failure for sel4 on raspberry pi 5
by l4＠photiczone.com 14 Aug '24

14 Aug '24

Hi everyone, I am getting a link failure during the build of sel4test-tests: /usr/bin/ld: apps/sel4test-driver/musllibc/build-temp/stage/lib/libc.a(__stdio_exit.o): copy relocation against non-copyable protected symbol `__stdin_used' collect2: error: ld returned 1 exit status Searching t'interwebs seems to imply this is a gnarly problem caused by the nuances of various build tools - but one that should not apply to Arm. You can summarise everything I did before the build like this: sudo apt install ninja-build libxml2-utils repo pip3 install pyyaml typing hardware pyfdt jinja2 jsonschema six future ply python3-protobuf grpcio-tools cd && mkdir xxx && cd xxx Then to follow your build repo init -u https://github.com/seL4/sel4test-manifest.git repo sync mkdir build && cd build ../init-build.sh -DPLATFORM=bcm2711 ninja And yes I know it is not supported and the BCM2711 is for the Pi 4. I am evaluating ;) Any help greatly appreciated. Thanks, Smiley

3 4

I am interested in porting LionOS to X64 architecture
by Peter Relich 14 Aug '24

14 Aug '24

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-700… 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?) Thanks so much for your time. Respectfully, Peter Relich Research Scientist Intellisense Systems, Inc. ________________________________ The information contained in this e-mail and any attachments from Intellisense Systems may contain confidential and/or proprietary information, and is intended only for the named recipient to whom it was originally addressed. If you are not the intended recipient, any disclosure, distribution, or copying of this e-mail or its attachments is strictly prohibited. If you have received this e-mail in error, please notify the sender immediately by return e-mail and permanently delete the e-mail and any attachments.

5 5

CPU/ISA tuned specifically for seL4?
by Isaac Beckett 25 Jun '24

25 Jun '24

Hello! I recall reading about old CPUs/ISAs made for Lisp machines, with features and optimized for specifically running Lisp. And I’ve heard people discuss how current CPUs are optimized for C code and similar programming paradigms, and vice versa: C and others are optimized for those CPUs. This got me wondering, what might a CPU or instruction set designed more specifically to run seL4 look like? I’m guessing it might involve capability hardware like CHERI to accelerate seL4’s software implementation of capabilities, but what else might be relevant? Thanks, Isaac Beckett

3 2

seL4 developer hangout reminder
by Gerwin Klein 23 Jun '24

23 Jun '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 26 Jun, 08:00 UTC. For your local date and time please see https://sel4.systems/contact/. Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Gerwin

1 0

Success and Effort in seL4 x86_64 Virtualbox
by thomas.j.hampton＠gmail.com 21 Jun '24

21 Jun '24

Hey; configuration is a pretty big space and I didn't see anything specific, and may have bumped into a bug along the way. Here's some details about getting seL4test working, and using the EGA driver on this platform. Here's the commits I'm on: - sel4test 95522e9 - seL4 ddeb18a01 I managed to get seL4test running in VirtualBox on a Tiger Lake chip some weeks ago, not terribly impressive, things worked pretty well, generally. - I discovered that on the platform I needed to manually set all the '*HAVE_TIMER*' flags in the code to 0 - to get the tests to succeed on VirtualBox; CMake doesn't appear to support this transformation. - a major stumbling block was that these changes were being reverted each time I re-ran CMake, under my feet. So that's pretty cool... Some further exploration I discovered that there's the pc99/ega (ega.c) driver, since I'm curious about the requirements for starting to build a custom OS on top of seL4 for this platform, and seeing it run on the hardware in front of me (again, a Tiger Lake laptop). I spent many weeks trying to massage things into place. Reading and learning along side the bootstrap pathway; multiboot.S -> head.S -> boot_sys -> common -> char_dev ... to no avail. However I came into some time and decided to revisit the problem. - #define MULTIBOOT_GRAPHICS_TEXT 2 is an error; Multiboot1 spec has that this should be 1, instead - When I was trying to boot UEFI, this would manifest as a Protection Fault - Fixing this left the system booting, utilizing high amount of CPU, and then going quiet. - UEFI on this platform has unclear / additional requirements / doesn't actually support EGA/VGA text mode - https://www.reddit.com/r/osdev/comments/st0psl/framebuffer_output_for_multi…

2 1

Assertion failure when booting seL4 image on x86 UEFI via Grub
by fennelfoxxo＠gmail.com 15 Jun '24

15 Jun '24

Hello all! This is my first time posting here, but I'll try to provide all the detail I can, and I'm grateful for any advice others have to fix this issue. I've been trying to boot the seL4 Hello World tutorial in QEMU with UEFI support on the x86 platform, with the help of the Grub bootloader. It seems I can load the kernel okay, but an error occurs when the kernel tries to load the rootserver: > seL4 failed assertion 'mods_end_paddr > boot_state.ki_p_reg.end' at /home/fennel/grubbuild/stacktest/sel4-tutorials/kernel/src/arch/x86/kernel/boot_sys.c:452 in function try_boot_sys From my research, it seems to be happening because grub is loading the rootserver module at a lower address than expected. These two lines from serial output during boot indeed show that the module end address is lower than the kernel end address: > module #0: start=0x751000 end=0x7954c8 size=0x444c8 name='' > Kernel loaded to: start=0x100000 end=0xc12000 size=0xb12000 entry=0x100298 When running the same hello world project using ./simulate in the build directory, the rootserver module is placed at a higher address and boots ok: > module #0: start=0xc13000 end=0xc574c8 size=0x444c8 name='images/hello-world-image-x86_64-pc99' > Kernel loaded to: start=0x100000 end=0xc12000 size=0xb12000 entry=0x100298 Does anyone know if this is a mistake in how I am compiling and building the project, my QEMU settings, or perhaps an issue with how Grub is handling loading the module? Booting from Grub should be possible in theory (https://docs.sel4.systems/Hardware/IA32.html) so any guidance is appreciated. Thank you! - Fennel STEPS TO REPRODUCE: # Contents of grub.cfg - place in current directory menuentry "Load seL4" --class os { insmod efi_gop insmod efi_uga insmod all_video set root='(hd0,gpt1)' multiboot2 /EFI/BOOT/sel4kernel module2 /EFI/BOOT/sel4rootserver } # End of grub.cfg # Compile Grub 2.06 from source to ./grub-2.06 wget https://ftp.gnu.org/gnu/grub/grub-2.06.tar.gz -O grub.tar.gz # Download grub source tar -xvzf grub.tar.gz -C ./ && rm grub.tar.gz # Unzip and remove original file cd grub-2.06 && ./autogen.sh && ./configure --target=x86_64 --with-platform=efi && make # Configure & compile # Install, configure, and compile hello-world seL4 project to ./sel4-tutorials mkdir sel4-tutorials cd sel4-tutorials repo init -u https://github.com/seL4/sel4-tutorials-manifest # Install tutorials repo sync ./init --plat pc99 --tut hello-world cd hello-world_build cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -DKernelHugePage=OFF -G Ninja . # Disable huge page requirement ninja # Create final image as disk.img mkdir EFI EFI/BOOT grub-2.06/grub-mkimage -d grub-2.06/grub-core -o EFI/BOOT/BOOTX64.EFI -O x86_64-efi -p "" configfile fat part_gpt gzio multiboot video efi_gop efi_uga normal chain boot multiboot2 all_video cp sel4-tutorials/hello-world_build/images/kernel-x86_64-pc99 EFI/BOOT/sel4kernel cp sel4-tutorials/hello-world_build/images/hello-world-image-x86_64-pc99 EFI/BOOT/sel4rootserver cp grub.cfg EFI/BOOT/grub.cfg dd if=/dev/zero of=disk.img bs=1M count=35 # 35MB is just about the smallest FAT32 partition possible mformat -i disk.img@@2048s -v "EFI SYSTEM" -F # Create fat32 partition 2048 sectors in mcopy -i disk.img@@2048s -s EFI :: parted -s disk.img mklabel gpt mkpart '"EFI SYSTEM"' fat32 2048s 100% set 1 esp on # Create partition entry for ESP # Run in QEMU (most of these arguments are copied from the seL4 ./simulate script - replace OVMF path with your path to OVMF_CODE.fd for UEFI boot) qemu-system-x86_64 -cpu Nehalem,-vme,+pdpe1gb,-xsave,-xsaveopt,-xsavec,-fsgsbase,-invpcid,+syscall,+lm,enforce -serial mon:stdio -m size=512M -drive if=pflash,format=raw,readonly=on,file=PATH_TO_OVMF_CODE.fd -drive file=disk.img

1 0

Unblocking the caller of seL4_Call when the receiver is killed
by Arya Stevinson 12 Jun '24

12 Jun '24

Hello, I'll give a brief introduction since this is my first message here. I'm an undergraduate research assistant at the University of British Columbia, and I'm working with Margo Seltzer (https://www.seltzer.com/margo/) in the Systopia Lab. I'm helping with development of Sid Agrawal's (https://sid-agrawal.ca/) project built on seL4. I'm trying to determine what is the correct way to handle this situation: 1. Process 1 makes an seL4_Call to an endpoint that Process 2 is listening on. 2. Process 2 receives the message, and since we are running in non-MCS kernel, it will get a reply capability in its TCB. 3. Process 2 dies, for whatever reason, before it can reply to Process 1. If we wanted to unblock Process 1, what would be the correct approach? - I can use seL4_CNode_SaveCaller in Process 2 as soon as it receives a message, and store the slot number in some shared memory with the root task. Then when Process 2 dies, the root task is able to move the reply capability into its own cspace and send a reply indicating an error. This is not ideal for our purpose, because we do not want Process 2 to be able to perform any operations on its own cspace, but it needs its own root cnode capability in order to perform seL4_CNode_SaveCaller. - Is seL4_Call the wrong function for this purpose? We also considered using NBRecv and considering the call a failure after some timeout period. This is also not ideal since we would lose the convenience of the Call's reply cap, etc. - Is there some other solution that we are missing? As an aside: I notice that for the MCS kernel, if the reply cap is deleted, Process 1's thread state would be moved from ThreadState_BlockedOnReceive to ThreadState_Inactive. In non-MCS kernel, it seems that the state would remain ThreadState_BlockedOnReceive? Is there a reason for this? Best, Arya

2 2