November 2017 - Devel - lists.sel4.systems

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

UEFI support for x86
by Edward Sandberg 05 Dec '17

05 Dec '17

Is there a plan to add UEFI support in seL4 for x86 hardware in the near future? Newer x86 boards are frequently UEFI only. It is possible to get around the lack of UEFI support, as I have done with the UP board: https://up-community.org/wiki/Hardware_Specification but I am hitting problems which I will detail below. When I compile using ia32_debug_xml_defconfig and boot using the resulting images the board fails to find the RSDP location. To fix this I had to modify the source code a bit: * seL4test/projects/util_libs/libplatsupport/src/plat/pc99/acpi/acpi.h + #define UPBOARD_RSDP 0x5B161000 * seL4test/projects/util_libs/libplatsupport/src/plat/pc99/acpi/acpi.c - acpi->rsdp = acpi_sig_search(acpi, ACPI_SIG_RSDP, strlen(ACPI_SIG_RSDP), - (void *) BIOS_PADDR_START, (void *) BIOS_PADDR_END); + acpi->rsdp = (void *)UPBOARD_RSDP; * seL4test/kernel/src/plat/pc99/machine/acpi.c - for (addr = (char*)BIOS_PADDR_START; addr < (char*)BIOS_PADDR_END; addr += 16) { + for (addr = (char*)0; addr < (char*)PPTR_BASE; addr += 16) { It would be handy to have this as a kernel parameter to cover cases where it is not successfully discovered automatically. With these changes I can boot the board and several tests pass but then I get stuck on INTERRUPT0001 (Test interrupts with timer). I don't get a test failure or an error the board just sits and makes no more progress. Someone had that test fail in this post: https://sel4.systems/pipermail/devel/2017-February/001328.html and the first recommendation was to check if the irq of the timer was correctly found. I booted the board into linux to find the correct irq which was listed as 0 in /proc/interupts. I added a printf to handleInterrupt in the kernel source, recompiled and when I booted seL4 I found that the irq reported to handleInterrupt is 125 (which sel4 reports as the max interrupt value) every time that function is called. Adding this printf also showed me that when the test hangs the board hasn't crashed or locked up as calls to handleInterrupt are made continuously. At this point I noticed that before any tests started to run several ACPI tables are not recognized: Parsing ACPI tables Skipping table FPDTD, unknown Skipping table FIDT<9c>, unknown Skipping table UEFIB, unknown Skipping table TPM24, unknown Skipping table LPIT^D^A, unknown Skipping table BCFG9^A, unknown Skipping table PRAM0, unknown Skipping table CSRTL^A, unknown Skipping table BCFG9^A, unknown Skipping table OEM0<84>, unknown Skipping table OEM1@, unknown Skipping table PIDVÜ, unknown Skipping table RSCI,, unknown Skipping table WDAT^D^A, unknown Warning: skipping table ACPI XSDT Maybe one or more of those tables needs to be loaded to handle interrupts properly. The LPIT table is conspicuous in the case of the timer test but I think other tests are likely to depend on the other tables. Any suggestions about porting this type of hardware? -- Edward Sandberg Adventium Labs 111 3rd Avenue S. Suite #100 Minneapolis, MN 55401 ed.sandberg(a)adventiumlabs.com

4 10

camkes-gen.mk generated prerequisites
by Gordon Clark 01 Dec '17

01 Dec '17

We have a multi component camkes application with each component using a few common services and then having application interfaces to a small number of other components.All these components are imported into a top level system description camkes file. Examining the generated camkes I see that all the generated header and source files have exactly the same make prerequisites meaning a change to logically unrelated components causes them all to be regenerated and recompiled. Now I have discovered the camkes cache this is less of an issue but is there a better way we can structure our application to reduce the edit-compile-go cycle ? Regards Gordon

2 1

seL4SharedData
by Zippy Maniac 30 Nov '17

30 Nov '17

