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

141–150 of 151 posts

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

#141

Post by jacquesm »

jandrewrogers wrote: post #112
jacquesm wrote: post #111

Earlier quoted context omitted.

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…

And even if you do get it right, there is always that one guy that takes a USB stick and plugs it into your carefully air-gapped systems. And cell modems are everywhere now, and so small even an expert could still overlook one, especially if it is dormant most of the time.

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

#142

Post by DANmode »

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

“I don’t get told, it isn’t happening/possible.”

Hopefully this helps as succinctly as possible. Genuinely.

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

#143

Post by vacuity »

snvzz wrote: post #131
vacuity wrote: post #125

Earlier quoted context omitted.

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…

Do not miss the latest seL4 summit's state of seL4 talk by Gernot Heiser[0], which besides providing an update on the work done this year, goes into performance[1]. This is real world throughput and latency seL4 is crushing Linux on, not some synthetic IPC benchmark. 0. https://www.youtube.com/watch?v=wP48V34lDhk 1. https://youtu.be/wP48V34lDhk?t=1199

I think I've got the gist now. Although I think Gernot Heiser doesn't consider the following to be ideal, I think it's fair to say that true claims have undergone some sensationalization. I don't think people generally lie when they say their product has achieved some impressive performance, but those results exist in the context they are taken under. In the embedded roles LionsOS is being targeted for, I have no doubt that they represent a real improvement over existing Linux systems, and probably any Linux system short of a magical one. However, in a general-purpose OS (which is what I focus on), which is the same as saying that many distinct user bases are simultaneously involved, the kernel is far from being the only load-bearing component. Also note that the functionality compared is not 1:1, nor is Linux the final contender of monolithic systems.

Something I want to explore, and which has some viability in the LionsOS model too, is that a general-purpose system may still liberally cut out unused functionality if highly modular and easily configurable. Like Legos.

In conclusion, props to the people at Trustworthy Systems as always, but it's safe to say that the OS field is still far from settled. My best compliment to seL4 is that it has raised the bar and simultaneously paved the way for future generations of advances. It's a seminal work that was desperately needed.

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

#144

Post by cxr »

Rochus wrote: post #85
debugnik wrote: post #82

Earlier quoted context omitted.

Okay but that's not a wiki. Wiki implies pages can be collaboratively edited and linked. Otherwise it's not a wiki, it's just a website. The only collaboration here is to bait people into becoming maintainers and fix the hallucinated content. More than one maintainer has shown frustration at that site making up wrong documentation already.

It's just the name of the service, as imagined by its creator, Cognition Labs; it's called a "wiki" because it creates wiki-style documentation similar to Wikipedia's format. There are always people who complain about everything. I'm successfully using the service since a few month and even applied it to my own compiler projects, and I think it's pretty good; of course there are errors, but from my experience far les…

It's not "just the name of the service". The Deepwiki people are either morons or assholes or both. Complaining that someone is debasing the definition of the word "wiki" by applying it to something that isn't a wiki is not a trifling complaint.

Describing a topic-constrained encyclopedia as a "wiki" on the basis that Wikipedia is a thing is like calling coffee "ice" because iced coffee exists.

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

#145

Post by shadowgovt »

cxr wrote: post #144
Rochus wrote: post #85

Earlier quoted context omitted.

It's just the name of the service, as imagined by its creator, Cognition Labs; it's called a "wiki" because it creates wiki-style documentation similar to Wikipedia's format. There are always people who complain about everything. I'm successfully using the service since a few month and even applied it to my own compiler projects, and I think it's pretty good; of course there are errors, but from my experience far les…

It's not "just the name of the service". The Deepwiki people are either morons or assholes or both. Complaining that someone is debasing the definition of the word "wiki" by applying it to something that isn't a wiki is not a trifling complaint. Describing a topic-constrained encyclopedia as a "wiki" on the basis that Wikipedia is a thing is like calling coffee "ice" because iced coffee exists.

Or a quickly-editable website a "wiki" because it's the Hawaiian word for "quick."

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

#146

Post by shadowgovt »

debugnik wrote: post #82
Rochus wrote: post #70

Earlier quoted context omitted.

Don't tell me you don't know this service. It's extremely useful to get to know the code and architecture of a project. You can even ask questions about the code and get the relevant references to the corresponding sections in the source files.

Okay but that's not a wiki. Wiki implies pages can be collaboratively edited and linked. Otherwise it's not a wiki, it's just a website. The only collaboration here is to bait people into becoming maintainers and fix the hallucinated content. More than one maintainer has shown frustration at that site making up wrong documentation already.

Open collaborative editing is a useful feature enabled by wiki software, but I've never actually heard anyone claim it is core to the definition; it's more that it's the killer app enabled by the quick editing model embraced by WikiBase and the systems that ran on WikiBase after Cunningham made it available.

You can definitely have a wiki of one user. And it's extremely common for organizations to have a wiki of only authorized users. Although in a high trust circumstance, there's really a good reason to lock users who can read the wiki out from editing the wiki as long as edits are audited.

(Regardless of all of that, I'm fairly certain the deepwiki output is editable?)

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

#147

Post by cxr »

shadowgovt wrote: post #145
cxr wrote: post #144

Earlier quoted context omitted.

It's not "just the name of the service". The Deepwiki people are either morons or assholes or both. Complaining that someone is debasing the definition of the word "wiki" by applying it to something that isn't a wiki is not a trifling complaint. Describing a topic-constrained encyclopedia as a "wiki" on the basis that Wikipedia is a thing is like calling coffee "ice" because iced coffee exists.

Or a quickly-editable website a "wiki" because it's the Hawaiian word for "quick."

Which these things aren't.

But congratulations on grasping what a wiki is, I guess.

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

#148

Post by shadowgovt »

cxr wrote: post #147
shadowgovt wrote: post #145

Earlier quoted context omitted.

Or a quickly-editable website a "wiki" because it's the Hawaiian word for "quick."

Which these things aren't. But congratulations on grasping what a wiki is, I guess.

Are they not editable? They do appear to have an edit button.

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

#150

Post by irundebian »

indolering wrote: post #136
irundebian wrote: post #119

Earlier quoted context omitted.

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?

I mean, they do all the time. The value is generally in keeping access, however, and operational security and access control is helpful. You can knock a system out but then you just get kicked out and have to start over.

Do you have evidence for that?
Post reply on HN