January 2018 - 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

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

18 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

RefOS Building and Execution Error
by ALVI Aslam (MORPHO) 09 Feb '18

09 Feb '18

Hello Team, I was currently understanding the RefOS but the current code which is present in GIT is not Buildable at all. But after doing some workaround by myself I was able to build it successfully. While executing it on simulator for Kzm 1. Bootstrapping Kernel all finished successfully 2. Dropped to user Space successfully 3. RefOS initialize done successfully 4. Running RefOS Process Server failed In the step 4 while running the Process server it failed while proc_config_new() Failed to spawn Process for Console_server. So Far as per my debugging while coping and writing the elf Header it get failed while getting the capabilities. Excat error line vspace_internal.h line number 396. I would be a great support if anybody help me to resolve the issue. Thank You in advance Regards Aslam Alvi

2 1

OS Engineers Wanted!
by Gernot.Heiser＠data61.csiro.au 30 Jan '18

30 Jan '18

Would you like to get paid for making the world more secure with seL4? I'm in charge of directing OS development for the newly-founded company Hensoldt Cyber. We will develop an integrated, highly-secure hardware-software solution, combined with secure production, aimed at changing the game in securing real-world embedded/cyber-physical systems. Needless to say, there will be close collaboration with the Data61 Trustworthy Systems team. We're now hiring engineers who will help us getting there. Specifically, we're looking for strongly-motivated people with practical experience in OS development, although there is flexibility with the degree of experience. Actual experience with seL4 (or even lesser microkernels ;-) would be awesome. Place of work will be Munich (no remote work possible, sorry). You'll have to be prepared to obtain a German government security clearance (German citizenship is not a requirement for this). Interested? Please send me your CV. Gernot

1 0

seL4 as TEE OS in TrustZone
by Daniel (Xiaolong) Wang 29 Jan '18

29 Jan '18

Hi all, I’m exploring for possible ways to run seL4 as a secure TEE kernel in TrustZone. I found an old discussion thread back in 2016 and corresponding from Gernot: I’m very new to TrustZone technology. I wonder has anyone done that before using seL4? Is there any public available resources for reference? Also on which development board did Data61 run seL4 in the secure world? Thanks -Dan FYI Is it possible to run sel4 as a secure world OS in TrustZone? Has anyone successfully done that before? I believe we have done that in the past (with platforms where we could just ignore the secure/normal split and ran everything in secure mode). There is no reason why it wouldn’t work, it just comes down to initialising the platform correctly. https://sel4.systems/pipermail/devel/2016-March/000750.html <https://sel4.systems/pipermail/devel/2016-March/000750.html> Thanks -Dan

4 7

seL4 as a hypervisor running a linux guest and a RToS(or native sel4 applications) on ARM
by Joel Svensson 29 Jan '18

29 Jan '18

Hello, I'm trying to form an understanding of what one can do with seL4 and how much work is involved in doing it. I am currently under the impression that seL4 could act as a hypervisor and run a linux guest. But I have not found easily accessible instructions for how to do this (ARM targets are most interesting, the Raspberry Pi preferably as it is cheap and ubiquitously available). Did anyone here set up such a seL4 as hypervisor for linux guest and document the procedure? I would be very thankful for links. If such a setup is doable, can you still run some native seL4 code on the "hypervisor" then? Thank you very much /JS

2 2

python-capdl sets incorrect permissions on elf setions
by Joseph Takagi 28 Jan '18

28 Jan '18