We have a security requirement on our ARM based product using CAmkES 2.2.x to ensure all sensitive data declared in specific seL4SharedData regions are erased on detection of a power failure. We achieve this by overwriting the data with a known pattern that we read back from a separate component before declaring the device as secured. This is working fine. But we need to guarantee that the overwrite data is actually written to DDR and we aren't just using cached values. This means flushing the L1 and L2 data caches specific regions. We could use seL4HardwareMMIO regions and declare our data in the memory map and use these regions as un-cached. Or use the _hardware_cached attribute and call the provided flush method when necessary. Our main issue with doing this, except the fiddle of mapping multiple different sized regions into the memory map, is we could potentially expose the physical locations of the sensitive data rather than having it wrapped in the virtual address space of a component. Having a flush method on seL4SharedData would be the ideal solution. We are not in a position to upgrade our CAmkES version on this product at the moment. Any thoughts? Zippy

4 3

Tx1 UART and GiC distributor PPTR address
by Muneeswaran Rajendran 27 Nov '17

27 Nov '17

Hi, The PPTR address range between UART and GIC distributor was 12k (kernel/include/plat/tx1/plat/machine/device.h). But when refer in TX1 reference sheet the length was specified as 64byte for UART,4k for GIC distributor and 8k for interrupt controller. can you please point out the reference or reason to choose this address for Tx1 board? /* These devices are used by the seL4 kernel. */ #define UARTA_PPTR 0xffffffffffff0000 #define GIC_DISTRIBUTOR_PPTR 0xffffffffffff3000 #define GIC_CONTROLLER_PPTR 0xffffffffffff4000 These addresses are used during kernel device map to access in the userspace map_kernel_devices : kernel_devices[i].paddr :0x50042000 kernel_devices[i].pptr 0xffffffffffff4000 map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]: 0xffffff800002b000 vaddr :0x1f4 map_kernel_devices : kernel_devices[i].paddr :0x50041000 kernel_devices[i].pptr 0xffffffffffff3000 map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]: 0xffffff800002b000 vaddr :0x1f3 map_kernel_devices : kernel_devices[i].paddr :0x70006000 kernel_devices[i].pptr 0xffffffffffff0000 map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]: 0xffffff800002b000 vaddr :0x1f0 Regards, Munees

1 0

Caught cap fault in send phase at address 0x0 @Tx2
by Muneeswaran Rajendran 23 Nov '17

23 Nov '17

Hi seL4 Dev Team, I am bringing up the sel4 kernel on tx2 board with ref of Tx1. I encountered the TLB invalidation hang issue after kernel map window setup. I do not know the exact reason for hang so just disable that piece of code to look further execution of sel4 kernel. After that it dropped into the usersapce and throwing the cap fault or vm fault issue. Does anyone has come across this type of issue and how it debugged?. Please share your thought or pointers to debug this issue. I shared the full log details here. ## Starting application at 0x82000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p3 paddr=[82000000..827abfff] kernel_phys_start: 0xffffffff80000000 kernel_phys_end:0xffffffff8022fcdf load_elf : image_size 0x230000 ELF-loading image 'kernel' paddr=[80000000..8022ffff] vaddr=[ffffff8000000000..ffffff800022ffff] virt_entry=ffffff8000000000 load_elf : image_size 0x5e9000 ELF-loading image 'sel4test-driver' paddr=[80230000..80818fff] vaddr=[400000..9e8fff] virt_entry=41b160 Enabling MMU and paging Jumping to kernel-image entry point... kernel_info.virt_entry : 0x0 user_info.phys_region_start : 0xffffffff80230000 user_info.phys_region_end:0xffffffff80819000 user_info.virt_region_start:0x400000 user_info.virt_region_end:0x9e9000 user_info.phys_virt_offset:0x7fe30000 user_info.virt_entry:0x41b160 Bootstrapping kernel Booting all finished, dropped to user space Caught cap fault in send phase at address 0x0 while trying to handle: vm fault on code at address 0x41b160 with status 0x82000010 in thread 0xffffff8027ef4200 "rootserver" at address 0x41b160 With stack: halting... Kernel entry via VM Fault, fault type: 4305248 Thanks in advance Muneeswaran R

