August 2022 - Devel - lists.sel4.systems

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

Proper seL4 APi/ABI design
by Eric Jacobs 17 Sep '22

17 Sep '22

Jumping off from the recent thread, I was curious if anyone had any thoughts about how to optimally design API's for seL4. I noticed we had a bit of info about what not to do (don't do long IPC, don't implement Posix, don't use messaging as synchronization, etc.) Are there any shining examples of what _to_ do with an API? Thanks, -Eric

5 11

tool to report per-component memory / resource use from system.cdl
by Sam Leffler 27 Aug '22

27 Aug '22

I'm looking for a script/tool that can break down memory by component given a system.cdl file. I've been doing this by hand (sorta) but figured I should ask before doing something more organized. -Sam

1 0

Project Sparrow / KataOS Initial Open Source Release
by June Tate-Gans (ジューン) 23 Aug '22

23 Aug '22

Hey guys! Sam and I have been hard at work at releasing our source code for the Project Sparrow work we've been working on for the last year or so, and we just managed to get our first release up at < https://github.com/AmbiML/sparrow-manifest>. So, we thought we'd announce it to the devel list! A bit of background: Sparrow is a project to build an open source low-power secure embedded platform for Ambient ML applications. Our target platform leverages RISC-V and OpenTitan, and all our contributions are licensed under the Apache-2 open source license. The Sparrow software includes a home-grown operating system named KataOS, that runs on top of seL4 and is written almost entirely in Rust. We’ve pushed some foundational pieces of KataOS to GitHub together with build glue to run seL4 CAmkES test applications on a 64-bit ARM platform (running in simulation on qemu). These are intended to show the direction we’re headed and enable anyone to start building their own systems in Rust on top of seL4. This initial tranche of code includes: frameworks (e.g. the sel4-sys crate that provides seL4 syscall apis), an alternate rootserver (needed for dynamic system-wide memory management), and the kernel modifications that enable reclaiming the memory used by the rootserver. This push does not, as yet, include the CAmkES services that support dynamic loading+running of applications–that will be published as we deem it ready for sharing until eventually all of Sparrow (software and hardware designs) will be available. While we are developing for an experimental 32-bit RISC-V platform, we intend to push code that runs on aarch64 platforms. Help is welcome to make the code base run on more platforms. In the long run, we're planning on opening up everything we can, so please watch this space! -- June Tate-Gans Software Engineer Techlead, Kata OS / AmbiML, Google

4 5

Reminder seL4 developer hangout
by Birgit Brecknell 22 Aug '22

22 Aug '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Aug 24, 7am (UTC), Topics: (open) * Sydney: Wed, Aug 24, 5pm * Central Europe: Wed, Aug 24, 9am * US Pacific Time: Aug 24, 12 midnight Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Re: QubesOS+seL4
by Gernot Heiser 11 Aug '22

11 Aug '22

[ Redirecting this inquiry to the more appropriate ailing list] On 2 Aug 2022, at 05:55, ossgroup <ossgroup(a)protonmail.com<mailto:ossgroup@protonmail.com>> wrote: I'm interested in porting QubesOS to seL4. Is there already an initiative for this? If not, would you mind pointing me in the right direction to get started? People have been playing with this on-and-off, including a honours thesis here at UNSW years ago. The closest current activity I’m aware off is our Makatea project which, in collaboration with Swiss company Neutrality, has a (presently) more limited aim of isolating servers on a private cloud: https://trustworthy.systems/projects/TS/makatea A full Qubes port would be cool but a fair bit of work. I’d definitely like to see it done, and it’s clearly a more secure approach than having Xen (and therefore a whole Linux) in your trusted computing base. Gernot

3 2

Re: QubesOS+seL4
by Demi Marie Obenour 09 Aug '22

