February 2022 - Devel - lists.sel4.systems

hello_rumprun app not worked
by MOHAMAD REZA SHAFIEI 19 Apr '25

19 Apr '25

hi. i'm recently worked on sel4 with camkes framework. when i compile rumprun_hello on x86_64 platform its compiled and build correctly but when run with qemu by ./simulate script, program crashed with this errors: simple_get_extended_bootinfo_length@simple.h:600 simple_get_extended_bootinfo_length not implemented FAULT HANDLER: data fault from hello.hello_0_control (ID 0x1) on address 0x8, pc = 0x402b7f, fsr = 0x6 FAULT HANDLER: Register dump: FAULT HANDLER: rip :0x402b7f , . . so i found that this method not implemented yet so i return 0 in this method and resolved. for second problem that cause failure if trace program and i found that in "init rumprun" process the program failed in the /projects/sel4runtime/include/sel4_arch/x86_64/sel4runtime/thread_arch.h file and sel4runtime_set_tls_base method. so i read git log and in recently commit your team use sel4runtime for thread TLS, so when we run rumprun_hello, the program failed in sel4runtime_set_tls_base method. can you help me fix this bug? thanks for your attention. -- This email was Anti Virus checked by Security Gateway.

5 5

seL4 test on x86
by Yevgeny Lavrov 30 Jan '25

30 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 16 Oct '24

16 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

Questions about Memory Management in seL4
by Daniel Wang 19 May '23

19 May '23

Hi all, Sorry to bother, I have some basic questions about seL4 memory management. Can someone help me? 1. where is the kernel’s address space? I know there are basically three methods: a) separate virtual address space, e.g. through changing page tables on entry into privileged mode to access b) physical space, e.g. through disable automatic hardware translation of virtual addresses on entry into privilege mode c) privilege region in each process’s virtual address space, e.g. through page table to map kernel address into use-mode process. My question is which of this is being used by seL4 microkernel? 2. Objects like CSpace, VSpace, CNode, TCB, Endpoint, etc. are called kernel objects, but it seems all dynamically allocated in thread running/creating time. Are those objects (e.g. Figure 3.3 in seL4 manual) in kernel space or in user space? 3. I read that after the kernel boot up, it passes all resources, untyped memory to the first thread. Are those untyped memory physical memory or virtual memory in a single page? The reason I ask is I’m learning the code of the UNSW AOS project (two of the assignment projects are implementing frame and papers). I’m confused that before the implementation of frames and pages what kind of memory is passed to the the first thread? I saw int AOS project, it uses ut_table_init(), ut_steal_mem(), I wonder what kind of memory it operates on? Thanks -Dan

5 4

libsel4muslcsys: Error attempting syscall 215
by skydivebcn＠gmail.com 05 Mar '22

05 Mar '22

Hi guys, I was trying to boot a custom Linux 4.9.302 Kernel and fot this horrible message: "libsel4muslcsys: Error attempting syscall 215" hugo@dev:~/seL4/sel4webserver_hugusmaximus_fork/build$ sudo ./simulate --extra-qemu-args="-netdev tap,id=mynet0,ifname=tap0,script=no,downscript=no -device virtio-net,netdev=mynet0,mac=52:55:00:d1:55:01,disable-modern=on,disable-legacy=off" [sudo] contraseña para hugo: ./simulate: qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -nographic -m size=2048 -netdev tap,id=mynet0,ifname=tap0,script=no,downscript=no -device virtio-net,netdev=mynet0,mac=52:55:00:d1:55:01,disable-modern=on,disable-legacy=off -kernel images/capdl-loader-image-arm-qemu-arm-virt ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[61bf9000..631120af] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 61d3a2b8. Loaded DTB from 61d3a2b8. paddr=[60243000..60244fff] ELF-loading image 'kernel' to 60000000 paddr=[60000000..60242fff] vaddr=[ff8060000000..ff8060242fff] virt_entry=ff8060000000 ELF-loading image 'capdl-loader' to 60245000 paddr=[60245000..617fdfff] vaddr=[400000..19b8fff] virt_entry=408f38 Enabling hypervisor 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 <<seL4(CPU 0) [decodeUntypedInvocation/205 T0xff80bf815400 "rootserver" @4006f8]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>> Loading Linux: 'linux' dtb: 'linux-dtb' install_linux_devices@main.c:655 module name: map_frame_hack install_linux_devices@main.c:655 module name: init_ram install_linux_devices@main.c:655 module name: cross_vm_connections libsel4muslcsys: Error attempting syscall 215 libsel4muslcsys: Error attempting syscall 215 _utspace_split_alloc@split.c:266 Failed to find any untyped capable of creating an object at address 0x8020000 as this is purely an seL4 error message (musl libc seL4 code?) then I would appreciate any hint about what can be going on. P.S.: I have run my seL4 qemu aarch64 with several Linux kernel versions and never had this problem until now.

2 1

Call for support contract to the seL4 Foundation
by Birgit Brecknell 25 Feb '22

25 Feb '22

