3 ms·
After some brief research, I haven't found any notable emphasis on formal verification in any well-known unikernel (imperfectly defined by online searching, LLM
by xpe 3y ago
After some brief research, I haven't found any notable emphasis on formal verification in any well-known unikernel (imperfectly defined by online searching, LLM exploration, and focusing on languages like Haskell and Rust that tend to more interested in correctness). Did I miss anything? Even the Wikipedia pages lacks any mention of verification.
The closest I've found was a Reddit article titled "Stardust Oxide: I wrote a unikernel in Rust for my bachelors dissertation" with this comment "My impression, after investigating Singularity for my own undergrad: No. They did bytecode varification against a manifest after codegen, in their own intermediate language that all installed programs had to use. For the Rust compiler I imagine you're thinking of doing certification against the module sources? That's not going to provide the same level of verification."
- anentropic 3y agoNo idea if any others are closer to that ideal, but MirageOS unikernel (OCaml) offers nods in that direction: "Possible to formally verify critical components" https://www.cs.williams.edu/~cs432/osco/01-whit.pdf https://www.cs.williams.edu/~cs432/osco/01-whit.pdf "As part of our mission to build robust and secure systems, we strive to support technology that roots its design in the field of formal methods" has a TCP stack manually derived from a formal model https://tarides.com/blog/2024-01-24-mirageos-designing-a-more-resilient-networking-stack-with-tcp/ https://tarides.com/blog/2024-01-24-mirageos-designing-a-mor...
- xpe 3y agoThanks. / My interest is centered around AI safety. It seems clear that any learning system* that can improve its own code must be run in a provably secure virtual environment (at the very least). * by learning system I include any system that learns from experience