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

131–140 of 151 posts

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

#131

Post by snvzz »

vacuity wrote: post #125
snvzz wrote: post #53

Earlier quoted context omitted.

The most important effort is seL4[0], the fastest OS kernel out there which also happens to be the most formally verified. LionsOS[1] is its static scenario building framework, with some dynamic scenario support. Genode[2] is an independent OS construction kit that can also use the seL4 kernel. Their general purpose OS, Sculpt, just had a very interesting multi-kernel release[3]. The systems group at ETHZürich is bui…

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

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

#132

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 will check those out tomorrow, but in the meantime: I don't mean to say that a microkernel-based system is necessarily worse on performance. However, I think a highly optimized monolithic system will probably always be somewhat faster than a highly optimized microkernel-based system. And note that the seL4 system is probably less mature, and that I have many criticisms of Linux in being a supposedly highly optimized system. I'm all for microkernels. I'm planning to write one myself. But there are some aspects that microkernel-based systems have to work harder on.

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

#133

Post by indolering »

vacuity wrote: post #124
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…

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…

seL4 has the lowest IPC overhead of any kernel and it's an order of magnitude faster than Linux [1]. But you are correct: switching cost amounts of noise when architectured correctly. LionsOS [2] (which is based on seL4) has some benchmarks showing improved performance over Linux [3].

I am betting you know what mandatory access control is ; ). They basically amount to a firewall that is placed on applications restricting what they can do. The rules are generally written by downstream distros and are divorced from the implementation. The problem is that it's hidden control flow, so the program just dies and can't fall back gracefully. Capability oriented APIs make broker processes and narrowing of permissions tractable.

[1]: https://sel4.systems/performance.html

[2]: https://lionsos.org/

[3]: https://trustworthy.systems/publications/papers/Heiser_25%3A...

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

#134

Post by indolering »

Veserv wrote: post #130
indolering wrote: post #126

Earlier quoted context omitted.

Everything thinks of Defcon et al a a gathering of elite hackers. But it's more of a fucking drinking game. The depressing fact is that you don't need an RCE to accomplish most goals.

I am aware. I was making a concrete example pointing at a well known conference where average industry professionals would find the very concept of these systems being secure to be laughable. Somehow we have ended up in this bizarro land where everybody in software knows software, especially COTS operating systems, is horribly insecure due to the endless embarrassing failures yet somehow they also doublethink these s…

I was agreeing with you! It's a drinking game because the infosec field is laughable. Who needs a zero day RCE when the president is using an EOL Samsung?

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

#135

Post by indolering »

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…

It's in a proto state due to anemic academic funding. We need to throw cash at the problem.

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

#136

Post by indolering »

irundebian wrote: post #119
indolering wrote: post #77

Earlier quoted context omitted.

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?

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.

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

#137

Post by jandrewrogers »

indolering wrote: post #135
jandrewrogers wrote: post #112

Earlier quoted context omitted.

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…

It's in a proto state due to anemic academic funding. We need to throw cash at the problem.

Yes, it is underfunded for sure. I have been underwhelmed by what academia has managed to produce, funding aside. It is a solvable problem but you have to give the money to the people that can solve it in an operational context, which rarely seems to happen.

It is a genuinely fun project for someone with sufficiently sophisticated skill but I suspect there is relatively little money in it, which colors the opportunity and outcomes.

The absence of clear commercial opportunity gives the domain a weird dynamic.

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

#138

Post by indolering »

lossolo wrote: post #80
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…

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.

Thankfully, there are regulatory regimes that require physically segregated systems for most cars, airplanes, power stations, etc

However, safety critical is not limited to cars: it also includes the phones of activities and journalists living under authoritarian regimes.

Monolithic kernels written in portable assembly mean that such bugs DO grow on trees [1] and the lack backporting means they just drop to the ground: the poor are sold phones that may never receive a security update. So even sugar tax activists in Mexico are the target of spyware!

We have seen the sophistication of these attacks ramp up as cryptocurrency has made them profitable and the North Koreans have made a killing exploiting these bugs.

Maybe you are right and it is very difficult to find these bugs but that just means low demand is what is keeping the price down. But that's probably because there enough LPEs and known RCEs that they are not needed most of the time.

[1]: https://www.cvedetails.com/vulnerability-list/vendor_id-33/L...

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

#139

Post by cedilla »

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.

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

I completely agree. Maybe I should have put "air-gapped" in quotes.

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

#140

Post by lproven »

Rochus wrote: post #89
lproven wrote: post #87

Interesting. Ada is in the greater Wirthian family (it's Pascal-like), and until now, the only Unix-like kernel I was aware of in a Wirthian language was TUNIS: https://en.wikipedia.org/wiki/TUNIS It was implemented in Concurrent Euclid. https://en.wikipedia.org/wiki/Concurrent_Euclid

> the only Unix-like kernel I was aware of in a Wirthian language was TUNIS SPIN developed at the University of Washington in the nineties was written in Modula-3; it was a microkernel-based system and supported the Digital UNIX system call interface, allowing Unix applications to run. There was also Sol implemented at INRIA in a Pascal dialect in the eighties which offered a Unix-compatible environment; it was follo…

Fascinating! Thank you!
Post reply on HN