5 ms·

Interesting project. I'm curious about the limits of formal verification of worst case execution time. There are other formally verified kernels like seL4 and a

Interesting project. I'm curious about the limits of formal verification of worst case execution time. There are other formally verified kernels like seL4 and atmosphere, as well as layers you can stack on top to get a mostly compatible posix-ish layer like genode. You can also go out and find completely compatible kernels with enough maturity that (full) formal verification isn't a major value-add, like QNX or VxWorks. I'm not aware of much that combines WCET + formal verification + POSIX compatibility though. The verification page here is mostly at stone level, which from my understanding of SPARK terminology just means it passes validation, but might have runtime errors where most of Ada's WCET nondeterminism comes from. I'm skeptical that this is actually production usable for the hard real-time use cases all over their documentation at the current stage, but nothing on the website gives any clue as to the actual maturity short of reading the code myself.

indolering 1y ago
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 privileges from code and is too clunky to use in practice (see seLinux).
- SahAssar 1y ago
  > 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 devastating effect?
  - DANmode 1y ago
    1) Those things are being hardened right now 2) You haven’t seen a hot conflict yet
  - indolering 1y ago
    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 that can extract information from locked phones [2]. Availability of that sort of access to anyone's phone by local law enforcement is absurdly cheap. [1]: https://opzero.ru/en/prices/ https://opzero.ru/en/prices/ [2]: https://arstechnica.com/gadgets/2025/10/leaker-reveals-which-pixels-are-vulnerable-to-cellebrite-phone-hacking/ https://arstechnica.com/gadgets/2025/10/leaker-reveals-which...
    - SahAssar 1y ago
      > [1]: https://opzero.ru/en/prices/ 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-pixels-are-vulnerable-to-cellebrite-phone-hacking/ 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 in their couch." That implies that Kiribati currently could easily buy RCE on for example hardened Linux or OpenBSD running the most sensitive infra in the world. I just don't buy that, since if it was true any current conflict would look much different. Of course there are security holes and major fuckups do happen, but not at the scale the parent implied.
      - indolering 1y ago
        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 sized security outfit selling to the cops and the FBI. When activists lobbying for a fucking sugar tax in Mexico get hacked, then the bar is too fucking low. Let's not talk about the nightmare that is old networking equipment or IoT devices.
- vacuity 1y ago
  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 other hand, it continues the trend of L4 microkernels demonstrating the viability of stricter designs. But keep in mind that more time and effort is necessary to implement larger systems well. I'm bullish on capabilities too, but I don't know much about MAC. Can you explain your last sentence?
  - dathinab 1y ago
    they mean "mandatory access controls (MAC)" https://en.wikipedia.org/wiki/Mandatory_access_control https://en.wikipedia.org/wiki/Mandatory_access_control through what exactly people mean with it is often vague Like e.g. both seLinux and AppAmore are technically MAC but people tend to only mention seLinux when speaking about how cumbersome it is and treat AppAmore as something different as it's not so cumbersome.
  - indolering 1y ago
    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 https://sel4.systems/performance.html [2]: https://lionsos.org/ https://lionsos.org/ [3]: https://trustworthy.systems/publications/papers/Heiser_25%3Akisv.abstract https://trustworthy.systems/publications/papers/Heiser_25%3A...
johnisgood 1y ago
It does not have to remain at stone level, and it can get legit certifications, too. Looking forward to it. A formally verified OS is a great step towards better security.
- AlotOfReading 1y ago
  That really depends on what formal verification means in context. I don't see any interesting specifications in the repo, just basic stuff like this MD5 spec [0] that doesn't verify whether the MD5 implementation is correct. This is one of the areas where formal verification is listed as completed/gold level. It's common for the interesting OS proofs to take more code than the kernel itself. Take a look at the seL4 proofs [1], or those for CertiKOS as examples. If you're actually interested in alternative OSes in memory safe languages, you might like TockOS, which is more production-ready at this point. Formal verification work of the isolation model is still ongoing, because it's difficult work. [0] https://codeberg.org/Ironclad/Ironclad/src/branch/main/source/cryptography/cryptography-md5.ads https://codeberg.org/Ironclad/Ironclad/src/branch/main/sourc... [1] https://github.com/seL4/l4v https://github.com/seL4/l4v
  - johnisgood 1y ago
    There is none in [0]. :P

