Can we use Rust / Go / Java (GraalVM Native) or Flutter Linux to build an executable that runs on an OS with an Ironclad kernel? Or is there special treatment that makes it incompatible with "plain" Linux exe?
Ironclad – formally verified, real-time capable, Unix-like OS kernel
31–40 of 151 posts
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#32The MAC's are good: https://ironclad-os.org/manual/Mandatory-access-control-_002...
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#33Building new operating systems seems so ambitious to me. Radiant Computer ( https://radiant.computer/ ) was also recently posted. What other exciting projects like these exist?
There is always Plan9
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#34Earlier quoted context omitted.
I wonder why all of these do not use gpl2?
I wouldn’t kneecap a OS project I wish to be adopted by licensing it GPL. Look at glibc which basically can’t practically support static linking. You make any of your OS standard libraries GPL and they need to suck to use and can’t statically link your code without being forced to also be licensed GPL. That viral property some people find desirable.
WRT kneecapping, history has shown that companies will bleed the commons dry and they need to be legally strong-armed into contributing back to the free software projects they make their fortunes off of.
Virality might suit the ego, but it doesn't make for a healthy project when its primary users are parasitic.
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#35There is an NDA related company called ironclad as well. Beware the trademark/copyright terrorists. That said, I am huge fan of works like this. But in practice, the security layer that betrays all of this tends to be the firmware layer. My dream is to have something like the Framework computer use verifiably secure EFI firmware, as well as similarly verified and audited firmware for every hardware component.
That isn't how trademarks work. There can be multiple business with the same name, as long as they operate in a different field. Case in point, Apple Computer had to pay for the rights to The Beatles label Apple Music only when they entered the music industry (not that they didn't try to contest it!) Copyright is something different entirely! https://xkcd.com/386/
That make sense. I'd still be weary though, you can win in court, but the cost of getting sued isn't small. Nintendo's lawsuits come to mind.
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#36Earlier quoted context omitted.
I wonder why all of these do not use gpl2?
Rust's technical choices seem to make releasing GPL software with it cumbersome and unattractive. Also the implied goal of a lot of Rust projects is to replace GPL'ed programs with permissive ones.
Which technical choices are thinking of here? My best guess is the crates ecosystem and the oft discussed ‘dependency hell’ that pervasive package manager usage seems to engender. Is there something else I’m missing contributing to the (maybe purposeful) reluctance to push GPL code?
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#37OK can someone smarter than me educate me?
A couple weeks ago I was curious what the strictest programming language was. ChatGPT listed a couple, and it kicked off a short discussion where I began asking it about the capabilities of stricter programming languages at low levels. Funny enough at the end it mentioned that SPARK/Ada was the strictest you could get at the lowest levels, same as Ironclad.
At one point while asking it about drivers, it said "ACL2’s logic is [...] side‑effect‑free definitions with termination proofs when admitted to the logic. That is misaligned with effectful, interrupt‑driven kernel code.
I'm not an OS or kernel dev, most of my work has been in Web Dev, ML, and a little bit of embedded. How accurate is the information that was presented to me? Here is the link to the discussion: https://chatgpt.com/share/691012a7-a06c-800f-9cc9-54a7c2c8b6...
I don't know SPARK or Ada, but it just bothers me to think that we can't...I guess...prove everything about our software before we run it (yes yes, I'm familiar with halting problem shenanigans, but other than that).
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#38Interesting project. I'm curious about the limits of formal verification of worst case execution time. There are other formally verified kernels like seL4 and atmosphere, as well as layers you can stack on top to get a mostly compatible posix-ish layer like genode. You can also go out and find completely compatible kernels with enough maturity that (full) formal verification isn't a major value-add, like QNX or VxWor…
Any government can get RCE on any OS with the change in their couch. Formal verification of process isolation is REALLY important when lives depend on it. That's a huge value add! My main concern is speed and the lack of capability based security. seL4 is faster than Linux by a mile and I'm guessing that this is much slower. You can put a POSIX layer on seL4 but POSIX is inherently flawed too. MAC separates privilege…
> Any government can get RCE on any OS with the change in their couch.
Do you really believe that? That seems extremely implausible based on just simple observations like all governments using COTS OS for military/intelligence work or standard OS:es being used for critical infrastructure like power/water/finance/transportation.
If your statement was even remotely true then why is this not used in conflicts to devastating effect?
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#39Is there a technical reason it only supports x86_64, riscv64, and not arm64?
There were a bunch of ports, like arm64, but with several bugs. So the maintainer removed all but x86_64, and then another group added risc64.
From there arm64 can be tried again
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#40Interesting project. I'm curious about the limits of formal verification of worst case execution time. There are other formally verified kernels like seL4 and atmosphere, as well as layers you can stack on top to get a mostly compatible posix-ish layer like genode. You can also go out and find completely compatible kernels with enough maturity that (full) formal verification isn't a major value-add, like QNX or VxWor…
It does not have to remain at stone level, and it can get legit certifications, too. Looking forward to it. A formally verified OS is a great step towards better security.
That really depends on what formal verification means in context. I don't see any interesting specifications in the repo, just basic stuff like this MD5 spec [0] that doesn't verify whether the MD5 implementation is correct. This is one of the areas where formal verification is listed as completed/gold level.
It's common for the interesting OS proofs to take more code than the kernel itself. Take a look at the seL4 proofs [1], or those for CertiKOS as examples.
If you're actually interested in alternative OSes in memory safe languages, you might like TockOS, which is more production-ready at this point. Formal verification work of the isolation model is still ongoing, because it's difficult work.
[0] https://codeberg.org/Ironclad/Ironclad/src/branch/main/sourc...