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
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
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
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
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
[ 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
-----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-----
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
