Formally Verified Software in the Real World (2018)

186 points by icc97 6 years ago | 17 comments
  • tpaschalis 6 years ago
    Second day in a row where HN frontpage features formally verified software!

    If you're like me, and would like to get started, or just see what this is all about, the TLA+ homepage and video course (narrated by Leslie Lamport himself), is a nice resource [1].

    In about half an hour you will have a brief understanding of what "formal specification languages" are, write and 'prove' your first small program/spec. If you have another hour to spend, keep the cheatsheet [2] near you and follow through, you will write and 'prove' more complex specs, plus you'll start thinking about systems in a more abstract way. Finishing up the video course you'll be able to start reading complex specs others have written, or write a spec for any algorithm you think is fun!

    [1] https://lamport.azurewebsites.net/video/videos.html [2] https://lamport.azurewebsites.net/tla/summary-standalone.pdf

    • drharby 6 years ago
      I really want this to be a sarcastic post demonstrating how thinly veiled some pr efforts are
    • dahfizz 6 years ago
      Kind of a dumb question: have any operating systems been formally verified? Unless you are running an embedded application, verifying your software seems kind of pointless if you are still at the mercy of "unverified" system calls, memory manager, scheduler, etc etc.
      • brians 6 years ago
        Yes! But none you want to use on a workstation. Honeywell and Burroughs both produced A1 verified operating systems—presumably there are successors there or at General Dynamics. There are some Russian attempts as well. Nobody else had the engineers, the mathematicians, and the money to build a verified system.

        The standards there assume a TCB of about 10 kloc; 5kloc for the OS, 5kloc for each application. Separation is by static allocation—of disk space and memory usage, but also static time-domain multiplexing of CPU cores and IO lanes, with caches flushed on every context switch. They’re ferociously expensive to acquire in the first place, and then you take a huge operational penalty for running multiple applications.

        There are very few problems for which this is a helpful solution—maybe not none, but very few when you could just buy several distinct computers, run them airgapped, and go about your business.

        • nickpsecurity 6 years ago
          Depends on if you mean design or code. In old days, there was STOP, GEMSOS, and LOCK. I have a description of two of them:

          http://www.cse.psu.edu/~trj1/cse443-s12/docs/ch6.pdf

          Later on, the separation kernels:

          https://arxiv.org/pdf/1701.01535

          VerveOS was verified at least for safety down to assembly:

          https://www.microsoft.com/en-us/research/wp-content/uploads/...

          The Muen separation kernel and hypervisor is verified to be free of common problems:

          https://muen.sk/

          • heyjudy 6 years ago
            seL4 https://sel4.systems/
            • kccqzy 6 years ago
              Green Hills Software has the Integrity operating system rated to EAL6+, which stands for "Semiformally Verified Design and Tested" so almost there but not quite.

              But honestly it's not something you would want to use in daily life.

              • heyjudy 6 years ago
                Not to the rigor seL4 has, with multiple-levels of verification.
                • kccqzy 6 years ago
                  Yes I agree, but still with significantly more rigor than your typical operating system (Linux, Windows, macOS).
              • Nokinside 6 years ago
                The question is to what degree.

                * EAL5 (Semiformally Designed and Tested) Logical partitions in IBM System Z.

                * EAL6 (Semiformally Verified Design and Tested) INTEGRITY-178B and SeL4 I think.

                * EAL7 (EAL7: Formally Verified Design and Tested). No operating system has been verified to this level. Only small number of data diodes and other some specialized systems have this level of assurance. https://www.fox-it.com/datadiode/certificates/cc-eal7-certif...

                • pron 6 years ago
                  PharOS RTOS: https://members.loria.fr/SMerz/papers/abz2016-pharos.html
                  • gok 6 years ago
                    seL4
                  • jschwartzi 6 years ago
                    I have wanted to see a real-world use of seL4 in a safety-critical system since I heard about it 2 years ago. This is really impressive, and I'm very happy to see this here.
                    • nestorD 6 years ago
                      The exemple I was given while studying the subject is that the sofware for the driverless metro line 14 in Paris has been proven in Coq.
                    • 6 years ago