There is an NDA related company called ironclad as well. Beware the trademark/copyright terrorists.
That said, I am huge fan of works like this. But in practice, the security layer that betrays all of this tends to be the firmware layer.
My dream is to have something like the Framework computer use verifiably secure EFI firmware, as well as similarly verified and audited firmware for every hardware component.
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.
From their verification roadmap, it sure seems generous to refer to this as “formally verified”. They don’t prove anything important about the kernel clearly at all. Seems very disingenuous to describe it as they do since it lacks any of the merits of other formally verified kernels like seL4 and Tock.
Can we use Rust / Go / Java (GraalVM Native) or Flutter Linux to build an executable that runs on an OS with an Ironclad kernel? Or is there special treatment that makes it incompatible with "plain" Linux exe?
A couple weeks ago I was curious what the strictest programming language was. ChatGPT listed a couple, and it kicked off a short discussion where I began asking it about the capabilities of stricter programming languages at low levels. Funny enough at the end it mentioned that SPARK/Ada was the strictest you could get at the lowest levels, same as Ironclad.
At one point while asking it about drivers, it said "ACL2’s logic is [...] side‑effect‑free definitions with termination proofs when admitted to the logic. That is misaligned with effectful, interrupt‑driven kernel code.
I'm not an OS or kernel dev, most of my work has been in Web Dev, ML, and a little bit of embedded. How accurate is the information that was presented to me? Here is the link to the discussion: https://chatgpt.com/share/691012a7-a06c-800f-9cc9-54a7c2c8b6...
I don't know SPARK or Ada, but it just bothers me to think that we can't...I guess...prove everything about our software before we run it (yes yes, I'm familiar with halting problem shenanigans, but other than that).
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.
As far as I know formal verification is another testing method and as as such it's is as good as the quality and the extent of the "verification" (aka tests).
Best way to verify that I know of is Fuzzing + testing.
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:
What I like most about ironclad is that it is fully posix-compliant, meaning that you can run a lot of UNIX programs on it already, like what "Gloire" does: https://github.com/Ironclad-Project/Gloire
22 comments
[ 4.7 ms ] story [ 44.6 ms ] threadWhat other exciting projects like these exist?
That said, I am huge fan of works like this. But in practice, the security layer that betrays all of this tends to be the firmware layer.
My dream is to have something like the Framework computer use verifiably secure EFI firmware, as well as similarly verified and audited firmware for every hardware component.
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.
I thought SPARK was a paid (not free) license. Am I mistaken?
Very cool project btw.
https://codeberg.org/Ironclad/Gloire
A couple weeks ago I was curious what the strictest programming language was. ChatGPT listed a couple, and it kicked off a short discussion where I began asking it about the capabilities of stricter programming languages at low levels. Funny enough at the end it mentioned that SPARK/Ada was the strictest you could get at the lowest levels, same as Ironclad.
At one point while asking it about drivers, it said "ACL2’s logic is [...] side‑effect‑free definitions with termination proofs when admitted to the logic. That is misaligned with effectful, interrupt‑driven kernel code.
I'm not an OS or kernel dev, most of my work has been in Web Dev, ML, and a little bit of embedded. How accurate is the information that was presented to me? Here is the link to the discussion: https://chatgpt.com/share/691012a7-a06c-800f-9cc9-54a7c2c8b6...
I don't know SPARK or Ada, but it just bothers me to think that we can't...I guess...prove everything about our software before we run it (yes yes, I'm familiar with halting problem shenanigans, but other than that).
A guy can dream, at least.
As far as I know formal verification is another testing method and as as such it's is as good as the quality and the extent of the "verification" (aka tests).
Best way to verify that I know of is Fuzzing + testing.
https://en.wikipedia.org/wiki/TUNIS
It was implemented in Concurrent Euclid.
https://en.wikipedia.org/wiki/Concurrent_Euclid
1. https://blog.adacore.com/cubit-a-general-purpose-operating-s...
2. https://github.com/docandrew/CuBit
What filesystems are supported ?