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

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

CfP: Microkernel and Component-based OS Devroom at FOSDEM 2024
by Martin Decky 16 Nov '23

16 Nov '23

Microkernel and Component-based OS Devroom at FOSDEM 2024 CALL FOR PARTICIPATION On-line version of this CfP: http://fosdem.microkernel.info/ The developers and users of several free and open source microkernel-based, unikernel-based and component-based operating systems will meet as part of FOSDEM 2024 [1] and will share a developer room. The devroom is currently looking for content in the form of talks and other activities related to microkernel-based, unikernel-based, component-based operating systems and similar areas. Possible topics of the devroom include, but are not limited to: * introduction of a specific OS or framework * design of subsystems and the general architecture of an OS * languages, tools and toolchains used * enabling support for hardware (architectures, device drivers) and programming languages * development processes, debugging * maintenance, testing and release engineering * safety, security and robustness * trends and challenges * research and open questions * community and governance * use cases, experiences and status updates * best practices and lessons learned * demos The devroom has been scheduled to Saturday February 3rd 2024 in the afternoon (Central European Time). This is a call for your participation. We kindly ask you to submit your proposals no later than on December 10th 2023 (End of Day, Anywhere on Earth). Please use the pretalx [2] web site to submit your proposals. Note that this is a new submission system and the user accounts from the previous submission system (pentabarf) have not been transferred. Make sure to select the Microkernel and Component-based OS as the track when submitting your proposal and include at least the following information: * title of your proposal * short abstract (one or two paragraphs) * duration (at least 15 minutes and no longer than 40 minutes) * your full name * your short bio You can specify your preferred time slot of your proposal and any other relevant information. The communication language of the devroom is English. Please note that the devroom has been allocated only a half of a day this year. Therefore the final decision on the duration of the talks will be made by the devroom organizers based on the number of accepted proposals. The official devroom schedule (along with the accepted talks) will be announced on December 15th 2023 on the devroom's mailing list [3] and the speakers will be notified via e-mail. The schedule will be published on the FOSDEM web site, too. About the Devroom Since the first Microkernel OS Devroom at FOSDEM 2012 [4], this devroom has been a part of each following FOSDEM (with slight variations of the name). The focus gradually widened to include component-based, unikernel-based and other operating systems. By now, it has become a somewhat institutionalized tradition for the open source operating systems community, a kind of "extended family meeting" and it is one of the places where microkernel and unikernel enthusiasts meet regularly. To this date, over two dozen projects have participated in one way or another. Many of the projects face similar challenges but come up with partially different solutions. Therefore, the goal of the devroom is to bring the various projects together, let them exchange ideas, cross-pollinate and socialize. As every previous year, the devroom will offer the "stage" both to established community members and to newcomers. We like to select the talks in an inclusive manner, while staying true to the main technical topics (system-level software, broadly speaking) and creating a balanced and unbiased schedule. We would like to keep the quality bar of the devroom same as in the previous years. Presenting at FOSDEM implies that the recordings of the talks will be published under Creative Commons license by FOSDEM. By submitting a proposal, the speaker agrees to have the talk made available publicly indefinitely. For organizational purposes, we also need contact information of the speakers of accepted talks. Microkernel Dinner It has also become a habit that the devroom participants dine together somewhere in Brussels. The year 2024 will not be any different, so there is going to be a dinner on Saturday night. We will inform you about the exact arrangements later. About FOSDEM FOSDEM [5] is a two-day conference organized by volunteers to promote the widespread use of free and open source software. FOSDEM is widely recognized as one of the largest and best such events worldwide. FOSDEM covers a wide spectrum of free and open source software and hardware projects and offers a platform for people to collaborate. To this end, FOSDEM has set up developer rooms (devrooms) where teams can meet and showcase their projects. Devrooms are a place for teams to discuss, hack and publicly present latest directions, lightning talks, news and proposals. Besides developer rooms, FOSDEM also offers main tracks, lightning talks, certification exams and project stands. In recent years, FOSDEM has been hosting more than 8000 developers annually at the ULB Solbosch Campus in Brussels, Belgium. The participation in FOSDEM is totally free, although the organizers gratefully accept donations and sponsorship. No registration is necessary. Attendees are expected to follow the [6]FOSDEM's code of conduct. Important Dates Recap * 2023-12-10: Deadline for proposal submission * 2023-12-15: Schedule published and speakers notified of acceptance * 2024-02-03: Devroom taking place Contact For any comments, questions and suggestions, please do not hesitate to use the devroom's mailing list [3] to contact the devroom organizers. The primary organizers of the devroom in 2024 are: * Martin Decky * Razvan Deaconescu References [1] https://fosdem.org/2024/ [2] https://pretalx.fosdem.org/fosdem-2024/cfp [3] https://lists.fosdem.org/listinfo/microkernel-devroom [4] https://archive.fosdem.org/2012/schedule/track/microkernel_os_devroom.html [5] https://fosdem.org/ [6] https://fosdem.org/2024/practical/conduct/

1 0