1 0

Tx1 SMP and Hypervisor support
by Muneeswaran Rajendran 17 Nov '17

17 Nov '17

Hi Sel4 Dev Team, Any update of SMP and Hypervisor feature which fully functional on TX2. If its not available when will get this feature supported . Regards, Munees

3 4

1:1 Mapping of Zynqmp devices
by Chris Guikema 16 Nov '17

16 Nov '17

Hello, I am attempting to port the camkes-arm-vm to the zynqmp platform. For the TK1 and Exynos platforms, the physical address of the hardware devices are well below the kernelBase of 0xe0000000. However, for the zynqmp, these hardware devices are greater than the kernel base. This causes the "map_emulated_device" function call to fail for the GIC and any other passthrough devices. sel4utils_reserve_range_at_no_alloc@vspace.c:589 Range not available at 0xff010000, size 0x1000 Assertion failed: res.res (/home/chrisguikema/seL4/NAMC/camkes-arm-vm/libs/libsel4arm-vmm/src/devices.c: map_device: 160) Is there a way to 1:1 map these devices, even if they are above the kernelBase? Thanks, Chris

2 1

loading and booting seL4 on a tegra Tx2
by Muneeswaran Rajendran 15 Nov '17

15 Nov '17

Hi, I am trying to bring up sel4 on tegra Tx2 platform using tegra Tx1 as reference. I tweaked the important changes of UART,Timer configuration and IRQ number and also GIC controller, GIC distributor configuration w.r.t Tx2 after loading and booting the Tx2 board sel4 enter into init kernel to initialize the kerenl memory map for GIC and UART devices then control transfer to user space. I underdtand from ref manual both Tx1 and Tx2 using the same clock and baud rate for UART configuration. ## Starting application at 0x82000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p3 paddr=[82000000..827abfff] kernel_phys_start: 0xffffffff80000000 kernel_phys_end:0xffffffff8022fcdf load_elf : image_size 0x230000 ELF-loading image 'kernel' paddr=[80000000..8022ffff] vaddr=[ffffff8000000000..ffffff800022ffff] virt_entry=ffffff8000000000 load_elf : image_size 0x5e9000 ELF-loading image 'sel4test-driver' paddr=[80230000..80818fff] vaddr=[400000..9e8fff] virt_entry=41b160 Enabling MMU and paging Jumping to kernel-image entry point... Also try to add debug print in the init kernel thread to understand the virtual memory set-up but its crashed with synchronous exception. It indicates that the UART driver till not available to log the messages this was seen in Tx1 and Tx2. Not able to check/debug further on this issue. Also experimented with various arbitrary address for UARTA_PPTR and GIC_PPTR because Tx1 UARTA has 64byte size in case of Tx2 its 1MB.but still nothing has improved the state remain same. I completely walk through the sel4 boot and arm MMU code.I do not see any board specific changes in this code apart from UART,GIC configuration and IRQ number. The assembly code of MMU mainly setting up TCR ,TTBR , TLB invalidation and pagetable setup for arma-57. Please let me know your thought on this issue and how do debug this kind of issue. Regards, Munees

2 2

loading and booting seL4test on a zynq7000
by Joel Svensson 13 Nov '17

13 Nov '17

