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

21–30 of 151 posts

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

#21

Post by oguz-ismail »

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.

[dead]

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

#22

Post by scoot »

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.

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/

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

#23

Post by misswaterfairy »

alberth wrote: post #18

> It is written in SPARK and Ada, and is comprised of 100% free software. I thought SPARK was a paid (not free) license. Am I mistaken? Very cool project btw.

> I thought SPARK was a paid (not free) license. Am I mistaken?

Similar model to Qt: permissive licensed open source version, with a commercial 'Pro' offering.

https://en.wikipedia.org/wiki/SPARK_(programming_language)

https://alire.ada.dev/transition_from_gnat_community.html

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

#24

Post by floam »

criticalfault wrote: post #17
lifty wrote: post #10

Earlier quoted context omitted.

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?

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.

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

#25

Post by dokyun »

criticalfault wrote: post #17
lifty wrote: post #10

Earlier quoted context omitted.

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?

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.

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

#26

Post by zzo38computer »

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?

I have ideas as well, and wrote about some of them (including some partial specifications), although I do not have a name for my own, so due to this, there is not a repository or anything like that yet. Note that, there are multiple parts, and different projects will have a different set of these parts: hardware, kernel, user/application programs; my ideas involve all three (there may be other parts, and different ways to divide them, too).

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

#27

Post by criticalfault »

floam wrote: post #24
criticalfault wrote: post #17

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

Isn't this what made Linux successful?

Being able to sell it closed and not releasing the source would make closing the android ecosystem 'good old times', no?

We would only get a bunch of closed outdated company controlled binaries, but now for everything, not only drivers?

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

#30

Post by lovidico »

From their verification roadmap, it sure seems generous to refer to this as “formally verified”. They don’t prove anything important about the kernel clearly at all. Seems very disingenuous to describe it as they do since it lacks any of the merits of other formally verified kernels like seL4 and Tock.
Post reply on HN