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

11–20 of 151 posts

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

#11

Post by F3nd0 »

notepad0x90 wrote: post #7

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.

You might want to check out MNT Research if you haven’t yet. They make repairable laptops, too, but they also release their work as free software and open hardware.

https://mnt.re/

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

#12

Post by indolering »

AlotOfReading wrote: post #8

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 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 privileges from code and is too clunky to use in practice (see seLinux).

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

#13

Post by indolering »

notepad0x90 wrote: post #7

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.

You need a different kernel for firmware verification. But it should be regulated at this point.

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

#15

Post by johnisgood »

AlotOfReading wrote: post #8

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

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

#17

Post by criticalfault »

lifty wrote: post #10
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.

I wonder why all of these do not use gpl2?

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

#19

Post by chrsw »

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?

Not new, but alternative https://www.haiku-os.org/

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

#20

Post by notepad0x90 »

F3nd0 wrote: post #11
notepad0x90 wrote: post #7

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.

You might want to check out MNT Research if you haven’t yet. They make repairable laptops, too, but they also release their work as free software and open hardware. https://mnt.re/

The MNT is too small for my usage, but it's a great effort. I think their goal is to make open hardware right now, not necessarily a verifiable one.
Post reply on HN