Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Ironclad – formally verified, real-time capable, Unix-like OS kernel

ironclad-os.org

Post reply on HN
Print view View original

1–10 of 151 posts

Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel

#4

Post by aloisdg »

ivanjermakov wrote: post #3
joshuakelly wrote: post #2

Building new operating systems seems so ambitious to me. Radiant Computer ( https://radiant.computer/ ) was also recently posted. What other exciting projects like these exist?

https://serenityos.org/

[flagged]

Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel

#6

Post by attila-lendvai »

joshuakelly wrote: post #2

Building new operating systems seems so ambitious to me. Radiant Computer ( https://radiant.computer/ ) was also recently posted. What other exciting projects like these exist?

it seems to be little more than a mission statement... no?

Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel

#7

Post by notepad0x90 »

There 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.

Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel

#8

Post by AlotOfReading »

Interesting 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 VxWorks.

I'm not aware of much that combines WCET + formal verification + POSIX compatibility though. The verification page here is mostly at stone level, which from my understanding of SPARK terminology just means it passes validation, but might have runtime errors where most of Ada's WCET nondeterminism comes from. I'm skeptical that this is actually production usable for the hard real-time use cases all over their documentation at the current stage, but nothing on the website gives any clue as to the actual maturity short of reading the code myself.

Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel

#9

Post by sharts »

ivanjermakov wrote: post #3
joshuakelly wrote: post #2

Building new operating systems seems so ambitious to me. Radiant Computer ( https://radiant.computer/ ) was also recently posted. What other exciting projects like these exist?

https://serenityos.org/

This looks perfect. Just wonder how the hardware /software support goes

Re: Ironclad – formally verified, real-time capable, Unix-like OS kernel

#10

Post by lifty »

joshuakelly wrote: post #2

Building new operating systems seems so ambitious to me. Radiant Computer ( https://radiant.computer/ ) was also recently posted. What other exciting projects like these exist?

https://asterinas.github.io/ (Linux compatible Kernel) and https://redox-os.org/ are two promising ones.
Post reply on HN