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

101–110 of 151 posts

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

#101

Post by DANmode »

jchw wrote: post #86
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…

> 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. I do, but have a slightly different take: even though COTS software is pretty much unilaterally full of bugs that will be exploitable and could be found, it is…

Knowledge that humans plug shit into computers without knowing what it is?

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

#104

Post by jchw »

DANmode wrote: post #101
jchw wrote: post #86

Earlier quoted context omitted.

> 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. I do, but have a slightly different take: even though COTS software is pretty much unilaterally full of bugs that will be exploitable and could be found, it is…

Knowledge that humans plug shit into computers without knowing what it is?

Stuxnet targeted the specific PLCs used at Iranian nuclear facilities, and had to be able to function in an airgapped environment. I reckon the logistics were far and away more complicated than finding Windows exploits, especially at that time.

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

#105

Post by SahAssar »

DANmode wrote: post #95
SahAssar wrote: post #93

Earlier quoted context omitted.

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.

Nobody in this thread has provided anything that would lead me to believe that any government can easily buy RCE on any OS. Read the quote again:

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

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

#106

Post by SahAssar »

Veserv wrote: post #100
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…

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…

> You are claiming that every major OS is unhackable by governments.

I did no such thing. I claimed that it's implausible that every government can buy RCE for every OS.

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

#107

Post by DANmode »

jchw wrote: post #104
DANmode wrote: post #101

Earlier quoted context omitted.

Knowledge that humans plug shit into computers without knowing what it is?

Stuxnet targeted the specific PLCs used at Iranian nuclear facilities, and had to be able to function in an airgapped environment. I reckon the logistics were far and away more complicated than finding Windows exploits, especially at that time.

It's probably more impressive than that. Probably targeted a range of potential PLCs.

But what's all this have to do with the ongoing conversations about pwning Windows-based networks inside major consumer utility assets?

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

#108

Post by Veserv »

SahAssar wrote: post #106
Veserv wrote: post #100

Earlier quoted context omitted.

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…

> You are claiming that every major OS is unhackable by governments. I did no such thing. I claimed that it's implausible that every government can buy RCE for every OS.

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 (or at least require more than pocket change to a potential US adversary to attack, i.e. at least more than a single tank (~10 M$), at least more than a single fighter jet (~100 M$), probably at least more than a aircraft carrier (~1 G$) before not being pocket change).

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

#109

Post by indolering »

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.

I was not being hyperbolic: a couple million dollars is very cheap for virtually any military. Both exploit broker bounties and corporate bug bounties are in that range.

What is your objection?

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

#110

Post by Veserv »

SahAssar wrote: post #105
DANmode wrote: post #95

Earlier quoted context omitted.

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

Nobody in this thread has provided anything that would lead me to believe that any government can easily buy RCE on any OS . Read the quote again: > Any government can get RCE on any OS with the change in their couch

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 for purpose.
Post reply on HN