09 Aug '22

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA512 On Mon, Aug 08, 2022 at 03:24:51PM +0200, Hugo V.C. wrote: > You are absolutely rigth Demi. Anyway, I think the point here is not to > "switch" from Xen to seL4, which is an giant task, but to start > "something", some port of QubesOS, based on seL4. Obviously, it will lack > most features, bad hardware support, etc, but I guess that as soon there's > something that can be run, the community will slowly add effort to such > project. If you remember the first versions of Linux, desktop support was > horrible... But at some point there should be people starting new > challenging stuff. I don't think we can have a QubesOS based on seL4 at > short term, but if we start now, it can be a reality in few years. I can > smell lot of interest on it... - From a Qubes OS perspective, the approach I would prefer is to first get Qubes OS working on seL4, with the control plane running in a Linux VM as it does now. This is definitely less than optimal, but it is likely the quickest way to get Qubes on seL4 working at all, and therefore the solution that is the most likely to actually be finished. Over time, more and more of the code can be replaced by native seL4 components as those components become available. For instance, the firewall is currently based on Linux, but it is a stand-alone component that already has an alternative implementation based on MirageOS. Therefore, it would be an excellent candidate for replacement with a firewall running natively on seL4. - -- Sincerely, Demi Marie Obenour (she/her/hers) Invisible Things Lab -----BEGIN PGP SIGNATURE----- iQIzBAEBCgAdFiEEdodNnxM2uiJZBxxxsoi1X/+cIsEFAmLxkk0ACgkQsoi1X/+c IsH9Kg//U+FlcwVOtDXGfjJI2WCkRrLFbIC2Mvh6k1/m+f+aGtc7jvqj0xAFXxm3 JpvIYgil2LGGsdpC3dvyTH+7xqGQUVgzcYYyJDwbdRv0gBau1T+z3xkagYvOE1E8 94aEHLmvZV6GvXZ+6LdwZjkLgOQ0qnupOSkOJtmNW86tZdXC99u6cGhszejrCSG7 GzlWPaXfP7Niy16RA9QOf4nSusXvpetQwNhzTBvn1y2XrcnvitV9MNyhp23uyWMI 4VCMaA4tYbxyZdH0whQEpjrc75S2j/ewNuuiZ3VVnkOPxid0XG8UCsLGpWtoMIak /pO/JkZ25QuHAJv5ef4JpmDD5EO410vzrs70yswEb9Xcb6Fr+RnyCLmutAS1mpan zQs31KSXVOe0R5glO3p28wpkXLO80hjYrjVITnNknWv+uujHIGE1LiF8yRFaWMNa XpAUnKcTIBSqr/VkRwphBWRHkXMxKUBFbYBwV3WaUJ0fqOsGpUD4wLpLpE6N6Lb9 hRRfdM6raJ5LXNiSuheGKCh2Hxb5WejbQCH9vSCxd0Ew6j5NZf21YY84iykT47aR dO+o2XF04s4lfeBUhd8zMTSrKA6zIyAVdbtYfThT+ONXQd15YkkLWm0f7UJBCx4X kEsgYlCHXdJIQ9mkJZI4WIGRXO39sW+NCe3bs9w/YYwuVhmQKqg= =BkM1 -----END PGP SIGNATURE-----

2 4

Reminder seL4 developer hangout
by Birgit Brecknell 08 Aug '22

08 Aug '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue Aug 9, 10pm (UTC), Topics: (open) * Sydney: Wed, Aug 10, 8am * Central Europe: Wed, Aug 10, 12 midnight * US Pacific Time: Tue, Aug 9, 3pm Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

section type mismatch on aarch64
by Sam Leffler 03 Aug '22

03 Aug '22

I'm building for aarch64 and hitting: /usr/local/google/home/sleffler/camkes-aarch64-rootserver/kernel/include/arch/arm/arch/64/mode/kernel/vspace.h:55:36: error: ‘mode_reserved_region’ causes a section type conflict with ‘avail_p_regs’ 55 | static const region_t BOOT_RODATA *mode_reserved_region = NULL; ... /usr/local/google/home/sleffler/camkes-aarch64-rootserver/build/kernel/gen_headers/plat/machine/devices_gen.h:67:37: note: ‘avail_p_regs’ was declared here 67 | static const p_region_t BOOT_RODATA avail_p_regs[] = { Looking at the commit history I see this commit: https://github.com/seL4/seL4/commit/680ce96b590295c1d49db6a2a34f77ac22e8475a followed by this commit: https://github.com/seL4/seL4/commit/8a87015a7c289f8bc2b5799d61e7c91482ad1cb2 I'm using gcc 11.2 from arm's prebuilt toolchain repo: https://developer.arm.com/tools-and-software/open-source-software/developer… Removing the clang band-aid fixes things. My source tree is "tracking" upstream but not directly based off it. Have I missed a change that resolves this? Is the 11.2 release just not being used yet (assuming it's a change in gcc? -Sam

3 4