‹ BackHN Continuity

Thread

Several vulnerabilities have been discovered in the Linux kernel

576 points · 408 comments · luispa

  1. intrepidsoldier · · focus · HN ↗
    Just the beginning. AI is going to expose how fragile the entire computing infrastructure in our world is.
    1. jaypatelani · · 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. csrse · · focus · HN ↗
        There is also LionsOS <a href="https:&#x2F;&#x2F;lionsos.org&#x2F;" rel="nofollow">https:&#x2F;&#x2F;lionsos.org&#x2F; (SeL4-based).
      2. RossBencina · · focus · HN ↗
        &gt; most devs don&#x27;t want to do formal verified system development.

        That may be true. Serious question though: even if most devs wanted to develop formally verified code, do you think that it is reasonable to suggest that the typical systems developer could do it with today&#x27;s tools? I don&#x27;t mean verified protocols (TLA+) or verified algorithms (SPIN) I mean end-to-end verified code, a-la seL4. I got the impression that this is still very specialised work. Perhaps things have advanced since I last checked.

      3. menaerus · · focus · HN ↗
        Do you make your professional career by building formally verified systems? I ask because I don&#x27;t think that the reason comes down to &quot;because most devs don&#x27;t want to do formal verified system development&quot;. It&#x27;s much more complicated of course.
        1. stackskipton · · focus · HN ↗
          I could believe it. Verified system development most likely comes with metric ton of paperwork.

          Want to merge the PR? I need verified sign off in ServiceNow by staff level engineer. They are on vacation for 2 weeks? Did manager fill out delegation paperwork in ServiceNow with VP sign off? Oh they did but they forgot to put in return date AND time. Form needs to be corrected and reapproved before we can go into ServiceNow and make changes.

      4. abathologist · · focus · HN ↗
        <a href="https:&#x2F;&#x2F;sel4.systems&#x2F;" rel="nofollow">https:&#x2F;&#x2F;sel4.systems&#x2F; is relevant in this space!
      5. iamnothere · · 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.

Open on Hacker News to reply ↗

Unofficial Hacker News client; not affiliated with Y Combinator.