Hacker News new | past | comments | ask | show | jobs | submit login

I don't understand why they didn't want to base it on the formally-verified, capability-based micro-kernel called seL4.

Formal verification is the difficult but necessary next step for security-intensive applications.

Also, any new kernel should only be written in a memory-safe language. Rust would be the best, since it is also safe from data races, outside of unsafe blocks.

Well... it's non-trivial to use seL4 correctly. It has all of the facilities to build something great and very little rails to ensure that you actually do. CAmkES, the component framework to help you do that, is... challenging in all the wrong ways.

The proof evidence is very hard to extend meaningfully for new platforms, and you're limited to environments which have a sufficient MMU.

We're starting with seL4 and building a whole Rust-based userland around it, and creating a whole pile of compile-time assurances along the way to make sure we're not inadvertently doing something dangerous or stupid with the rope seL4 gives you.

It's worth it for us. However, it is a colossal pain in the ass. That said, in the coming months we're likely to open source some of our progress in making it easier and more reliable to work with, integrate with, and otherwise leverage seL4 for certain use cases.

I'm super interested in the work you're doing. I spent a couple of weekends building bindings and trampolines to get Rust binaries linked into Chibi/OS and FreeRTOS and it worked really well. I've always wanted to work with seL4, so I downloaded the source and started working through the tutorials and... oh dear. There ended my experiments trying to add Rust into the mix. So if there's any way I can subscribe or otherwise keep abreast of the work you're doing, I'd love to do that.

As an aside, I wonder just how much async/await in Rust will obviate the need for small kernels in deeply embedded applications. If I can do blocking IO with my peripherals and use the async state machines to do "task" switching, well... who needs tasks and capabilities? It'd land somewhere on the "language OS" side of an embedded OS almost.

At the moment we're light on marketing materials & outreach. We've been heads down bootstrapping and working with early customers.

When we open source things in the coming weeks & months they'll all land on GitHub, https://github.com/auxoncorp, so that's probably the lowest touch way of observing what we're up to as things mature.

async/await in embedded is actually an interesting thing, that i also evaluated. I think it can't be an alternative to preemptive RTOS kernels, since the cooperative nature doesn't allow to process things within guaranteed deadlines. Therefore I think async/await might end up more as an add-on to RTOS: All time-critical things are run within independent RTOS tasks. And all the remaining and less critical stuff could potentially be run inside a single-threaded async/await scheduler.

While Rust seems to be promising here, I'm not sure whether the current async/await implementation will really allow for this. I experimented a bit with it, and found lots of issues where async/await lead to severe memory bloat (composing 3 async functions that do not a lot things requiring a 20kB task allocation). The compatibility with Futures and the requirement to move async fns to compose them before using them (which requires extra stack - which again ends up as extra heap/task memory) plays a bit against it. But these things are also worked on, so let's seee how it works out.

>If I can do blocking IO with my peripherals and use the async state machines to do "task" switching, well... who needs tasks and capabilities? It'd land somewhere on the "language OS" side of an embedded OS almost.

Waiting directly on the resource like that would require exclusive access quite often though?

Deets would be appreciated. Sounds interesting.

Rust isn't safe from race conditions. It is not a guarantee. It is free from memory errors, that is true, though.

Rust is safe from race conditions, because race conditions are memory errors.

You should read [1] to understand how Rust achieves this.

[1]: https://doc.rust-lang.org/nomicon/send-and-sync.html

Quoting some more relevant stuff from the nomicon. The linked article is short and sweet.

A data race has Undefined Behavior, and is therefore impossible to perform in Safe Rust.


However Rust does not prevent general race conditions.

This is pretty fundamentally impossible, and probably honestly undesirable. Your hardware is racy, your OS is racy, the other programs on your computer are racy, and the world this all runs in is racy. Any system that could genuinely claim to prevent all race conditions would be pretty awful to use, if not just incorrect.

Source: https://doc.rust-lang.org/nomicon/races.html

not true - you can have a program that is free of data races but still contains race conditions. Rust prevents data races.

No, Rust isn't.

Maybe you should read a bit more on its docs [1]. I quote:

However Rust does not prevent general race conditions.

[1] https://doc.rust-lang.org/nomicon/races.html

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact