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

seL4 summit 2024: survey about location
by Birgit Brecknell 29 Nov '23

29 Nov '23

Dear seL4 friends, With the great success of the seL4 summit 2023 behind us, we are now looking at the seL4 summit 2024! This should happen around Sep/Oct 2024. We have started investigating options for the location, and we would like your feedback. We would greatly appreciate it if you could fill in this very short survey to tell us your opinion between Abu Dhabi and Sydney: https://forms.gle/LQKSHVrqLGNqV2Ld8 Please do so by Nov 22nd 2023. Feel free to forward to anyone you believe may want to attend the summit next year. Many thanks! June & Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

2 3

How to avoid priority inversion in seL4
by chenpingyuan＠xiaomi.com 29 Nov '23

29 Nov '23

Hello experts, I'm reading the code of seL4 kernel, but I got confused how seL4 could help to avoid priority inversion. seL4 itself doesn't change the priority of TCB at the kernel level, does it mean that seL4 leaves the user level to handle priority inversion? Regards Neil.

2 2

A few questions regarding seL4
by Benjamin J. Kelly 29 Nov '23

29 Nov '23

To Whom It May Concern, My name is Ben Kelly. Myself and my partner James Briscoe - CC'd on this email - are in the beginning stages of starting a company that will host websites and web services for clients requiring high security on hardware that we control from the firmware up. We haven't decided which OS we want to use yet. Our initial goal is a customizable OS that contains only the minimum services to host a web server and nothing else. We will be evaluating the seL4 Microkernel. We're also intrigued by the possibilities of enhanced application performance and security that can be had from a unikernel approach. Is there anything that would forbid using the seL4 MicroKernel acting as a 'hypervisor/scheduler' for highly isolated and performant unikernel applications? If not, seL4 and Unikernel technology could potentially deliver the maximum amount of performance and security possible for hardware running seL4-compatible CPUs. In the following video Boyd Multerer, https://youtu.be/YG5BaoB24eA?si=TcxHq51Q5HLC0m1_ was asked the question if seL4 would "make sense on servers." Boyd replied that "I think it would but it's not something that we are targeting ... yet." He also said that "Yeah, I do think seL4 would be perfect at the bottom of the server once the multi-core thing gets figured out. But we don't need to solve that right away." Do you think seL4 is mature enough for our purpose? If we were to invest our time doing a deep dive into understanding seL4 do you know of any companies that are willing to pay for our acquired knowledge? Very Respectfully, Benjamin J. Kelly President Windsor Lake Computing LLC http://windsorlake.llc/ Sent with [Proton Mail](https://proton.me/) secure email.

3 5

Reminder seL4 developer hangout
by Birgit Brecknell 27 Nov '23

27 Nov '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Nov 29, 8am For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

How to run seL4 on FVP?
by Hesham Almatary 23 Nov '23

23 Nov '23

Hello, I can build sel4test for FVP, how do I run it there? I couldn't find any documentation on that, would be great if someone could drop a command line and any required dependencies. Regards, Hesham

3 4

Use C-parser on seL4 based application
by r2ji＠uwaterloo.ca 20 Nov '23

20 Nov '23

Hi, I have been trying to reuse the seL4 verification framework to verify a toy example I built on seL4, and I am currently stuck on the c-parser step. I am trying to use c-parser to parse the example I built, then conduct refinement verification. The toy example is a normal c project, which includes `sel4.h`. From this thread: https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/3QYNFY… I learned that I am supposed to do $ ./isabelle/bin/isabelle jedit -d . -l CParser toy.thy And the toy.thy file is supposed to begin with `install_C_file("toy.c")`. However, since toy.c includes sel4.h, I am not sure how to preprocess it before I put it into toy.thy. I know the standalone c-parser can have a -I flag to include in all the dependency directories, but it cannot open an interactive window. (From my understanding, the standalone c-parser seems to be only a checking tool) I also know that when sel4 is parsed into HOL, it is preprocessed into a single c file `kernel_all.c_pp`, which is later parsed. I am not sure if the preprocessor tool can be reused for other applications as well. My question is summarized as: 1. Is there a way to add an include directory in interactive CParser? 2. If not, can I reuse the preprocessing approach for sel4 to preprocess my application to a singleton file that can be parsed by c-parser? Any help will be appreciated! Thanks, Ru

2 2

Conclusions regarding speculation
by Demi Marie Obenour 18 Nov '23

18 Nov '23

I talked with a Xen developer and came to these conclusions: - Speculative taint tracking provides complete protection against speculative attacks. This is sufficient to prevent leakage of cryptographic key material, even in fully dynamic systems. Furthermore, it is compatible with fast context switches between protection domains. - Full time partitioning eliminates all timing channels, but it is possible only in fully static systems, which severely limits its applicability. - Time protection without time partitioning does _not_ fully prevent Spectre v1 attacks, and still imposes a large penalty on protection domain switches. Additionally, I am almost certain that: - On properly designed hardware, both time protection and speculative taint tracking can be enabled and disabled by systems software. - Time protection and speculative taint tracking are not mutually exclusive. A cloud provider might use time partitioning to partition different customers from each other, while guest OSs use speculative taint tracking to protect different processes from each other. In short, time protection is excellent, but it is not a sufficient mechanism for general-purpose computing. Speculative taint tracking is a different mechanism that is applicable to many more workloads, and which provides complete protection against speculative attacks. Both mechanisms can be used together depending on system security policy. -- Sincerely, Demi Marie Obenour (she/her/hers)

6 18