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

111–120 of 151 posts

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

#111

Post by jacquesm »

jandrewrogers wrote: post #99
cedilla wrote: post #83

Earlier quoted context omitted.

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.

Diode networks can be - and have been - used to exfiltrate data though.

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

#112

Post by jandrewrogers »

jacquesm wrote: post #111
jandrewrogers wrote: post #99

Earlier quoted context omitted.

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

Diode networks can be - and have been - used to exfiltrate data though.

Definitely! I've worked on the design of these types of systems, there is more subtlety to the security models than people assume. Some of the designs in the wild have what I would consider to be notable weaknesses.

The most interesting subset of these systems are high-assurance bi-directional data paths between independent peers that are quasi-realtime. Both parties are simultaneously worried about infiltration and exfiltration. While obviously a misnomer, many people still call them diodes...

The entire domain is fascinating and less developed than you would think.

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

#113

Post by SahAssar »

Veserv wrote: post #110
SahAssar wrote: post #105

Earlier quoted context omitted.

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

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

#114

Post by jchw »

DANmode wrote: post #107
jchw wrote: post #104

Earlier quoted context omitted.

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?

I responded to this thread of thought:

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

Mainly to agree with it. I believe it is still likely true.

Any resemblance to other discussion further up or down is unintentional.

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

#115

Post by irundebian »

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…

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

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

#116

Post by irundebian »

Veserv wrote: post #108
SahAssar wrote: post #106

Earlier quoted context omitted.

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

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 just see constant exploitation of RCE zero days, or at the least the impact of that. But that is not the case.

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

#117

Post by notepad0x90 »

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

I think wary would have been a better word, but I really did mean "weary", as in I would find the ordeal tiresome or bothersome? I wouldn't disagree if you said that's bad grammar still.

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

#118

Post by notepad0x90 »

ktm5j wrote: post #91
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.

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.

Check this out: https://www.suedbynintendo.com/

If a gaming company can sue a local supermarket over trademark, I don't know what to say.

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

#119

Post by irundebian »

indolering wrote: post #77
SahAssar wrote: post #72

Earlier quoted context omitted.

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

I doubt that most critical systems are air gapped. Even if there are, most part of Russians economy is not, but is still using IT based on COTS systems. Why wouldn't the Ukraine DoS or compromise the whole non air-gapped IT infrastructure of Russia to hit the economy if they could have easy access to RCE just because they are a government?

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

#120

Post by tombert »

meling wrote: post #51
tombert wrote: post #49

I haven’t fully given up on the hope that a fully verified kernel eventually catches on. It would be basically impossible to verify all of Linux at this point, but I could see seL4 eventually getting traction in something like the smartphone market. A guy can dream, at least.

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 a base and the manufacturer could write their own drivers for whatever hardware is needed.

I mean, how cool would it be if every single part of the stack that is even possible to verify was fully verified. I know about the halting problem, I know there are things that would be basically impossible to verify fully, but I still think it would be cool to live in a world where software engineers actually had a little assurance what they were doing actually worked before unleashing into the world.

Post reply on HN