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

91–100 of 151 posts

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

#91

Post by ktm5j »

notepad0x90 wrote: post #35
scoot wrote: post #22

Earlier quoted context omitted.

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/

That make sense. I'd still be weary though, you can win in court, but the cost of getting sued isn't small. Nintendo's lawsuits come to mind.

Such a case would never end up in court. You can't sue someone for doing something that's perfectly legal.. well you can try, but it's going to be really hard to find a lawyer willing to waste their time (a lawyer you're going to have to pay).. and the case would ultimately get thrown out long before court.

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

#92

Post by SahAssar »

jacquesm wrote: post #79
SahAssar wrote: post #74

Earlier quoted context omitted.

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

I work in security. I know all of the above. But the parent said that "any government can by RCE on any OS", that is not at all the same as saying that it is plausible that a few of the more advanced countries probably have a few critical exploits "on ice". They also stated it as a fact, not as a possibility.

You are not arguing the same point.

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

#93

Post by SahAssar »

indolering wrote: post #76
SahAssar wrote: post #71

Earlier quoted context omitted.

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

Come on, you said:

> Any government can get RCE on any OS with the change in their couch

If you were extremely hyperbolic for effect that's fine, that's why I asked if you actually believed that, but what you are saying now is not at all arguing the same point.

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

#94

Post by cenamus »

KAMSPioneer wrote: post #63
notepad0x90 wrote: post #35

Earlier quoted context omitted.

That make sense. I'd still be weary though, you can win in court, but the cost of getting sued isn't small. Nintendo's lawsuits come to mind.

Normally I wouldn't say anything, but since we're on the topic of mixing up two different concepts: I suspect you meant to say "wary." Wary means "cautious," "weary" means "tired."

Weary and wary are also homophones, in certain dialects at least

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

#95

Post by DANmode »

SahAssar wrote: post #93
indolering wrote: post #76

Earlier quoted context omitted.

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

Come on, you said: > Any government can get RCE on any OS with the change in their couch If you were extremely hyperbolic for effect that's fine, that's why I asked if you actually believed that, but what you are saying now is not at all arguing the same point.

“Extremely hyperbolic”,

or relative?

$50k-$150k+ is a low-to-medium cost case to carry out for US law enforcement. or military.

Much like the $3 in change you could dig out of your couch or car to get a small drink or sandwich.

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

#97

Post by throwaway838112 »

bigstrat2003 wrote: post #42
heavyset_go wrote: post #34

Earlier quoted context omitted.

WRT kneecapping, history has shown that companies will bleed the commons dry and they need to be legally strong-armed into contributing back to the free software projects they make their fortunes off of. Virality might suit the ego, but it doesn't make for a healthy project when its primary users are parasitic.

> history has shown that companies will bleed the commons dry and they need to be legally strong-armed into contributing back to the free software projects they make their fortunes off of. Software is not a scarce good. Let companies use free software without contributing back as much as they wish; it doesn't affect others in the least. There is no bleeding of the commons here, because even if companies take as much…

Companies do worse than bleeding of the commons: lock down weak-licensed software and lock in users and devices. It totally reduces users ability to benefit from FOSS and reduces funding for developers.

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

#99

Post by jandrewrogers »

cedilla wrote: post #83
jacquesm wrote: post #78

Earlier quoted context omitted.

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

If I had a dollar for each time I was told that they would get me a firewall exception to get to the air gapped system... It does make it much easier to do stuff but kinda defeats the purpose.

> firewall exception to get to the air gapped system

Any system accessible with a firewall exception is not "air-gapped" by definition.

A level below that is diode networks, which are not air-gapped but provide much stronger system isolation than anything that is accessible with a "firewall exception".

Far below either of these is vanilla network isolation, which is what you seem to be talking about.

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

#100

Post by Veserv »

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…

You are claiming that every major OS is unhackable by governments. Can you point to literally any specific system that is demonstrably unhackable? Can you find literally anybody who would publicly claim their systems are unhackable by governments? Can you find literally anybody who would publicly claim that no competent team of 5 working for 3 years full-time (~1 tank worth of dollars, not even a basic company, just 1 tank) could not breach their systems? And that is just demonstrating for a single vendor, let alone your claim that it is true for everybody.

Your proof is that it would be really bad if everything were horribly insecure therefore it must not be true. Proof by wishful thinking has never been a valid argument.

In contrast, a few years ago I worked with a vulnerability broker who had literally hundreds of unsold zero-days with tens in each major commercial OS with zero-click RCEs only being a few million each. That is just one vendor in a sea of vulnerability brokers. That is the state of reality. We just live in the metaphorical equivalent of the pre-9/11 world where you can easily kill a lot of people by flying a plane into a building, but nobody has figured it out yet.

Post reply on HN