A friendly reminder that bids are due before March 4th, 2022 AOE: The seL4 foundation is seeking to contract support for the following duties: - address open github issues in the seL4 organisation repositories, with prioritisation directed by the TSC delegates; this includes: - documentation, tutorials - bugs - tests - docsite and possibly website in coordination with Foundation people - help keeping an eye on making sure questions on mailing lists, discourse and github issues are answered (by someone) Requirement for the person working on these tasks are: - multiple years of experience with seL4, both at kernel level and user-level code - good familiarity with the seL4 organisation repositories - active contributor to one or more seL4 repositories - fluent in written and spoken English The seL4 foundation would contract a service company, initially for 6 months. The service company should identify the person that will be performing the work, ideally on a full-time basis. To bid for the contract, send email to foundation(a)sel4.systems before March 4th, 2022 AOE, with the resume of the person that will be performing the work and a cover letter addressing the requirements. --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au seL4 Foundation, birgit(a)sel4.systems 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Re: Announcing Neptune OS release v0.1.1: A Windows NT personality for seL4
by Chang Liu 24 Feb '22

24 Feb '22

Thank you both for the discussion on licensing. Seems that GPLv3 is a good choice for now. Wikipedia seems to claim that ReactOS is licensed under "GPLv2 or any later version" but I didn't find this on the reactos source code itself. If the ReactOS foundation has an objection later I can always change it to v2. Best, Chang On Wed, Feb 23, 2022 at 12:09 AM G. Branden Robinson < g.branden.robinson(a)gmail.com> wrote: > Hi Chamg, > > At 2022-02-22T23:29:21-0500, Chang Liu wrote: > > I just added a LICENSE file which is GPLv3. > > Good choice! > > > I'm honestly not sure what the difference between GPLv2 and GPLv3 > > There are modest differences, but the general thrust of both versions of > the license is the same: guaranteed access to source code under a "share > and share alike" principle. > > > is so I went with the latest version (I assume they are compatible?) > > Technically, no. But most GPLv2 software is licensed under terms that > allow promotion of the license to "any later version". One famous > example of an exception that is GPLv2-only is the Linux kernel. > So is seL4 itself[1]. Consider whether you expect to need to share code > with a GPLv2-only project. (Even if you do, I would only revisit your > decision once concrete code-sharing is imminent.) > > You're not stuck with a choice of a single license forever. The GPLv3 > is a good selection to start with (in my opinion) because most > organizations that would like to exploit a work for proprietary > advantage are allergic to that license. > > You can always relicense a work under more permissive terms later if > doing so would align better with your goals. Going from more permissive > terms (like a BSD-style license) to a copyleft (like any version of the > GPL) can be impractical, or result in unintended consequences, because > it is arguably impossible to rescind the permissive license on the older > versions of the code--unless you have an Apple- or Oracle-sized budget > for lawyers to intimidate rivals maintaining the old code base. > > There is probably a better forum for licensing discussions, but my view > is that you've made a perfectly reasonable choice, one that situates > your project squarely and clearly within the Free Software community, > while still leaving you the option to reconsider later. > > Regards, > Branden > > [1] https://microkerneldude.org/2019/12/09/what-does-sel4s-license-imply/ >

1 0

Announcing Neptune OS release v0.1.1: A Windows NT personality for seL4
by Chang Liu 23 Feb '22

23 Feb '22

Hi list, For the past several months I have been working on a project which is to implement a Windows NT personality for the seL4 microkernel, which I have now taken to call “Neptune OS”, named after the codename for Windows 2000. The project has reached the point where I have implemented enough NT primitives such that a keyboard driver stack (taken from the ReactOS source code) can be loaded (as a user process), as well as a command prompt (shell), which is also taken from the ReactOS source code (albeit a very early version of ReactOS). These are all kernel-mode Windows device drivers that I’m running as user processes under seL4. The project is now on github: github.com/cl91/NeptuneOS. The entire system fits in a floppy (download link: github.com/cl91/NeptuneOS/releases/tag/v0.1.0001) Check it out! I think it’s cool! For the next release I’m planning to port the PCI stack, the AHCI stack, and a basic file system (probably fastfat.sys).

4 5

seL4 developer hangout/video call
by Birgit Brecknell 21 Feb '22

21 Feb '22

Hi all A friendly reminder that the seL4 developer hangout is on this week: * Sydney: Wed, Feb 23, 8am * Central Europe: Tue, Feb 22, 10pm * US Pacific Time: Tue, Feb 22, 1pm (There are too many time zones in the world to cite them all :)) Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au seL4 Foundation, birgit(a)sel4.systems 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Ability to change bench app options for RiscV
by Nataliya Korovkina 12 Feb '22

12 Feb '22

