Lions OS: secure – fast – adaptable
trustworthy.systems
trustworthy.systems
https://github.com/au-ts/lionsos
> LionsOS is aimed at embedded, IoT and cyberphysical systems and is designed to be formally verifiable, adaptable to a wide class of use cases in the target domain, while at the same time setting the benchmark for performance of microkernel-based operating systems. We aim to achieve all three goals by a highly modular yet ruthlessly performance-oriented design and strict adherence to the time-honoured KISS principle.
The term is favored by DARPA over any of its alternatives; seL4 received DARPA funding, and was adopted by DARPA projects, so it's not surprising that they'd use the associated term. It's no worse than other terms in the embedded systems world, and communicates the intended use cases to the most likely users.
Basically, if TrendMicro builds you a bunch of infrastructure to optimize the power grid, it will be described as consisting of Intelligent Electronic Devices. If Collins Aerospace builds the exact same infrastructure, it will be described as consisting of Cyber Physical Systems.
Factory equipment, vehicles, drones, power grids, medical robots, HVAC, … the list goes on.
After reading the Wikipedia page and a couple corporate pages about cyberphysical, I think it looks like it’s more about rebranding existing systems that contain interacting heterogenous elements with different RT needs, rather than introducing fundamentally new systems methodologies or technologies. It kinda reminds me of Agile, where a shift in mindset and terminology was hyped way more than any legitimate improvement in the underlying systems being built, and engineering “Agile products” became so important for some businesses.
Nah, it's a term used in academia.
https://en.wikipedia.org/wiki/A_Commentary_on_the_UNIX_Opera...
The LionsOS name is a direct callback to the John Lions Lions' Commentary on UNIX 6th Edition, an Australian computer scientist and somewhat nomadic Professor.
Trustworthy, as seen in the post link, also hails from New South Wales.
So LionOS and Genode appear to be about equal in that regard.
I was hoping Genode would get there sooner, and GNU Hurd should have gotten there years ago.
Capabilities are the computing version of circuit breakers. They make it possible to run code without having to trust it. You can't do that with Linux, Windows, MacOS, et al. MULTICS could do it, but it was deemed too complex, at the time.
Even a microkernel has three things that form part of the TCB: the part that interfaces with the even-lower-level stuff (interrupt and exception handlers, paging, memory model, etc), the interface it provides to its clients (syscalls and whatever it provides via syscalls), and the code that glues the first two parts together and implements the microkernel’s internal logic.
The latter two, in seL4, are straightforward and formally verified. The former, on x86, not so much.
AIUI, the situation on ARM is likely better.
I would not trust any system on x86.
>AIUI, the situation on ARM is likely better.
Somewhat, but still not good.
RISC-V is where it's at, when it comes to seL4.
(seL4 participates in RISC-V)
"Sculpt is an open-source general-purpose OS. It combines Genode's microkernel architecture, capability-based security, sandboxed device drivers, and virtual machines in a novel operating system for commodity PC hardware and the PinePhone. Sculpt is used as day-to-day OS by the Genode developers."
I'm hoping that Sculpt 24.04 does the job for me. If I can make sense of it enough to get Free Pascal running on it, or even just a C compiler, and "Hello, World" in a CLI, we're off to the races.
I suppose that's part of the price for high-security.
I don't have an x86 machine, and running it under a VM is too slow.
A replacement with a more serious architecture based on seL4 is in the works[0].
It’s like asking under what scenarios would you want to drive an ATV through New York. Technically possible, but that’s just not what it was made to do.
Linux is truck/SUV of computer world if I can extend your analogy. It doesn't belong to center of big city, but it is here.
Every other OS has to play catch-up. They either need a killer app or lots of funding, or else they'll be stuck in a specific niche.
Well-designed microkernels have been proven to have only a minor impact on performance, afaik. Especially if said kernel is small enough to fit in a cpu's L1 or L2 cache entirely.
With that in mind, I'd say there's few cases left where users would not want to take a minor performance hit, if that gets rid of entire classes of bugs & vulnerabilities.
Reasons this isn't the norm these days are mostly historic. But going forward, a good midpoint would be popular OS kernels like Linux split into smaller components, while providing same user-space APIs. Along the lines of how XFree86 was modularized into a set of Xorg libraries. Maybe L4Linux could be an example? (dunno how modular that is though).
On such a componentized system, components could be shared among multiple 'OS personalities'. Kinda like a multi-VM setup but finer grained with much more shared code, much reduced attack surface for individual components, while maintaining very strong isolation guarantees between components.
My posts are never "shadow deleted" they in fact sometimes get a boost from the mods when they though it just missed the mark timing-wise (i.e. interesting post, but some breaking news thing happened, and I didn't get the love).
The moderators only car about keeping the discord civil (as civil as possible), and the posts relevant/interesting for their niche.
There probably is a "club" - but not being in it doesn't get your content shadow deleted. It just wasn't interesting enough at the time to get votes.
But you can always email the mods. They're very responsive.
I mean, this post isn't really big news, it feels like it's just barely scraping by the notability/interest level required to make it on HN. Mostly, I just think the presence of some kind of cabal or conspiracy is a lot less likely than "mods are human and thus subjective and inconsistent".