Hello, I want to learn about seL4 so I am trying to get is started on the hardware I already have (a zynq 7000). I have generated the image: sel4test-driver-image-arm-zynq7000 Now I try to load that onto the zynq by executing these commands in XMD: connect arm hw rst fpga -f design_1_wrapper.bit source ps7_init.tcl ps7_init ps7_post_config dow sel4test-driver-image-arm-zynq7000 run All of the above seem to be successful. Then, I have a serial link hooked up to the board (uart) and there I get the following output (screen /dev/ttyUSB1 115200) : ELF-loader started on CPU: ARM Ltd. Cortex-A9 r3p0 paddr=[10000000..103c881f] ELF-loading image 'kernel' paddr=[0..2afff] vaddr=[e0000000..e002afff] virt_entry=e0000000 But then nothing more. I am lost what to do from this position in order to continue exploring seL4. I don't even know if what I see is an indication of a problem or not. If anyone has experience in running seL4 on zynq and if you sit on knowledge you want to share, please fill me in. Thank you

2 6

CAmkES mutex Question
by Brandon, Jeffrey - 0553 - MITLL 06 Nov '17

06 Nov '17

Hi, I've been taking a look at mutex implementations in the camkes-app example and I had a question. In the mutex example here https://github.com/seL4/camkes/tree/master/apps/mutex suppose I wanted to extend to add a third component C I need to add the corresponding camkes, source, Kbuild, and Kconfig files and then I need to add connections to the master mutex.camkes file correct? My first intuition was to add a connector: Assembly { Composition{ . Connection seL4MyConnector connection(from c.lock, to b.lock); . } } But this yields and error saying something to the effect "seL4MyConnector expects one from endpoint and two are specified" To remedy this I added another lock component to B, and made a connection between C and this new lock B provides. The new lock being implemented by the same template. My Questions: In this scenario do A B and C still have access to the same mutex? If A has a lock on the mutex, then C requests a lock, will this cause A to be unable to release the lock? In my mental model I have three threads of control, one each for A B and C, if A has a lock and then C requests a lock, does this block B (when it receives a message from C and is now blocked on requesting the mutex)? Then when A tries to release, B is blocked and cannot release the mutex on A's behalf. To put it another way, does this mutex example rely on B having direct access to the templated code and there only being two components? Secondarily, in the lockserver example https://github.com/seL4/camkes/tree/master/apps/lockserver a situation is presented where three clients access a single mutex through a single server. Would there be an issue if one of the clients also acted as the server? So for instance if A implemented the three pairs of lock unlock functions instead of the server and then B and C used seL4RPCCall connections to A in order to access them, would there be any synchronization issues? I'm relatively new to this and am trying to build a system with the help of camkes and I want to make sure I understand this before I get too far. I don't want to be working under incorrect assumptions. Thanks for taking the time to read this. Sincerely, Jeff Brandon Associate Staff MIT Lincoln Laboratory Secure Resilient Systems and Technology Ph: +1 781.981.9233

3 2

PPTR address computation on Sel4 Kernel
by Muneeswaran Rajendran 05 Nov '17

05 Nov '17

Hi sel4 development team, I understand from the sel4 kernel the paddr and pptr used in the kernel framework to compute the page table entry. I found from ref manual GICD_PADDR defined as (ARM_PERIPHBASE (0x50040000) + 0x1000) 0x50041000 for that GIC_DISTRIBUTOR_PPTR used as 0xffffffffffff3000. This details was not able to see in the ref manual and other sel4 reference. Can someone help to understand the pptr calculation w.r.t sel4? Thanks in advance Munees

2 1

UART initialisation on seL4 @TX1
by Muneeswaran Rajendran 03 Nov '17

03 Nov '17

Hi sel4 development team, I understand from the seL4 kernel the initial printf message are not routed through sel4 platform uart driver. Because the sel4 UART driver initialisation happened later when seL4 Main kernel initialization is finished. till then sel4 kernel uses u-boot UART driver to route the message. This interpretation is correct as per my understanding. Also mentioned in code as well debug output available via serial interface after kernel init thread started. /* debug output via serial port is only available from here */ printf("Bootstrapping kernel\n"); It means that when sel4 kernel comes up with u-boot uart driver and then later using sel4 uart driver. Please correct me if any thing wrong here and throw some input. Regards, Munees

2 2