November 2021 - 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

seL4 developer hangout/video call
by Gerwin Klein 25 Jan '22

25 Jan '22

Hi seL4 devs, a few of us thought it might be nice to talk more directly from time to time rather than only via pull requests, so we're trialling a seL4 developer hangout/video chat. The idea for this is to be: - informal, about 1h - for technical discussions about seL4 and related repositories - anyone can join - every two weeks, initially for 3 times, then we can decide how we like it At least one or two technical steering committee (TSC) members will try to be at every one of these, but these are not TSC meetings where formal decisions are made, just technical discussions about whatever people have on their minds. To provide a starting topic, one thing we'd be interested in is: seL4 boot code There have been quite a few pull requests in that area, and it'd be nice to know what people's plans are and how we can keep this part of seL4 high assurance while making it more flexible. Other topics for future meetings could be better support for other language bindings (e.g. Rust), any RFCs that are open or people are thinking about opening, or just discussions about current pull requests or issues. The first hangout is on - Sydney: Wed, Nov 3, 8am - Central Europe: Tue, Nov 2, 10pm - US East Coast: Tue, Nov 2, 2pm Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Gerwin

2 9

capdl-loader questions
by Sam Leffler 08 Dec '21

08 Dec '21

I've been investigating how capd-loader works and have some questions. My apologies if these were previously discussed. 1. CDL_Model is mutable. The capDL specification looks like a perfect candidate for being in .rodata but it's stored+treated as mutable. Why? I see capdl-loader uses the mutability to store mapped page frame caps and, for risc-v, VSpace roots, but both can be easily handled w/o modifying the spec. Having this immutable has many benefits. 2. All page frames are treated as shared. CAPDL_SHARED_FRAMES is #define'd in the code so every frame is treated as shared. This inflates the size of the orig_caps array and the kernel capabilities table but seems unnecessary. Why? I've verified that instead of doing the Copy op on each page you can just check the return of the seL4_Page_Map call and if necessary clone the cap. Better would be for camkes to identify shared page frames so this doesn't require 2x syscalls (which spam's the console w/ CONFIG_PRINTING enabled). 3. Why does copy_addr_with_pt exist? There are two memory regions created for mapping page frames into the rootserver address space for doing fill ops. One is 64KB and the other is 1 page (nominally 4KB). init_frame tries the 4KB region first then falls back to the 64K region if mapping into the 4KB region fails. Why (i.e. why would the 1st mapping call fail)? On my risc-v system I never use the 64K region and I'm not sure when it might be used? Even if it were used, why is 64K always allocated; seems like the region should be sized according to the target platform. Having this extra region has a cost that can be significant on small systems. 4. console output. Why is sel4_DebugPutChar (or similar) not a standard part of the kernel? This forces capdl-loader to depend on libsel4platsupport for console output which in turn affects cap space. I can't imagine an seL4 system that cannot write to the console and I think it's entirely reasonable to have a critical system service like the rootserver use that. 5. duplicate_caps. The scheme for constructing a running system from a spec is straightforward except for duplicating caps. Why are all TCB's and CNode caps dup'd? Why does init_tcbs call init_tcb on the original object but immediately configure_tcb on the dup? There are other places where the dup cap is used instead of the original cap (e.g. init_cnode_slot). None of this seems to matter on risc-v; maybe this matters on some other architectures? 6. On risc-v all pages appear to be marked executable--including ipc buffers! This seems just wrong and a potential security hole. 7. Why does seL4_TCB_WriteRegisters take a _mutable_ seL4_UserContext? I'm guessing this is a mistake in the xml spec (but haven't looked). 8. init_cspaces mystifies me. There are two loops over all CNodes; one that does "COPY" operations and one that does "MOVE" operations. I see nothing explaining what's happening. I've read this code many times and still don't get it; please explain. 9. According to comments, the use of a global static to setup the UserContext for a new TCB is done because one cannot take the address of a local variable. On what architecture is this true? On risc-v the context is copied into "registers" before calling the kernel so this doesn't appear to be an issue with crossing the user-kernel protection boundary. 10. Memory reclamation. I'm unclear what happens to the memory used by capdl-loader. The process does a TCB_Suspend call when it's done. Does this cause the CSpace & VSpace to be reclaimed? For CAmkES this doesn't matter as there's no support for allocating memory but I'm building a system where this isn't true. How do I release memory (in particular) back to the untyped pool? I have a bunch of niggly code complaints/questions but let's start with the above. -Sam

