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.
santoshalper 79 days ago [-]
It's developed by UNSW Sydney, whose mascot is a Lion. (Specifically, "Clancy the Lion"), so I am guessing it's probably that.
kragen 78 days ago [-]
That's also where John Lions taught.
skavi 78 days ago [-]
John Lions is not Lions OS
is not is not
Clancy the Lion
imvetri 78 days ago [-]
What does mascot mean
saithound 78 days ago [-]
A mascot is an animal figure that represents a product or sports team. For example, the penguin named Tux is the mascot of Linux, and the mascot for the Brisbane Broncos rugby team is the horse named Buck the Bronco.
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.
Very cool! I’m a huge fan of Genode, another OS that runs on SeL4. Does anyone here know how they compare?
panick21_ 78 days ago [-]
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.
lproven 78 days ago [-]
> 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.
spencerflem 78 days ago [-]
No, you’re totally right I phrased it badly
Y_Y 78 days ago [-]
Unequal
peterisza 78 days ago [-]
Finally an OS that is really an OS and not a linux distro
fithisux 78 days ago [-]
"but contains composable components for creating custom operating systems that are specific to a particular task"
like reviving OSfree aka 64bit OS/2
Propelloni 78 days ago [-]
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.
fithisux 77 days ago [-]
OSFree is developed on top of L4.
fithisux 78 days ago [-]
Aussies were supposed to progress with Darbat.
It never happened.
mikewarot 78 days ago [-]
>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.
dctoedt 78 days ago [-]
My first thought was to wonder whether it was a Linux offshoot.
gethly 78 days ago [-]
[flagged]
aloha2436 78 days ago [-]
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.
fooker 78 days ago [-]
I see you have not met a lot of Rust activists.
aloha2436 78 days ago [-]
Certainly I don't seem to run into as many of them as I'm led to believe exists.
adastra22 78 days ago [-]
I am a “Rust activist” any day of the week. seL4 is awesome and amazing.
johnisgood 78 days ago [-]
Thoughts on Ada / SPARK? Why are you not using Ada / SPARK considering it has such a neat type system, pre- and post-conditions, formal verification, and so forth. It has built-in concurrency constructs as well and it helps you avoid deadlocks and race conditions.
adastra22 77 days ago [-]
Well, why should I? Does it bring anything else to the table? After 50 years it doesn’t have the momentum rust has, or the tooling and ecosystem.
In any case, it really isn’t comparable. It doesn’t have a borrow checker, contracts are enforced at runtime not compile time, no move semantics and no smart pointers… I find it strange actually that there is always someone bringing up “what about Ada/SPARK?” in the comments when there aren’t even comparable.
77 days ago [-]
johnisgood 77 days ago [-]
You are wrong on all counts.
It brings more to the table than Rust does. I have talked about this before, but here I go again (because your comment is full of misinformation).
SPARK contracts are compile-time verified, not runtime. The GNATprove tool statically proves absence of runtime errors, buffer overflows, arithmetic overflow, and user-defined contracts (preconditions, postconditions, invariants) at compile time with zero runtime overhead. This is formal verification, not runtime checks.
Ada has move semantics since Ada 2012 via limited types and function returns. Limited types cannot be copied, only moved. This is enforced at compile time. Build-in-place optimization eliminates unnecessary copies.
Ada has smart pointers. Ada.Containers.Indefinite_Holders provides reference semantics, GNATCOLL.Refcount provides explicit reference counting, and controlled types (Ada.Finalization.Controlled) give you RAII-style resource management with deterministic finalization, effectively custom smart pointers. Search for "Ada smart pointers".
Ownership/borrowing in SPARK: While not called a "borrow checker," SPARK's ownership model (Ada 202x, SPARK RM 3.10) provides compile-time verification of pointer safety, including ownership transfer, borrowing (observed/borrowed modes), and prevents use-after-free and aliasing violations. The verification is actually more comprehensive than Rust because it proves full functional correctness, not just memory safety.
Certification: Ada/SPARK is DO-178C certified for avionics, used in safety-critical systems (Airbus, Boeing, spacecraft), and has Common Criteria EAL certification. Rust has no comparable certification history for high-assurance systems.
The tooling argument is partially valid. Rust has better modern tooling (although Ada now has a proper package manager) and a more lively ecosystem. But claiming Ada lacks move semantics, or smart pointers is factually incorrect, and SPARK proves what Rust's borrow checker only approximates, and does so with mathematical proof, not heuristics.
Why should you care? You answer that, but I think you may be right, you are just a Rust activist.
What I find strange is the confidence with which you make verifiably and demonstrably incorrect statements about Ada, a language you clearly have not studied.
adastra22 77 days ago [-]
You are right. I just plain don't care. Maybe I am misinformed. Maybe you are misunderstanding my requirements. Either way, it doesn't matter.
You seem to be missing the point - there is an entire ecosystem of things built in Rust, a community of developers using it in related fields to where I am working, and a vast store of experience and knowledge to draw upon.
Outside of aviation or defense, does Ada have that? No, it does not.
That is why no one uses it.
PS: This subthread started when someone made an assumption that Rust activists would pounce on this for not being written in Rust. I chimed in to say that, as a "rust activist" seL4 is actually pretty cool and that's fine. Then you butted in preach the Ada gospel. Not a good look.
johnisgood 77 days ago [-]
> Outside of aviation or defense, does Ada have that? No, it does not.
> That is why no one uses it.
Both of these statements are false as well.
(I only made this response because you keep spreading misinformation about a language you know nothing about, self-admittedly, and demonstrably. Not a good look. Neither is your response to you being corrected. If you do not care, at least stop spreading bullshit so confidently about a language you do not know at all.)
ksec 77 days ago [-]
Just want to say Thank You. May be thank you "again" because I remember I said this previously as well.
Every time I mention Ada on HN it is always the Rust people that claims it is irrelevant, especially when it is them who started only Rust can do X.
The unwritten rule of HN: You do not criticise The Rusted Holy Grail or the Riscy Silver Bullet.
77 days ago [-]
whytevuhuni 77 days ago [-]
I'm a Rust fanatic but probably not an activist. I am curious about Ada / SPARK though.
From what I've seen, taking on SPARK means taking on full verification, close to what seL4 is doing. Doesn't that make it extremely difficult to use for larger projects? My understanding is that seL4 is an absolutely heroic effort.
GhosT078 77 days ago [-]
Ada is very scalable, suitable for everything from blinking LEDs on an AVR microcontroller board to controlling interplanetary spacecraft. Similarly, SPARK can be used incrementally, proving lower level or critical parts first.
whytevuhuni 77 days ago [-]
How does this SPARK/non-SPARK mix compare to Rust's safe/unsafe mix though, in terms of both safety and pragmatism for larger non-interplanetary software? Like, for creating a CLI tool, a GUI application, a game, a web server?
pppppiiiiiuuuuu 78 days ago [-]
It's funny how people always allude to fanatical Rust developers in the most tangential threads, but they never actually turn up and demand we rewrite the entire Kernel in Rust or whatever terrible takes they're alleged to have.
Gosh... and people on HN tell us that they have yet to meet a Rust fanatic. Just look around the GitHub Issues I linked.
---
BTW I stumbled upon https://github.com/r9os/r9 as well. Reading the source code, it is mainly unsafe blocks and assembly. :| Who would have thought?
aduty 78 days ago [-]
Love that discussion on the Haiku board.
lovidico 78 days ago [-]
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).
kjs3 78 days ago [-]
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.
pjmlp 78 days ago [-]
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.
kjs3 72 days ago [-]
Yeah, once again you (you, pjmlp specifically) have missed the point. But thanks for explaining the obvious (once again).
snvzz 78 days ago [-]
Because it is not UNIX like.
It does provide some degree of POSIX compatibility, but it does not dictate architecture.
kjs3 72 days ago [-]
Yes, I think most of us are clear that seL4 isn't Unix. But people continue to complain that anything with a Posix layer is Unix-like, and therefore somehow 'bad'. My point was that virtually everyone who complains about this never, ever explains what would have been better to implement, just that it should have been different.
snvzz 78 days ago [-]
Rust, an immature language with fluidly evolving specification / reference implementation, is not suitable for high assurance nor formal verification.
steveklabnik 78 days ago [-]
… 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.
johnisgood 78 days ago [-]
Why would Rust need formal verification tools like https://github.com/rust-lang/miri if the programming language is so safe that it prevents them[1]?!
[1] Undefined Behaviors.
steveklabnik 78 days ago [-]
Miri is not really a formal verification tool. It is more of a runtime sanitizer.
And it's because Rust's "no undefined behavior" is for safe Rust. Miri is used dynamically at runtime to catch undefined behavior in the unsafe superset.
Finally, Rust's safety guarantees relate to memory safety only. There's a lot more properties you'd want to prove about programs, some safety related in a broader sense, some totally unrelated to safety concerns.
johnisgood 78 days ago [-]
Is it possible to find UB in "unsafe" at compile time?
steveklabnik 77 days ago [-]
By using some proof tools, you can find some of it.
It is technically impossible to find 100% of it at compile time because some of the finer details about what is UB are not nailed down 100% yet. But those are generally pretty fine corner cases, and one of the goals of those definitions is to not invalidate code as written.
Formal verification is very hard.
fooker 78 days ago [-]
> Amazon even has placed bounties (and paid some) for proving things about the standard library.
That announcement was a year ago, I haven’t kept up with the repo.
hulitu 78 days ago [-]
[flagged]
lproven 78 days ago [-]
> 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.
sparkie 76 days ago [-]
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.
lukan 78 days ago [-]
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"
panick21_ 77 days ago [-]
Its just the fastest, safest and most reliable possible operating system, giving you more formal guarantees then literally anything else ... why don't you just read more then just 1 sentence and actually spend 15min learning about the system.
oytis 78 days ago [-]
One application would be safety and security critical real-time systems that also need significant amount of processing power
kragen 78 days ago [-]
Those are applications, not operating systems. With occasional exceptions, you can run any application on any operating system.
mmooss 78 days ago [-]
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.
Could have been done for fun. You wouldn't understand.
vrighter 78 days ago [-]
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
fortyseven 78 days ago [-]
Yeah, Linus, what's the point?
lmm 78 days ago [-]
Hardly a fair comparison. Linus wanted an OS that would run on his own PC and let him do his Unix homework assignments.
johnisgood 78 days ago [-]
What makes the comparison not fair? We do not know the author's story!
fifticon 78 days ago [-]
if you rearrange the letters, you get the Linos OS.
amelius 78 days ago [-]
Mountain Lion is calling and wants its name back.
CursedSilicon 78 days ago [-]
You mean OS X 10.7 Lion?
lproven 78 days ago [-]
10.8 was Mountain Lion.
But before OS X was OS 9, and OS 9 was not the same thing as OS-9.
[0] https://en.wikipedia.org/wiki/John_Lions
[1] https://en.wikipedia.org/wiki/A_Commentary_on_the_UNIX_Opera...
Mascot is, unrelatedly, also a suburb of Sydney.
1: https://os.inf.tu-dresden.de/L4/l3elan.html
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
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.
like reviving OSfree aka 64bit OS/2
It never happened.
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.
In any case, it really isn’t comparable. It doesn’t have a borrow checker, contracts are enforced at runtime not compile time, no move semantics and no smart pointers… I find it strange actually that there is always someone bringing up “what about Ada/SPARK?” in the comments when there aren’t even comparable.
It brings more to the table than Rust does. I have talked about this before, but here I go again (because your comment is full of misinformation).
SPARK contracts are compile-time verified, not runtime. The GNATprove tool statically proves absence of runtime errors, buffer overflows, arithmetic overflow, and user-defined contracts (preconditions, postconditions, invariants) at compile time with zero runtime overhead. This is formal verification, not runtime checks.
Ada has move semantics since Ada 2012 via limited types and function returns. Limited types cannot be copied, only moved. This is enforced at compile time. Build-in-place optimization eliminates unnecessary copies.
Ada has smart pointers. Ada.Containers.Indefinite_Holders provides reference semantics, GNATCOLL.Refcount provides explicit reference counting, and controlled types (Ada.Finalization.Controlled) give you RAII-style resource management with deterministic finalization, effectively custom smart pointers. Search for "Ada smart pointers".
Ownership/borrowing in SPARK: While not called a "borrow checker," SPARK's ownership model (Ada 202x, SPARK RM 3.10) provides compile-time verification of pointer safety, including ownership transfer, borrowing (observed/borrowed modes), and prevents use-after-free and aliasing violations. The verification is actually more comprehensive than Rust because it proves full functional correctness, not just memory safety.
Certification: Ada/SPARK is DO-178C certified for avionics, used in safety-critical systems (Airbus, Boeing, spacecraft), and has Common Criteria EAL certification. Rust has no comparable certification history for high-assurance systems.
The tooling argument is partially valid. Rust has better modern tooling (although Ada now has a proper package manager) and a more lively ecosystem. But claiming Ada lacks move semantics, or smart pointers is factually incorrect, and SPARK proves what Rust's borrow checker only approximates, and does so with mathematical proof, not heuristics.
Why should you care? You answer that, but I think you may be right, you are just a Rust activist.
What I find strange is the confidence with which you make verifiably and demonstrably incorrect statements about Ada, a language you clearly have not studied.
You seem to be missing the point - there is an entire ecosystem of things built in Rust, a community of developers using it in related fields to where I am working, and a vast store of experience and knowledge to draw upon.
Outside of aviation or defense, does Ada have that? No, it does not.
That is why no one uses it.
PS: This subthread started when someone made an assumption that Rust activists would pounce on this for not being written in Rust. I chimed in to say that, as a "rust activist" seL4 is actually pretty cool and that's fine. Then you butted in preach the Ada gospel. Not a good look.
> That is why no one uses it.
Both of these statements are false as well.
(I only made this response because you keep spreading misinformation about a language you know nothing about, self-admittedly, and demonstrably. Not a good look. Neither is your response to you being corrected. If you do not care, at least stop spreading bullshit so confidently about a language you do not know at all.)
Every time I mention Ada on HN it is always the Rust people that claims it is irrelevant, especially when it is them who started only Rust can do X.
The unwritten rule of HN: You do not criticise The Rusted Holy Grail or the Riscy Silver Bullet.
From what I've seen, taking on SPARK means taking on full verification, close to what seL4 is doing. Doesn't that make it extremely difficult to use for larger projects? My understanding is that seL4 is an absolutely heroic effort.
https://github.com/seL4/seL4/issues/487
Check out https://github.com/ansuz/RIIR/issues/ for more.
Gosh... and people on HN tell us that they have yet to meet a Rust fanatic. Just look around the GitHub Issues I linked.
---
BTW I stumbled upon https://github.com/r9os/r9 as well. Reading the source code, it is mainly unsafe blocks and assembly. :| Who would have thought?
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.
It does provide some degree of POSIX compatibility, but it does not dictate architecture.
Rust is not as immature or evolving in the ways you imply.
[1] Undefined Behaviors.
And it's because Rust's "no undefined behavior" is for safe Rust. Miri is used dynamically at runtime to catch undefined behavior in the unsafe superset.
Finally, Rust's safety guarantees relate to memory safety only. There's a lot more properties you'd want to prove about programs, some safety related in a broader sense, some totally unrelated to safety concerns.
It is technically impossible to find 100% of it at compile time because some of the finer details about what is UB are not nailed down 100% yet. But those are generally pretty fine corner cases, and one of the goals of those definitions is to not invalidate code as written.
Formal verification is very hard.
Can you provide some links? Thanks.
Are these reasonably current?
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 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.
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"
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.
Ergo it would be 10.7 Lion, no?