Ironclad – formally verified, real-time capable, Unix-like OS kernel • Hacker News Board

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

#121

Post by Veserv » Mon, Nov 10, 2025, 12:42 AM UTC

irundebian wrote: post #116

Veserv wrote: post #108

Earlier quoted context omitted.

Yes you did, you said: "all governments using COTS OS for military/intelligence work" and then argued: "If your statement was even remotely true then why is this not used in conflicts to devastating effect?". You are clearly arguing that the operating systems they use, which you clearly admit are standard COTS operating systems, must be unhackable by other governments otherwise we would be seeing devastating effects…

No, he didn't. Learn to discuss properly. OP stated that any government could get RCE for any OS. And that is highly unlikely, since budget above market rates does not imply that you can easily get RCEs. The market rates are high because there is scarcity of such vulnerabilites. Governments using COTS operating systems does not imply that these systems are unackable. If the statement of OP would be true, we would jus…

We do see constant exploitation of government and critical infrastructure systems. The US telecom network is literally actively compromised right now and has been for multiple years [1]. Like wishful thinking, ignorance is also not a valid argument.

It is frankly baffling that I even need to argue that COTS operating systems are easily hacked by governments and commercial hackers. It literally happens every day and not a single one of those companies or organizations even attempts to claim that they can protect against such threats. Government actors are literally what these companies peddling substandard security use to argue "nothing we could do". It has been literal decades of people trying to make systems secure against government actors and failing time and time again with no evidence of success.

I mean, seriously, go to Defcon and say that nobody there with a team of 5 people with 3 years (~10 M$, a single tank) could breach your commercially useful and functional Linux or Windows deployment and you are putting up a 10 M$ bounty to prove it. I guarantee they will laugh at you and then you will get your shit kicked in.

[1] https://en.wikipedia.org/wiki/Salt_Typhoon

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

#122

Post by indolering » Mon, Nov 10, 2025, 12:44 AM UTC

irundebian wrote: post #115

indolering wrote: post #45

Earlier quoted context omitted.

The publicly available exploit prices put a browser zero day at $200k-$500k. That's the same cost as firing a few Javalin missiles. OS RCE runs into $1-$2 million. Much less than a cheap Russian tank. [1] The cost of internally developed exploits is probably much lower. They aren't one shot assets either, they can be used until someone plugs the hole. There are private companies selling devices to law enforcement tha…

Just because the market would buy something for X$, doesn't mean that you could buy that if you have more than X$.

Militaries have billion dollar budgets.

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

#123

Post by indolering » Mon, Nov 10, 2025, 12:53 AM UTC

SahAssar wrote: post #113

Veserv wrote: post #110

Earlier quoted context omitted.

That is inanely pedantic. The municipal government of Monowi, Nebraska probably can not buy a RCE in any OS as they only govern a single person. That is also utterly meaningless to argue as it bears no effect on the core thrust of the argument that COTS operating systems in use by military and critical infrastructure are easily and cheaply hackable by potential adversaries. They are demonstrably grossly inadequate fo…

All my questions where with the assumption of a country-level government. I asked why, if this is so cheap, common and easy we do not see it used more. Even if we said that we restrict it to for example the G20 I still don't think they can easily and cheaply "RCE any OS".

We do see it! Do you not remember the Snowden leaks?

Shit hasn't changed much. We still have monolithic kernels written in portable assembly. Linus still doesn't tag bug fixes with potential security impacts as such because he is more worried about unpatched consumer garbage (which compromise all low end phones). When your mitigation for such problems is to not make it obvious, then your OS is not safe enough in safety critical settings (which includes consumer devices).

Process isolation would downgrade the vast majority of critical Linux CVEs to availability bugs (crash a server but not compromise it).

Just because governments don't need to reach for RCE everytime doesn't mean that it is safe. Th fact that such bugs are so cheap is an indication that your safety margin is too thin.

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

#124

Post by vacuity » Mon, Nov 10, 2025, 1:07 AM UTC

indolering wrote: post #12

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 privilege…

Note: IPC performance isn't the only factor in overall OS performance. Especially for a "traditional microkernel", where programs are split up into separate processes liberally, performance degrades due to the sheer number of cross-boundary interactions. A whole system is performant if the design of the whole system, not just the design of the kernel, is aligned with performance. This is not to put down seL4; on the other hand, it continues the trend of L4 microkernels demonstrating the viability of stricter designs. But keep in mind that more time and effort is necessary to implement larger systems well.

I'm bullish on capabilities too, but I don't know much about MAC. Can you explain your last sentence?

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

#125

Post by vacuity » Mon, Nov 10, 2025, 1:08 AM UTC

snvzz wrote: post #53

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?

The most important effort is seL4[0], the fastest OS kernel out there which also happens to be the most formally verified. LionsOS[1] is its static scenario building framework, with some dynamic scenario support. Genode[2] is an independent OS construction kit that can also use the seL4 kernel. Their general purpose OS, Sculpt, just had a very interesting multi-kernel release[3]. The systems group at ETHZürich is bui…