2 4

VM Kernel Modules
by Michael Neises 20 Nov '21

20 Nov '21

Hello all, I recently spent a lot of time getting the camkes-vm-linux tutorial to work, because it is the only example I could find of compiling a kernel module for the linux vm as a part of the camkes build process. Unfortunately, the kernel module doesn't seem to work. For more information, see the previous email chain as well as https://github.com/NeisesResearch/vm_measure/wiki/Building-the-camkes_vm_li… . In lieu of doing things the right way, I believe I could compile a kernel module for the linux kernel that is provided as part of the camkes build system. I believe this is how the introspect-app accomplishes its work. However, I need to have the exact kernel and exact configuration in order to compile the kernel module correctly. Can anyone point me to the correct kernel version and configuration, so that I can target the provided linux kernel for module compilation? Or if there's a better way to get a kernel module in there, please let me know. Cheers, Michael Neises

4 5

the security whiltelist of smc call 答复: Devel Digest, Vol 124, Issue 1
by yadong.li 19 Nov '21

19 Nov '21

Hi: In our ARMv8 platform，we access secure world not only from the VM guest OS， but also form native compont like config clk register In ARMv8 platform, SMC instructions are not allowed from EL0. So in camkes-vm project, I create a new smc capability and a new syscall as a temporary solution, like below: "LIBSEL4_INLINE seL4_ARM_SMC_CallFunc_t seL4_ARM_SMC_CallFunc(seL4_ARM_SMC _service, seL4_Word function_id, seL4_Word arg0, seL4_Word arg1, seL4_Word arg2)" But I did not pay much attention to security, it is just meet our current work. I didnot really understand the essence of kernel whitelist mentioned by "https://sel4.atlassian.net/browse/RFC-9"? I have some question below, I feel the smc cap should like schedcontrol cap belong every core. 1. what is the whiltelist describe ? sip command smc function id? 2. how are the members of whilelist represented in the kernel , check the invLabel of syscall in kernel if we provide one smc cap not every function id? or just check the range of function id ? 3. Does each TCB have its own whitelist or does the entire system have a whitelist? thank you very much. -----邮件原件----- 发件人: devel-request(a)sel4.systems [mailto:devel-request@sel4.systems] 发送时间: 2021年11月10日 9:00 收件人: devel(a)sel4.systems 主题: Devel Digest, Vol 124, Issue 1 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. RFC-9: new capability for seL4 SMC Forwarding on Arm (Gerwin Klein) ---------------------------------------------------------------------- Message: 1 Date: Tue, 9 Nov 2021 21:52:58 +0000 From: Gerwin Klein <kleing(a)unsw.edu.au> Subject: [seL4] RFC-9: new capability for seL4 SMC Forwarding on Arm To: devel <devel(a)sel4.systems> Message-ID: <613858AC-3DB1-4D7C-A892-9ABDB5B31D58(a)unsw.edu.au> Content-Type: text/plain; charset="utf-8" I’d like to solicit discussion on the new RFC on forwarding Secure Monitor Calls on Arm: https://sel4.atlassian.net/browse/RFC-9 Relevant Arm documentation (SMC calling conventions): https://developer.arm.com/documentation/den0028/latest?_ga=2.116565828.3903… Any opinions, concerns, alternative designs? Cheers, Gerwin ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems ------------------------------ End of Devel Digest, Vol 124, Issue 1 *************************************

1 0

Got it, Thank you for your help. 答复: Devel Digest, Vol 125, Issue 2
by yadong.li 18 Nov '21

18 Nov '21

