The mascot it super cute lion too. How can a project do everything so right? I was browsing some popular python libraries and they just slapped on the first image they got out of ChatGPT. It's nice to see care in the craft.
For a short while, I ran the Eumel operating system and wrote an application in Elan. Among other interesting properties, files weren't saved, but were checkpointed by the OS. I enjoyed this exercise, although Eumel remained a very small niche.
On recent news, LionsOS, as of about a week ago (I got notified via their announcement maillist), includes a router/firewall scenario[0].
Do not miss Gernot Heiser's recent talk[1] at the seL4 Summit, where among other things he shows seL4 massively outperforming Linux in a web server scenario.
Genode is a framework that can run on many places and on higher level has its own abstractions. Lion OS is based on Microkit the framework developed by the seL4 people that will also be verified. So Lion OS/Microkit is basically the outgrowth of the original seL4 research.
Hang on, what? Genode can run on seL4 but seL4 is not part of it. Genode can also run on Linux and a bunch of other things. It has its own native kernel and it's not based on seL4 in any way, AFAIK.
It's an OS built around a verified and formally proofed L4 kernel, ie. a microkernel like QNX or MACH. The L4 is a venerable design reaching back at least 25 years, if not longer. It has seen commercial and research uses, e.g. the SIMKO3 mobile phones or the Fiasco distribution. The term "task" is specific here. Running Linux as a custom operating system is a task in microkernel lingo.
>It is not a conventional operating system, but contains composable components for creating custom operating systems that are specific to a particular task. Components are joined together using the Microkit tool.
Unfortunately, like Genode, this approach yields something that is interesting, but can't be a daily driver for me. 8(
Meanwhile, the US national security continues its downhill slide because we've chosen operating systems based on ambient authority.
I'm trying to picture in my mind a person who is a fan of Rust and somehow against an OS with a formally-verified kernel no matter the language. I'm not having much success.
Rust is supported by the [seL4 Microkit](https://docs.sel4.systems/projects/rust/), which is the core framework enabling LionsOS. LionsOS can currently run components written in Rust, and there are some WIP drivers written in Rust in the seL4 Device Development framework (judging from pull requests).
At least someone hasn't complained about it being 'unix like', always without defining what the non-unix-like OS they want would look like, or where the software to run on it would come from.
First, we could start by what UNIX authors did after they considered UNIX done, looking at Plan 9 and Inferno.
Then there are the OSes already done during the 1960 and 1970 outside Bell Labs, as possible ideas.
As from where the software would come from, if we keep recicling UNIX, we will keep getting UNIX regardless of whatever cool features the OS might offer, as most developers are lazy.
Hence why it is great that while Apple and Google OSes have some UNIX there, bare bones POSIX apps will hardly make it into the store.
… except that Rust’s compiler has been qualified for several safety critical standards, with more to come, and has several formal verification tools as well. Amazon even has placed bounties (and paid some) for proving things about the standard library.
Rust is not as immature or evolving in the ways you imply.
As all the modern ones slowly converge on similar attributes of being incomprehensibly vast codebases unreadable by any human, typically implemented in C or something closely related to it, using a similar underlying register-machine model, there is value in simply being small, simple, readable, able to do useful work, and being different. If something is also provably correct that's just the icing on the cake.
The primary focus of Lions/seL4 is security, and formal verification of it. It's a necessary project for a world where CVEs are frequently published for the Kernel and other underlying system services, in part because they're still using a 1970s OS design which didn't have internet-connected computers in mind.
The seL4 kernel uses an Object-Capability system (ironically which have also been around since the '70s) in place of Access Control Lists used in POSIX systems. The idea behind capabilities is "don't separate designation from authority" - the capability is both a designator of a resource and the authority to use it - there are no separate ACLs. Separation of designation from authority leads to confused deputies - where one process with lower privileges can trick a higher-privileged process to use the higher privileges on its behalf, which very often leads to privilege escalation vulnerabilities (ie, RCE as root).
Each process has a "cspace" (Capability Space), which holds the capabilities the process may use. When the process performs a system call, it references a capability slot from a set of tables in its own cspace where the capability is held, and the Kernel verifies that the capability is valid in order to perform the syscall. The capabilities can be revoked at any time, and importantly, they cannot be forged - only delegated.
Additionally, seL4 is a microkernel design which is intended to have a small attack surface. It provides only a small number of system calls like `Send`, `Recv`, `Yield`, and combinations of, such as `Call`, `Reply`, `ReplyRecv`. It's a generic interface where an IPC buffer is passed along with a set of delegated capabilities, but there's no specific calls such as `SYS_write` or `SYS_mmap` - these are built on top of the `Send`/`Recv` syscalls and their services are provided by other user-space daemon processes.
One of the best developments of seL4 is the "Mixed-criticality system" support, which provides capabilities for processing time - to enable some processes to have real-time support without becoming CPU hogs.
seL4 can also be seen as a hypervisor which can virtualize other kernels, and part of the Lions effort is to be able to utilize Linux drivers using isolated Linux guests.
That’s a rather luridly practical view that’s entirely out of sync with academia and basic research that provides tangible benefits much further down the line.
Yes, but basic reseach in IT is still not random, but usually has a clear goal, or at least some scope. Like indeed, focus on security? Focus on speed? Focus on reliability? Focus on energy efficency (because it is supposed to run on a tiny embedded device for long).
And the gimmick here seems to be in fact, that it is supposed to be flexibel
"is not a conventional operating system, but contains composable components for creating custom operating systems that are specific to a particular task. Components are joined together using the Microkit tool"
That begs the point: Each application will often run better on some OSes than on others. For example, high traffic websites usually aren't run on Windows 11.
no operating system does. That's application software you're thinking of. So no, it can't. But neither can windows, linux, macos, solaris, templeOS or any others
Presumably named after Associate Professor John Lions[0], of A Commentary on the UNIX Operating System[1] fame.
[0] https://en.wikipedia.org/wiki/John_Lions
[1] https://en.wikipedia.org/wiki/A_Commentary_on_the_UNIX_Opera...
The mascot it super cute lion too. How can a project do everything so right? I was browsing some popular python libraries and they just slapped on the first image they got out of ChatGPT. It's nice to see care in the craft.
It's developed by UNSW Sydney, whose mascot is a Lion. (Specifically, "Clancy the Lion"), so I am guessing it's probably that.
That's also where John Lions taught.
1 reply →
What does mascot mean
1 reply →
It is https://www.youtube.com/watch?v=W8Ka_8kHTj4&t=903s
Not presumably, but explicitly. Both in documentation and presentations by seL4 they consistently make a point to mention so.
aka the Lions book
While folks keep discussing C vs Rust, what got my attention was MicroPython and Pancake (https://trustworthy.systems/projects/pancake).
When I read about Pancake, for a very short moment I was hoping for some Elan[1] influences…
1: https://os.inf.tu-dresden.de/L4/l3elan.html
For a short while, I ran the Eumel operating system and wrote an application in Elan. Among other interesting properties, files weren't saved, but were checkpointed by the OS. I enjoyed this exercise, although Eumel remained a very small niche.
Cool, thanks for the link.
I have not heard of Pancake, seems interesting. It led me to https://cakeml.org. Looking at https://github.com/CakeML/cakeml/blob/3194e00b69ce817cf47751..., I feel quite dumb. :P
On recent news, LionsOS, as of about a week ago (I got notified via their announcement maillist), includes a router/firewall scenario[0].
Do not miss Gernot Heiser's recent talk[1] at the seL4 Summit, where among other things he shows seL4 massively outperforming Linux in a web server scenario.
0. https://lionsos.org/docs/examples/firewall/
1. https://youtu.be/wP48V34lDhk
Very cool! I’m a huge fan of Genode, another OS that runs on SeL4. Does anyone here know how they compare?
Genode is a framework that can run on many places and on higher level has its own abstractions. Lion OS is based on Microkit the framework developed by the seL4 people that will also be verified. So Lion OS/Microkit is basically the outgrowth of the original seL4 research.
> Genode, another OS that runs on SeL4.
Hang on, what? Genode can run on seL4 but seL4 is not part of it. Genode can also run on Linux and a bunch of other things. It has its own native kernel and it's not based on seL4 in any way, AFAIK.
No, you’re totally right I phrased it badly
Unequal
Finally an OS that is really an OS and not a linux distro
"but contains composable components for creating custom operating systems that are specific to a particular task"
like reviving OSfree aka 64bit OS/2
It's an OS built around a verified and formally proofed L4 kernel, ie. a microkernel like QNX or MACH. The L4 is a venerable design reaching back at least 25 years, if not longer. It has seen commercial and research uses, e.g. the SIMKO3 mobile phones or the Fiasco distribution. The term "task" is specific here. Running Linux as a custom operating system is a task in microkernel lingo.
OSFree is developed on top of L4.
Aussies were supposed to progress with Darbat.
It never happened.
>It is not a conventional operating system, but contains composable components for creating custom operating systems that are specific to a particular task. Components are joined together using the Microkit tool.
Unfortunately, like Genode, this approach yields something that is interesting, but can't be a daily driver for me. 8(
Meanwhile, the US national security continues its downhill slide because we've chosen operating systems based on ambient authority.
My first thought was to wonder whether it was a Linux offshoot.
[flagged]
I'm trying to picture in my mind a person who is a fan of Rust and somehow against an OS with a formally-verified kernel no matter the language. I'm not having much success.
I see you have not met a lot of Rust activists.
17 replies →
Rust is supported by the [seL4 Microkit](https://docs.sel4.systems/projects/rust/), which is the core framework enabling LionsOS. LionsOS can currently run components written in Rust, and there are some WIP drivers written in Rust in the seL4 Device Development framework (judging from pull requests).
At least someone hasn't complained about it being 'unix like', always without defining what the non-unix-like OS they want would look like, or where the software to run on it would come from.
First, we could start by what UNIX authors did after they considered UNIX done, looking at Plan 9 and Inferno.
Then there are the OSes already done during the 1960 and 1970 outside Bell Labs, as possible ideas.
As from where the software would come from, if we keep recicling UNIX, we will keep getting UNIX regardless of whatever cool features the OS might offer, as most developers are lazy.
Hence why it is great that while Apple and Google OSes have some UNIX there, bare bones POSIX apps will hardly make it into the store.
1 reply →
Because it is not UNIX like.
It does provide some degree of POSIX compatibility, but it does not dictate architecture.
1 reply →
Rust, an immature language with fluidly evolving specification / reference implementation, is not suitable for high assurance nor formal verification.
… except that Rust’s compiler has been qualified for several safety critical standards, with more to come, and has several formal verification tools as well. Amazon even has placed bounties (and paid some) for proving things about the standard library.
Rust is not as immature or evolving in the ways you imply.
8 replies →
[flagged]
> What is the purpose of this OS ?
What is the purpose of any OS?
As all the modern ones slowly converge on similar attributes of being incomprehensibly vast codebases unreadable by any human, typically implemented in C or something closely related to it, using a similar underlying register-machine model, there is value in simply being small, simple, readable, able to do useful work, and being different. If something is also provably correct that's just the icing on the cake.
The primary focus of Lions/seL4 is security, and formal verification of it. It's a necessary project for a world where CVEs are frequently published for the Kernel and other underlying system services, in part because they're still using a 1970s OS design which didn't have internet-connected computers in mind.
The seL4 kernel uses an Object-Capability system (ironically which have also been around since the '70s) in place of Access Control Lists used in POSIX systems. The idea behind capabilities is "don't separate designation from authority" - the capability is both a designator of a resource and the authority to use it - there are no separate ACLs. Separation of designation from authority leads to confused deputies - where one process with lower privileges can trick a higher-privileged process to use the higher privileges on its behalf, which very often leads to privilege escalation vulnerabilities (ie, RCE as root).
Each process has a "cspace" (Capability Space), which holds the capabilities the process may use. When the process performs a system call, it references a capability slot from a set of tables in its own cspace where the capability is held, and the Kernel verifies that the capability is valid in order to perform the syscall. The capabilities can be revoked at any time, and importantly, they cannot be forged - only delegated.
Additionally, seL4 is a microkernel design which is intended to have a small attack surface. It provides only a small number of system calls like `Send`, `Recv`, `Yield`, and combinations of, such as `Call`, `Reply`, `ReplyRecv`. It's a generic interface where an IPC buffer is passed along with a set of delegated capabilities, but there's no specific calls such as `SYS_write` or `SYS_mmap` - these are built on top of the `Send`/`Recv` syscalls and their services are provided by other user-space daemon processes.
One of the best developments of seL4 is the "Mixed-criticality system" support, which provides capabilities for processing time - to enable some processes to have real-time support without becoming CPU hogs.
seL4 can also be seen as a hypervisor which can virtualize other kernels, and part of the Lions effort is to be able to utilize Linux drivers using isolated Linux guests.
To learn more, the seL4 manual is a good place to start: https://sel4.systems/Info/Docs/seL4-manual-latest.pdf. There's some videos on Youtube by Gernot Heiser discussing the MCS support.
That’s a rather luridly practical view that’s entirely out of sync with academia and basic research that provides tangible benefits much further down the line.
Yes, but basic reseach in IT is still not random, but usually has a clear goal, or at least some scope. Like indeed, focus on security? Focus on speed? Focus on reliability? Focus on energy efficency (because it is supposed to run on a tiny embedded device for long).
And the gimmick here seems to be in fact, that it is supposed to be flexibel
"is not a conventional operating system, but contains composable components for creating custom operating systems that are specific to a particular task. Components are joined together using the Microkit tool"
1 reply →
One application would be safety and security critical real-time systems that also need significant amount of processing power
Those are applications, not operating systems. With occasional exceptions, you can run any application on any operating system.
That begs the point: Each application will often run better on some OSes than on others. For example, high traffic websites usually aren't run on Windows 11.
There is an example of interface in the docs: https://lionsos.org/docs/examples/kitty/
Could have been done for fun. You wouldn't understand.
no operating system does. That's application software you're thinking of. So no, it can't. But neither can windows, linux, macos, solaris, templeOS or any others
Yeah, Linus, what's the point?
Hardly a fair comparison. Linus wanted an OS that would run on his own PC and let him do his Unix homework assignments.
1 reply →
if you rearrange the letters, you get the Linos OS.
Mountain Lion is calling and wants its name back.
You mean OS X 10.7 Lion?
10.8 was Mountain Lion.
But before OS X was OS 9, and OS 9 was not the same thing as OS-9.
https://apple.fandom.com/wiki/Mac_OS_9
https://microware.com/
Before OS 9 was OS 8, which was unrelated to OS/8.
https://apple.fandom.com/wiki/Mac_OS_8
https://gunkies.org/wiki/OS/8
Names overlap. The hommage in this one is fairly clear, I think.
2 replies →