Hi, Does anyone remember why sel4bench configuration for RiscV was not allowed to change bench app options? If it was skipped because it was not necessary then I'd like to fix it. I would add a line to https://github.com/seL4/sel4bench/blob/master/apps/sel4bench/CMakeLists.txt --- a/apps/sel4bench/CMakeLists.txt +++ b/apps/sel4bench/CMakeLists.txt @@ -35,14 +35,15 @@ config_string( # Default dependencies on kernel benchmarking features. Declared here so that # all the benchmark applications can use it if( (KernelArchX86 AND KernelExportPMCUser AND KernelX86DangerousMSR) OR (KernelArchARM AND KernelArmExportPMUUser) OR (KernelArchArmCortexA8 AND KernelDangerousCodeInjection) + OR (KernelArchRiscV) ) set(DefaultBenchDeps TRUE) else() set(DefaultBenchDeps FALSE) endif() find_package(musllibc REQUIRED) Thanks, Nataliya

2 1

How to build compile seL4 along with another C++ project that includes <stdlib.h>
by christinefragoso＠protonmail.com 12 Feb '22

12 Feb '22

I want to run my C++ project in a camkes image for i.mx6. This image should be statically linked. I have a camkes app in https://github.com/seL4/camkes-manifest. The app's CMakeLists.txt includes my project with add_subdirectory("${CMAKE_CURRENT_LIST_DIR}/workspace_DDSHelloWorld"), which is a simple DDS example https://fast-dds.docs.eprosima.com/en/latest/fastdds/getting_started/simple… that also uses CMake as its build system. The entire app is built with ../init-build.sh -DPLATFORM=sabre -DCAMKES_APP=dds. However, the build fails. 1. My project includes <stdint.h>, but sel4 uses the -nostdinc and -nostdinc++ flags, so I get the error "stdint.h: No such file or directory". How do I make my C++ project include seL4's musllibc instead? 2. My project includes other C++ headers like <functional>. Is there any way to build seL4 with C++ headers?

2 1

testing rust program in sel4webserver example project
by lfern70＠gmail.com 12 Feb '22

12 Feb '22

Hi, I am trying to compile a simple rust web server to be executed in the virtual machine (as lighthttpd works in this webserver project). This server works perfect (I am using qemu for testing -aarch64), but when I try to get some random bytes using the rand crate the program hangs: .... let mut key = vec![0u8; 32]; rand::thread_rng().fill_bytes(&mut key); ... Do anybody knows if this could be related to some missing settings (in qemu command line or in some device.camkes file) or some rust features that don't work in a sel4 VM?? Thanks

2 1

Call for support contract to the seL4 Foundation
by June Andronick (seL4 Foundation) 11 Feb '22

11 Feb '22

The seL4 foundation is seeking to contract support for the following duties: - address open github issues in the seL4 organisation repositories, with prioritisation directed by the TSC delegates; this includes: - documentation, tutorials - bugs - tests - docsite and possibly website in coordination with Foundation people - help keeping an eye on making sure questions on mailing lists, discourse and github issues are answered (by someone) Requirement for the person working on these tasks are: - multiple years of experience with seL4, both at kernel level and user-level code - good familiarity with the seL4 organisation repositories - active contributor to one or more seL4 repositories - fluent in written and spoken English The seL4 foundation would contract a service company, initially for 6 months. The service company should identify the person that will be performing the work, ideally on a full-time basis. To bid for the contract, send email to foundation(a)sel4.systems before March 4th, 2022 AOE, with the resume of the person that will be performing the work and a cover letter addressing the requirements.

1 0

picoserver and qemu
by lfern70＠gmail.com 08 Feb '22

08 Feb '22

Hi, I am trying to test picoserver app in qemu, but I am not able to connect to the echo component on port 1234. These are the steps I am following, please, let me know if I am doing something wrong. Thanks in advance: $ repo init -u https://github.com/seL4/camkes-manifest.git $ repo sync # use docker container to compile $ container @in-container:/host$ mkdir build @in-container:/host$ cd build @in-container:/host$ ../init_build.sh -DCAMKES_APP=picoserver -DPICOSERVER_IP_ADDR=127.0.0.1 -DSIMULATION=1 @in-container:/host$ ninja Everything seems to be ok, but when I tried to execute in qemu: $ sudo ./simulate --machine q35,accel=kvm,kernel-irqchip=split --mem-size 2G --extra-cpu-opts "+vmx" --extra-qemu-args="--enable-kvm -device intel-iommu,intremap=on,caching-mode=on -netdev user,id=network0,hostfwd=tcp::1234-:1234 -device e1000e,netdev=network0" It seems the echo component is listening on port 1234, but if I try to send data with "netcat 127.0.0.1 1234" I can't reach the echo component ...... IOMMU 0x0: enabling... enabled Booting all finished, dropped to user space 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). listener instance starting up, going to be listening on 192.168.0.21:4321 echo instance starting up, going to be listening on 192.168.0.21:1234

2 3

seL4 developer hangout/video call
by June Andronick (seL4 Foundation) 07 Feb '22

07 Feb '22

Friendly reminder that the seL4 developer hangout is on this week: - Sydney: Wed, Feb 9, 8am - Central Europe: Tue, Feb 8, 10pm - US Pacific Time: Tue, Feb 8, 1pm (There are too many time zones in the world to cite them all :)) Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, June

1 0