-----邮件原件----- 发件人: devel-request(a)sel4.systems [mailto:devel-request@sel4.systems] 发送时间: 2021年11月18日 5:56 收件人: devel(a)sel4.systems 主题: Devel Digest, Vol 125, Issue 2 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Re: some question about seL4 performance (Gerwin Klein) 2. Re: some question about seL4 performance (Gernot Heiser) 3. Re: some question about seL4 performance (Gerwin Klein) ---------------------------------------------------------------------- Message: 1 Date: Wed, 17 Nov 2021 21:24:57 +0000 From: Gerwin Klein <kleing(a)unsw.edu.au> Subject: [seL4] Re: some question about seL4 performance To: yadong.li <yadong.li(a)horizon.ai> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Message-ID: <CA210292-C334-42C1-9FB4-48CAFDE8CCC6(a)unsw.edu.au> Content-Type: text/plain; charset="utf-8" > On 18 Nov 2021, at 02:06, yadong.li <yadong.li(a)horizon.ai> wrote: > > Hi： > I learn the sel4 performance form > https://sel4.systems/About/Performance/ > I focus on the ARMv8 platform, from the website, the parameters are as follows: > ISA Mode Core/SoC/Board Clock IRQ Invoke IPC call IPC reply > "Armv8a 64 A57/Tx1/Jetson 1.9 GHz 863 (18) 396(15) 397(4)" > > I want to know what is the length of IPC for the record provided on the web page , when test IPC call and reply? 0 or 10? The page reports the 0-length numbers. The idea is that IPC should fit into registers, the 10 case is the one that make it spill into memory deliberately. That number is good to know for development, but should not be the main performance characteristic. Cheers, Gerwin ------------------------------ Message: 2 Date: Wed, 17 Nov 2021 21:36:39 +0000 From: Gernot Heiser <gernot(a)unsw.edu.au> Subject: [seL4] Re: some question about seL4 performance To: "devel(a)sel4.systems" <devel(a)sel4.systems> Message-ID: <9885F4AB-61C0-46CD-B239-595E38482673(a)unsw.edu.au> Content-Type: text/plain; charset="utf-8" On 18 Nov 2021, at 08:24, Gerwin Klein <kleing(a)unsw.edu.au> wrote: > > The page reports the 0-length numbers. The idea is that IPC should fit into registers, the 10 case is the one that make it spill into memory deliberately. That number is good to know for development, but should not be the main performance characteristic. Note that whether data is transferred solely in registers or using a memory buffer does not make a big difference on contemporary hardware. However, our present implementation reverts to the slow path as soon as the message size overflows the physical message registers, which will make the PIC much slower. This is something that could be fixed by widening the fastpath conditions without much complications. However, we haven’t yet come across an important use case where this matters, so there isn’t much motivation for investing time in it. Gernot ------------------------------ Message: 3 Date: Wed, 17 Nov 2021 21:56:06 +0000 From: Gerwin Klein <kleing(a)unsw.edu.au> Subject: [seL4] Re: some question about seL4 performance To: Gernot Heiser <gernot(a)unsw.edu.au> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Message-ID: <FFD95815-9F62-4A90-A3D0-59671152494D(a)unsw.edu.au> Content-Type: text/plain; charset="us-ascii" On 18 Nov 2021, at 08:36, Gernot Heiser <gernot(a)unsw.edu.au<mailto:gernot@unsw.edu.au>> wrote: On 18 Nov 2021, at 08:24, Gerwin Klein <kleing(a)unsw.edu.au<mailto:kleing@unsw.edu.au>> wrote: The page reports the 0-length numbers. The idea is that IPC should fit into registers, the 10 case is the one that make it spill into memory deliberately. That number is good to know for development, but should not be the main performance characteristic. Note that whether data is transferred solely in registers or using a memory buffer does not make a big difference on contemporary hardware. However, our present implementation reverts to the slow path as soon as the message size overflows the physical message registers, which will make the PIC much slower. Yes I should have mentioned that. If you look at the raw numbers for x86, eg. at https://github.com/seL4/sel4bench/actions/runs/1469475721#artifacts, fast path/no fast path is almost equal for length 10. You get a tiny bit better performance for length 10 when the fast path is switched off completely, because it doesn't first have to test whether to take the fast path or not. Cheers, Gerwin ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems ------------------------------ End of Devel Digest, Vol 125, Issue 2 *************************************

1 0

some question about seL4 performance
by yadong.li 18 Nov '21

18 Nov '21

Hi： I learn the sel4 performance form https://sel4.systems/About/Performance/ I focus on the ARMv8 platform, from the website, the parameters are as follows: ISA Mode Core/SoC/Board Clock IRQ Invoke IPC call IPC reply "Armv8a 64 A57/Tx1/Jetson 1.9 GHz 863 (18) 396(15) 397(4)" I want to know what is the length of IPC for the record provided on the web page , when test IPC call and reply? 0 or 10? thank you very much

3 3