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

71–80 of 151 posts

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

#71

Post by SahAssar »

indolering wrote: post #45
SahAssar wrote: post #38

Earlier quoted context omitted.

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

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…

> [1]: https://opzero.ru/en/prices/

Those are the prices that they are buying for, they do not indicate at all that these are common or how large the market is for RCE on any OS.

> [2]: https://arstechnica.com/gadgets/2025/10/leaker-reveals-which...

Those are (mostly) not RCE, and are for consumer devices configured in a default way.

---

The parent stated that "Any government can get RCE on any OS with the change in their couch."

That implies that Kiribati currently could easily buy RCE on for example hardened Linux or OpenBSD running the most sensitive infra in the world. I just don't buy that, since if it was true any current conflict would look much different.

Of course there are security holes and major fuckups do happen, but not at the scale the parent implied.

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

#72

Post by SahAssar »

numpy-thagoras wrote: post #52
SahAssar wrote: post #38

Earlier quoted context omitted.

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

Yes, I believe that. > If your statement was even remotely true then why is this not used in conflicts to devastating effect? It has been, it continues to be. Where have you been?

It really hasn't to the scale that you imply. Why hasn't ukraine and russia both used this to completely shut down each others infrastructure? Why isn't russia just hacking all the ukrainian COTS drones? Why hasn't anyone hacked a nuclear power plant?

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

#73

Post by virtue3 »

exe34 wrote: post #59
numpy-thagoras wrote: post #52

Earlier quoted context omitted.

Yes, I believe that. > If your statement was even remotely true then why is this not used in conflicts to devastating effect? It has been, it continues to be. Where have you been?

Do you have any resources that go deeper into this? It's a fascinating frontier for war!

USA was providing Ukrainian operatives Russian officer locations via soldier's using their cellphones

https://oe.tradoc.army.mil/product/smart-phones-playing-prom...

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

#74

Post by SahAssar »

emmelaich wrote: post #62
SahAssar wrote: post #38

Earlier quoted context omitted.

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

Finding a vulnerability is not at all the same as "RCE on any OS". Vulnerabilities are common, the ones that have the impact implied are not.

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

#75

Post by mjlee »

SahAssar wrote: post #38
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…

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

> why is this not used in conflicts to devastating effect?

The systems with devastating impact are air-gapped. They're designed, audited, validated and then never touched again. Ports are disabled by cutting the traces on the motherboard and adding tamper protection to the case, which is in a secure facility protected by vetted people with guns, who are in a security facility protected by different vetted people with guns.

No system is perfect, but the time and effort is better spent on the generic case that the military understands well.

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

#76

Post by indolering »

SahAssar wrote: post #71
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…

> [1]: https://opzero.ru/en/prices/ Those are the prices that they are buying for, they do not indicate at all that these are common or how large the market is for RCE on any OS . > [2]: https://arstechnica.com/gadgets/2025/10/leaker-reveals-which... Those are (mostly) not RCE, and are for consumer devices configured in a default way. --- The parent stated that " Any government can get RCE on any OS with the change i…

These prices are consistent (actually more costly) than public bounties by (now defunct) western based exploit brokers and manufacturer bounties.

> Those are (mostly) not RCE, and are for consumer devices configured in a default way.

I'm more worried about activists and journalists in developing counties without the financial means to afford flagship phones. But even Google can't manage to keep out a pedestrian mid sized security outfit selling to the cops and the FBI.

When activists lobbying for a fucking sugar tax in Mexico get hacked, then the bar is too fucking low.

Let's not talk about the nightmare that is old networking equipment or IoT devices.

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

#77

Post by indolering »

SahAssar wrote: post #72
numpy-thagoras wrote: post #52

Earlier quoted context omitted.

Yes, I believe that. > If your statement was even remotely true then why is this not used in conflicts to devastating effect? It has been, it continues to be. Where have you been?

It really hasn't to the scale that you imply. Why hasn't ukraine and russia both used this to completely shut down each others infrastructure? Why isn't russia just hacking all the ukrainian COTS drones? Why hasn't anyone hacked a nuclear power plant?

There is power in restricting access and air gapping helps a lot. A drone (for example) can fall back to basic cryptography to limit access.

Air gapping is a baseline requirement in most safety critical systems. Nuclear power plants in particular have lots of redundant layers of safety. AFAIK Russia hasn't physically tried to cause a meltdown, presumably due to the political blow back (although they have attacked Chernobyl's sarcophagus). I assume this limits their digital espionage attacks too.

We do get glimpses of the use of such malware, like when Saudi Arabia hacked Jeff Bezos' phone. But we don't hear about most of it because there is a benefit to keeping a hack secret, so as to keep access.

Finally, it's usually cheaper to social engineer someone into loading a PowerPoint presentation and doing a local privilege escalation. They burn those for things as petty as getting embarrassing political information.

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

#78

Post by jacquesm »

mjlee wrote: post #75
SahAssar wrote: post #38

Earlier quoted context omitted.

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

> why is this not used in conflicts to devastating effect? The systems with devastating impact are air-gapped. They're designed, audited, validated and then never touched again. Ports are disabled by cutting the traces on the motherboard and adding tamper protection to the case, which is in a secure facility protected by vetted people with guns, who are in a security facility protected by different vetted people with…

> The systems with devastating impact are air-gapped.

You wish. More often than not the people building these think they are very clever by using their bullet proof fire walls rather than a physical disconnect. Or SLIP over a serial port because for some reason serial ports are fine.

I've seen this kind of crap in practice in systems that should be airgapped, that they said were airgapped but that in fact were not airgapped.

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

#79

Post by jacquesm »

SahAssar wrote: post #74
emmelaich wrote: post #62

Earlier quoted context omitted.

In djb's course at UIUC, I recal he said that students were required to find a vulnerability as part of the course requirements.

Finding a vulnerability is not at all the same as "RCE on any OS". Vulnerabilities are common, the ones that have the impact implied are not.

Let me help a bit by trying to explain the situation. If you produce something that is a million lines of code you will most likely have at least a few hundred to a few thousand bugs in there. Some of those cause crashes, some of them cause hangs, and a small percentage will cause you to increase your privileges. Combine enough of those and sooner or later you end up with RCE. The problem is that you as a defender don't necessarily have the same budget to audit the code and to close it all down to the degree that an attacker has.

You need to do an absolutely perfect job in always spotting those RCE capable issues before an attacker does. And given the numbers involved this becomes a game of statistics: if there are 200 ways to get RCE on OS 'X' then you need to find and fix all of them before attackers do. Meanwhile, your system isn't a million lines but a multitude of that, there are your applications to consider (usually of a lesser quality than the OS), the risk of a purposeful insertion of a backdoor and so on.

So I don't think it is unreasonable to presume that any OS that is out there most likely has at least a couple of these that are kept 'on ice'.

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

#80

Post by lossolo »

SahAssar wrote: post #71
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…

> [1]: https://opzero.ru/en/prices/ Those are the prices that they are buying for, they do not indicate at all that these are common or how large the market is for RCE on any OS . > [2]: https://arstechnica.com/gadgets/2025/10/leaker-reveals-which... Those are (mostly) not RCE, and are for consumer devices configured in a default way. --- The parent stated that " Any government can get RCE on any OS with the change i…

This shouldn't be downvoted because it's stating facts. RCEs for critical infrastructure/OSes are very rare, they don't just grow on trees. I agree that OP exaggerated by saying that any government can buy whatever RCE they want and get access to any system they want, like buying candy in a candy shop. That's not reality.
Post reply on HN