Note: IPC performance isn't the only factor in overall OS performance. Especially for a "traditional microkernel", where programs are split up into separate processes liberally, performance degrades due to the sheer number of cross-boundary interactions. A whole system is performant if the design of the whole system, not just the design of the kernel, is aligned with performance. This is not to put down seL4; on the other hand, it continues the trend of L4 microkernels demonstrating the viability of stricter designs. But keep in mind that more time and effort is necessary to implement larger systems well.

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

#126

Post by indolering » Mon, Nov 10, 2025, 1:20 AM UTC

Veserv wrote: post #121

irundebian wrote: post #116

Earlier quoted context omitted.

No, he didn't. Learn to discuss properly. OP stated that any government could get RCE for any OS. And that is highly unlikely, since budget above market rates does not imply that you can easily get RCEs. The market rates are high because there is scarcity of such vulnerabilites. Governments using COTS operating systems does not imply that these systems are unackable. If the statement of OP would be true, we would jus…

We do see constant exploitation of government and critical infrastructure systems. The US telecom network is literally actively compromised right now and has been for multiple years [1]. Like wishful thinking, ignorance is also not a valid argument. It is frankly baffling that I even need to argue that COTS operating systems are easily hacked by governments and commercial hackers. It literally happens every day and n…

Everything thinks of Defcon et al a a gathering of elite hackers. But it's more of a fucking drinking game.

The depressing fact is that you don't need an RCE to accomplish most goals.

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

#127

Post by AlotOfReading » Mon, Nov 10, 2025, 1:22 AM UTC

tombert wrote: post #120

meling wrote: post #51

Earlier quoted context omitted.

It has been used for a while in the Secure Enclave operating system: https://en.wikipedia.org/wiki/L4_microkernel_family#:~:text=... But to my knowledge, not for the more general user facing OSes.

Yeah that's what I was getting at. I know seL4 is used in a bunch of places, but outside of a few hobbyist projects I have never heard of anyone using is at a "full" OS. It would be nearly impossible to have the support for the extremely diverse set of hardware that desktop Linux has while staying formally verified, but for something a bit more constrained like a smartphone, I think something like seL4 could work as…

I know at least one autonomous vehicle company is using it as their base OS in the autonomy stack, with efforts at extending some form of verification up to the high level code.

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

#128

Post by dathinab » Mon, Nov 10, 2025, 1:35 AM UTC

vacuity wrote: post #124

indolering wrote: post #12

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

Note: IPC performance isn't the only factor in overall OS performance. Especially for a "traditional microkernel", where programs are split up into separate processes liberally, performance degrades due to the sheer number of cross-boundary interactions. A whole system is performant if the design of the whole system, not just the design of the kernel, is aligned with performance. This is not to put down seL4; on the…

they mean "mandatory access controls (MAC)" https://en.wikipedia.org/wiki/Mandatory_access_control

through what exactly people mean with it is often vague

Like e.g. both seLinux and AppAmore are technically MAC but people tend to only mention seLinux when speaking about how cumbersome it is and treat AppAmore as something different as it's not so cumbersome.

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

#129

Post by tombert » Mon, Nov 10, 2025, 1:52 AM UTC

AlotOfReading wrote: post #127

tombert wrote: post #120

Earlier quoted context omitted.

Yeah that's what I was getting at. I know seL4 is used in a bunch of places, but outside of a few hobbyist projects I have never heard of anyone using is at a "full" OS. It would be nearly impossible to have the support for the extremely diverse set of hardware that desktop Linux has while staying formally verified, but for something a bit more constrained like a smartphone, I think something like seL4 could work as…

I know at least one autonomous vehicle company is using it as their base OS in the autonomy stack, with efforts at extending some form of verification up to the high level code.

That's cool as hell! I didn't know that but it makes me happy to see it getting a bit more love.

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

#130

Post by Veserv » Mon, Nov 10, 2025, 2:06 AM UTC

indolering wrote: post #126

Veserv wrote: post #121

Earlier quoted context omitted.

We do see constant exploitation of government and critical infrastructure systems. The US telecom network is literally actively compromised right now and has been for multiple years [1]. Like wishful thinking, ignorance is also not a valid argument. It is frankly baffling that I even need to argue that COTS operating systems are easily hacked by governments and commercial hackers. It literally happens every day and n…

Everything thinks of Defcon et al a a gathering of elite hackers. But it's more of a fucking drinking game. The depressing fact is that you don't need an RCE to accomplish most goals.

I am aware. I was making a concrete example pointing at a well known conference where average industry professionals would find the very concept of these systems being secure to be laughable.

Somehow we have ended up in this bizarro land where everybody in software knows software, especially COTS operating systems, is horribly insecure due to the endless embarrassing failures yet somehow they also doublethink these systems must be secure.