Hi I believe the capdl python tool does not correctly set permissions on data loaded from component ELF files. I am wondering if this is a known issue with a fix or whether I'm best off diving in and attempting to fix it myself. Im running on a 32-bit ARM platform The camkes generated linker scripts result in several ELF sections (including .rodata .text and .bss) being lumped together in a single ELF segment. The permissions on this segment in the ELF segment header are RWE. This can be seen from the example output below. readelf -l foo_group_bin Elf file type is EXEC (Executable file) Entry point 0x107b64 There are 4 program headers, starting at offset 52 Program Headers: Type Offset VirtAddr PhysAddr FileSiz MemSiz Flg Align EXIDX 0x021ad8 0x00111ad8 0x00111ad8 0x00008 0x00008 R 0x4 LOAD 0x010000 0x00100000 0x00100000 0x12178 0xd9000 RWE 0x10000 <-- .bss .text .rodata etc. are here with RWE permissions LOAD 0x030000 0x00200000 0x00200000 0x00000 0x01000 RW 0x10000 GNU_STACK 0x000000 0x00000000 0x00000000 0x00000 0x00000 RWE 0x10 Section to Segment mapping: Segment Sections... 00 .ARM.exidx 01 .text .init .fini .rodata .eh_frame .ARM.exidx .data .init_array .fini_array .jcr __vsyscall .bss guarded 02 ignore_fooregs 03 The individual sections are given more sensible permissions via their respective section headers, as can be seen below: .text has permissions 'AE' for alloc and execute, .rodata has 'A' and .bss has 'AW', etc. readelf -S ./foo_group_bin There are 28 section headers, starting at offset 0x8524c: Section Headers: [Nr] Name Type Addr Off Size ES Flg Lk Inf Al [ 0] NULL 00000000 000000 000000 00 0 0 0 [ 1] .text PROGBITS 00100000 010000 00eb68 00 AX 0 0 4096 <-- .text can't be written [ 2] .init PROGBITS 0010eb68 01eb68 000014 00 AX 0 0 4 [ 3] .fini PROGBITS 0010eb7c 01eb7c 000014 00 AX 0 0 4 [ 4] .rodata PROGBITS 0010f000 01f000 002ad4 00 A 0 0 4096 <-- .rodata is read-only [ 5] .eh_frame PROGBITS 00111ad4 021ad4 000004 00 A 0 0 4 [ 6] .ARM.exidx ARM_EXIDX 00111ad8 021ad8 000008 00 AL 1 0 4 [ 7] .data PROGBITS 00112000 022000 000168 00 WA 0 0 4096 [ 8] .init_array INIT_ARRAY 00112168 022168 000004 00 WA 0 0 4 [ 9] .fini_array FINI_ARRAY 0011216c 02216c 000004 00 WA 0 0 4 [10] .jcr PROGBITS 00112170 022170 000004 00 WA 0 0 4 [11] __vsyscall PROGBITS 00112174 022174 000004 00 WA 0 0 4 [12] .bss NOBITS 00112178 022178 000b08 00 WA 0 0 8 [13] guarded NOBITS 00113000 022178 0c6000 00 WA 0 0 4096 [14] ignore_fooregs NOBITS 00200000 030000 001000 00 WA 0 0 1048576 [15] .debug_info PROGBITS 00000000 022178 027a60 00 0 0 1 [16] .debug_abbrev PROGBITS 00000000 049bd8 00a4d4 00 0 0 1 [17] .debug_loc PROGBITS 00000000 0540ac 0113f1 00 0 0 1 [18] .debug_aranges PROGBITS 00000000 0654a0 000ef8 00 0 0 8 [19] .debug_line PROGBITS 00000000 066398 00c5ff 00 0 0 1 [20] .debug_str PROGBITS 00000000 072997 0060c1 01 MS 0 0 1 [21] .comment PROGBITS 00000000 078a58 000038 01 MS 0 0 1 [22] .ARM.attributes ARM_ATTRIBUTES 00000000 078a90 000039 00 0 0 1 [23] .debug_frame PROGBITS 00000000 078acc 002638 00 0 0 4 [24] .debug_ranges PROGBITS 00000000 07b108 002238 00 0 0 8 [25] .shstrtab STRTAB 00000000 085137 000114 00 0 0 1 [26] .symtab SYMTAB 00000000 07d340 005230 10 27 1269 4 [27] .strtab STRTAB 00000000 082570 002bc7 00 0 0 1 Key to Flags: W (write), A (alloc), X (execute), M (merge), S (strings) I (info), L (link order), G (group), T (TLS), E (exclude), x (unknown) O (extra OS processing required) o (OS specific), p (processor specific) The ELF.py code from python-capdl applies the segment permissions to the entire segment so disregards the permissions in the ELF section headers. As a result, data which shouldn't be writable or executable are so. I can confirm this through analysis of the capdl output which shows the entire segment being mapped as 64KB pages with RWE permissions set. Any advice on this would be appreciated. Joe Takagi

2 1

Fileserver connection error in RefOS
by ALVI Aslam (MORPHO) 23 Jan '18

23 Jan '18

Hello All, Greetings, I was trying to run RefOs for ia32_defconfig. Found some error while building but after removing all of them I was able to run it. But now I have an error while selfLoader is trying to laod Terminal or Timer_Server. [00.0] SELFLOADER | main(): --- Starting RefOS process selfloader --- [00.1] SELFLOADER | main(): Connect to the server for [/fileserv/terminal] ERROR main(): Error while connecting to file server. [00.84] PROCSERV | proc_exit_handler(): Process PID 2043 exiting with status 0 !!! [00.85] PROCSERV | proc_syscall_postaction(): Releasing process 2043 [/fileserv/terminal]... [00.0] SELFLOADER | main(): --- Starting RefOS process selfloader --- [00.1] SELFLOADER | main(): Connect to the server for [fileserv/timer_server] ERROR main(): Error while connecting to file server. I have also attached the full log of execution. I have also debugged it and found that while resolving the serverPath its get failed. Please help me out to resolve this issue. Thank You in advance Regards, Aslam

1 0

Hyperkernel paper
by Jeff Waugh 23 Jan '18

23 Jan '18

Hi seL4 friends, Any thoughts and/or feelings about the Hyperkernel paper from SOSP'17? This paper describes an approach to designing, implementing, and formally > verifying the functional correctness of an OS kernel, named Hyperkernel, > with a high degree of proof automation and low proof burden. https://homes.cs.washington.edu/~helgi/papers/hyperkernel.pdf Thanks, Jeff

2 1