Thread

Several vulnerabilities have been discovered in the Linux kernel

576 points · 408 comments · luispa

intrepidsoldier · 1790914300 · focus · HN ↗
Just the beginning. AI is going to expose how fragile the entire computing infrastructure in our world is.
1. jaypatelani · 1790916250 · focus · HN ↗
  Because most devs don't want to do formal verified system development. I know only one OS working on that which is open source Ironclad OS hope many others follow this path. It is Ada/SPARK based but others should do with whatever language they are using. NetBSD also heard going to do something similar with C in last AGM
  1. iamnothere · 1790965572 · focus · HN ↗
    Genode as a whole isn’t formally verified, but it can use seL4 as a kernel, and it uses a robust capabilities system to sandbox basically everything, including drivers.
    As it evolves I suspect there will be a push to verify more components of the stack. Once the capabilities layer can be verified, verification of most other components and drivers would become much less urgent.

Unofficial Hacker News client; not affiliated with Y Combinator.