indolering 1y ago

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 privileges from code and is too clunky to use in practice (see seLinux).

SahAssar 1y ago
> 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 devastating effect?
- DANmode 1y ago
  1) Those things are being hardened right now 2) You haven’t seen a hot conflict yet
- indolering 1y ago
  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 that can extract information from locked phones [2]. Availability of that sort of access to anyone's phone by local law enforcement is absurdly cheap. [1]: https://opzero.ru/en/prices/ https://opzero.ru/en/prices/ [2]: https://arstechnica.com/gadgets/2025/10/leaker-reveals-which-pixels-are-vulnerable-to-cellebrite-phone-hacking/ https://arstechnica.com/gadgets/2025/10/leaker-reveals-which...
  - SahAssar 1y ago
    > [1]: https://opzero.ru/en/prices/ 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-pixels-are-vulnerable-to-cellebrite-phone-hacking/ 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 in their couch." That implies that Kiribati currently could easily buy RCE on for example hardened Linux or OpenBSD running the most sensitive infra in the world. I just don't buy that, since if it was true any current conflict would look much different. Of course there are security holes and major fuckups do happen, but not at the scale the parent implied.
    - indolering 1y ago
      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 sized security outfit selling to the cops and the FBI. When activists lobbying for a fucking sugar tax in Mexico get hacked, then the bar is too fucking low. Let's not talk about the nightmare that is old networking equipment or IoT devices.
vacuity 1y ago
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 other hand, it continues the trend of L4 microkernels demonstrating the viability of stricter designs. But keep in mind that more time and effort is necessary to implement larger systems well. I'm bullish on capabilities too, but I don't know much about MAC. Can you explain your last sentence?
- dathinab 1y ago
  they mean "mandatory access controls (MAC)" https://en.wikipedia.org/wiki/Mandatory_access_control https://en.wikipedia.org/wiki/Mandatory_access_control through what exactly people mean with it is often vague Like e.g. both seLinux and AppAmore are technically MAC but people tend to only mention seLinux when speaking about how cumbersome it is and treat AppAmore as something different as it's not so cumbersome.
- indolering 1y ago
  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 https://sel4.systems/performance.html [2]: https://lionsos.org/ https://lionsos.org/ [3]: https://trustworthy.systems/publications/papers/Heiser_25%3Akisv.abstract https://trustworthy.systems/publications/papers/Heiser_25%3A...

johnisgood 1y ago

It does not have to remain at stone level, and it can get legit certifications, too. Looking forward to it. A formally verified OS is a great step towards better security.

AlotOfReading 1y ago
That really depends on what formal verification means in context. I don't see any interesting specifications in the repo, just basic stuff like this MD5 spec [0] that doesn't verify whether the MD5 implementation is correct. This is one of the areas where formal verification is listed as completed/gold level. It's common for the interesting OS proofs to take more code than the kernel itself. Take a look at the seL4 proofs [1], or those for CertiKOS as examples. If you're actually interested in alternative OSes in memory safe languages, you might like TockOS, which is more production-ready at this point. Formal verification work of the isolation model is still ongoing, because it's difficult work. [0] https://codeberg.org/Ironclad/Ironclad/src/branch/main/source/cryptography/cryptography-md5.ads https://codeberg.org/Ironclad/Ironclad/src/branch/main/sourc... [1] https://github.com/seL4/l4v https://github.com/seL4/l4v
- johnisgood 1y ago
  There is none in [0]. :P