Yay! Take that, Minix and GNU Hurd! \o/
Ironclad – formally verified, real-time capable, Unix-like OS kernel
61–70 of 151 posts
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#62Earlier quoted context omitted.
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 devasta…
In djb's course at UIUC, I recal he said that students were required to find a vulnerability as part of the course requirements.
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#63Earlier quoted context omitted.
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.
Normally I wouldn't say anything, but since we're on the topic of mixing up two different concepts:
I suspect you meant to say "wary." Wary means "cautious," "weary" means "tired."
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#64Earlier quoted context omitted.
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 p…
There is none in [0]. :P
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#65SPARK’s “ask about pricing” stickers indicate this is “free” software that’s a different kind of free.
That guy in Nebraska needs to buy food and shelter.
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#66Yay! Take that, Minix and GNU Hurd! \o/
Ironclad isn't a microkernel, is it? At least the device drivers, file system and network stack seem to run in kernel space. I didn't find any strong architectural hints pointing to microkernel design in the implementation so far.
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#67Can 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 has a POSIX API, so yes, in principle it should be possible. There is an OS on top of Ironclad (https://github.com/Ironclad-Project/Gloire) which uses GNU tools.
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#68Here is the deepwiki documentation: https://deepwiki.com/Ironclad-Project/Ironclad
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#69Here is the deepwiki documentation: https://deepwiki.com/Ironclad-Project/Ironclad
Is that an AI-generated page pretending to be a wiki?
Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel
#70Here is the deepwiki documentation: https://deepwiki.com/Ironclad-Project/Ironclad
Is that an AI-generated page pretending to be a wiki?
Don't tell me you don't know this service. It's extremely useful to get to know the code and architecture of a project. You can even ask questions about the code and get the relevant references to the corresponding sections in the source files.