- Devel - lists.sel4.systems

Support for Sel4 Project
by simone cataldo 29 Sep '22

29 Sep '22

Good morning, We are a small test team, investigating seL4 microkernel to evaluate its use it as core component for a novel “open avionics” drone concept. Essentially, we are starting from scratch, basing ourselves on the provided tutorials such as “hello world”. We were trying to modify its source code for evaluating basic thing simple functions, basic programs and custom libraries. However, it looks like the memory allocation is static and embedded in the original project: once we increase the complexity of the program it evidently causes trouble. We have not found any documentation about how to set the memory allocation at compile time, and how to include external dependencies (i.e. static libraries). We would like to have some guideline to get us started and direction to some in-depth documentation to acquire enough knowledge to build a full project of our own. We are looking forward to hearing from you soon. Best regards, Simone CATALDO

5 5

Reminder seL4 developer hangout
by Birgit Brecknell 19 Sep '22

19 Sep '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Sep 21, 7am (UTC), Topics: (open) * Sydney: Wed, Sep 21, 5pm * Central Europe: Wed, Sep 21, 9am * US Pacific Time: Wed Sep 21, 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

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

Reminder seL4 developer hangout
by Birgit Brecknell 05 Sep '22

05 Sep '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, Sep 6, 10pm (UTC), Topics: (open) * Sydney: Wed, Sep 7, 8am * Central Europe: Wed, Sep 7, 12 midnight * US Pacific Time: Tue, Sep 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

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 (ジューン) 22 Aug '22

22 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