Kry10 - a robust and secure OS for the IoT, based on seL4 and the Elixir stack

Chat / Discussions
, , , ,
1

I’ve been watching some videos on Kry10 - a robust and secure OS for the IoT. Because Kry10 is based on the seL4 microkernel, it has a performant, secure, verified, capability-based foundation. And, because it is also based on the Elixir stack, it has the convenience and robust behavior we know and love.

This seems like something other folks here might be interested in, so here are some links…

8 Likes
2

waiting for this for years now, anyone know when it will be available?

there are some other options for embedded Elixir right now:

*) last-millenia-OS
**) in the making

3

waiting for this for years now, anyone know when it will be available?

It appears that they are still concentrating on getting paying customers into their Beta program. However, their web site does offer a way to get on their mailing list…

There are some other options for embedded Elixir right now:

Thanks; I expanded your references a bit:

Some of these offerings are based on Linux; others are not. So, porting Linux apps may be a challenge in some cases…

-r

2 Likes
4

Having had a few days to reflect, here are a few opinionated reactions. As usual, YMMV…

The Kry10 folks say that they want Elixir web developers to become IoT engineers. This may happen, but I think the infrastructure may need some love before it’s really going to be widely attractive to these folks. Basically, they will want most of the usual Linux amenities.

Although the IoT use case has a number of peculiarities, it’s basically a “self-contained, networkable processing node”. So, it’s a close relative of cell phones, desktop and laptop computers, smart watches, tablet computers, etc. Clearly, all of these use cases could benefit from a robust and secure OS, but that isn’t all they need.

Specifically, many instances of these (including some IoT devices) need an easy way to drop in vanilla Linux programs. Ideally, these would be Rust crates, such as the upcoming version of the Fish shell.

However, if C/C++ apps are all that are available, that should be a safe and reasonably easy option. One way of accomplishing this would be to run a Linux VM on top of Kry10. The postmarketOS folks use something like this approach:

postmarketOS is based on Alpine Linux, which is so tiny (less than 10 MB in size) that development of pmOS can be done quickly on any Linux distribution. We install Alpine in multiple chroots to cross compile packages, build and flash postmarketOS, run it in a VM with QEMU or interactively port new hardware.

To be clear, I don’t really expect all of this to happen immediately, but this could (for example) allow a supercharged version of postmarketOS to be developed. So, I’m really hoping that things head in that direction (on a pony :-} ).

-r

5

It would be interesting how VM copes with limited resources nowadays, let’s say 8MB of ram and a 100MHZ CPU, because if that works well, there is a huge potential for elixir to take over IOT world, because process construct is just perfect for IO interaction.

Having said all that, another big problem is the runtime size, now if you make an elixir release, it has 20+ MB, witch is not a problem for things like rpi, however a lot of embedded devices don’t have that much rom.

1 Like
6

The typical specs on an “obsolete” cell phone (of which there are billions) are a lot more roomy than the ones you cite. Also, we can expect hardware density to keep increasing for at least a few years, so the capabilities of a “nearly minimal” IoT core can be expected to keep increasing, as well. So, my take is that hardware constraints need not be a gating item for many use cases.

-r

7

Cell phones are a different topic, I don’t think you will be able to use them anytime soon without any big improvements in this domain.

While you have access to the hardware, software is a very different issue, the way OSes like android work is the fact that the device’s “drivers” are located in a binary blob, fully developed and maintained by manufacturers. Of course you can run your software directly on top of android, however you need to root the device and tweak a lot of things to make it stable and usable.

2 Likes
8

Historically, there seem to be a couple of ways to get an open source OS running on cell phone hardware. One is to adapt Android; the other is to adapt a “generic” version of Linux (e.g., Alpine). The first approach dances around a lot of device driver issues; the second one meets them head on.

Although the postmarketOS folks have made some progress with the second approach, this effort may have been hampered by the fact that most programmers (myself included) aren’t kernel hackers. So, the pool of pmOS driver writers has been pretty limited.

However, if I may be allowed a war story, some years ago I wrote a couple of drivers for SCSI devices, using a friend’s implementation of a generic SCSI API (devscsi, which was actually adopted by SGI). Because I could write the drivers in user mode, the development progressed very quickly.

Given that Kry10’s drivers all run in userland, it wouldn’t surprise me to see similar success stories appear for cell phone drivers. However, there’s no guarantee of this and someone will have to do the heavy lifting to get a basic Kry10 system running on fairly generic cell phone hardware. So, we’ll see…

1 Like
9

A few years ago, with the help of the community I was able to fix the build, and run the VM on android arm64 (arm32 was working at the time). I also managed to run a elixir deploy with phoenix liveview on the device, strangely enough it was working out of the box, even osmon was working without any problems.

The problem appeared with the performance, connecting to liveview endpoint from another device in the network was very slow, and this can be related to a lot of things, starting from drivers and ending with their sandbox for applications.

I will definitely experiment with this more in the future, because as you mentioned, there are so many “old” mobile devices with very capable specs and peripherals already attached and they are dirt cheap at this point.

1 Like
10

Cool! By way of context, part of my motivation (like that of pmOS) is getting computing and communications capability into the hands of folks who can’t afford to buy a new cell phone. Meanwhile, the “old” ones are gathering dust…

One of the attributes I really like about Kry10 is that it boots in just a few seconds. This is close enough to “instant on” that it should be acceptable as the foundation for (say) a blind person’s “notetaker”, while having very long battery life.

11

Great project, I’ve just watched the last of these videos and I am really looking forward to tinkering with it. Didn’t know that Scenic was initially built for this project

2 Likes
12

It turns out that seL4 already supports running a VM-based Linux on ARMv7 and is pushing toward x86 support, as described in their FAQ:

How good is seL4 at supporting virtual machines?

Can I run Linux on top of seL4?

Yes, seL4 can run Linux in a virtual machine. At present the master branch supports this on ARMv7 processors (presently A15/A7 cores). For x86 there is experimental virtualisation support (requiring Intel VT-x, ETP and a HPET that supports MSI delivery). Please see the roadmap for anticipated release of a mature version.

To support virtual machines, seL4 itself runs as a hypervisor (x86 Ring-0 root mode or ARM hyp mode) and forwards virtualisation events to a virtual machine monitor (VMM) which performs the necessary emulations. The VMM runs de-privileged (x86 Ring-3 root mode or ARM supv mode).

Does seL4 support multiple virtual machines at once?

Yes, multiple VMs are supported, including heterogeneous ones.

In keeping with the spirit of seL4, it might be appropriate to use a “secure” (for some value of secure) Linux, Rust-based commands where possible, etc. That said, I’d think that seL4’s capability-based approach would already provide a fair amount of security.

Can anyone provide more information on the use of Linux and/or Linux ports of applications on Kry10, or more generally, seL4?

-r

1 Like
13

FYI, around 21 minutes into seL4 and BEAM, a match made in Erlang, Ihor Kuz discusses an approach to supporting POSIX apps without the use of either Linux or a VM.