Stories
Slash Boxes
Comments

SoylentNews is people

posted by janrinok on Sunday August 03 2014, @03:15AM   Printer-friendly
from the verified-if-assumptions-are-correct dept.

seL4, a formally verified ("bug-free") L4 microkernel variant designed to provide strong security properties, has been released under the GPLv2. The proof is written in Isabelle and the code in C. Both the C code and the binaries produced from it have been proven to meet a formal specification. Further, it has been proven that the specification can be used to enforce the properties of integrity and confidentiality. (The proof currently only applies to the ARM port, and a list of proof assumptions and limitations is available.)

This discussion has been archived. No new comments can be posted.
Display Options Threshold/Breakthrough Mark All as Read Mark All as Unread
The Fine Print: The following comments are owned by whoever posted them. We are not responsible for them in any way.
  • (Score: 0) by Anonymous Coward on Sunday August 03 2014, @03:45AM

    by Anonymous Coward on Sunday August 03 2014, @03:45AM (#76831)

    Would this kernel work with GNU HURD? Maybe it would help keep the project moving?

    • (Score: 0) by Anonymous Coward on Sunday August 03 2014, @04:12AM

      by Anonymous Coward on Sunday August 03 2014, @04:12AM (#76835)

      Good Lord no. They shifted microkernel cores more times than I care to remember. First is was Mach, then L4, and then Coyotos and now who knows. The fact that they've kept doing this is probably the greatest hurdle (no pun intended) that has kept them from building a complete, viable system. They should just stick to one foundation and run it to completion. Similar decisions kept Duke Nukem Forever in vapour-ware status for so long (they kept changing 3D engine cores).

      • (Score: 4, Informative) by forsythe on Sunday August 03 2014, @05:36AM

        by forsythe (831) on Sunday August 03 2014, @05:36AM (#76846)

        That's not entirely correct. They have tried to shift kernels multiple times, but they always have stuck with Mach in the end. This is not to heap any praise on Mach, rather the HURD was designed when Mach was the only real microkernel around, and so HURD has grown around Mach in a very organic fashion.

        The latest real attempt to replace Mach was the Viengoos kernel, which, as I recall, barely made it to bare metal, then ran into some problems getting things like `fork' working.

    • (Score: 4, Interesting) by forsythe on Sunday August 03 2014, @05:42AM

      by forsythe (831) on Sunday August 03 2014, @05:42AM (#76847)

      If it worked, it would be a tremendous boost to the project. If [soylentnews.org] it worked, to blow my own horn a little. Mach is one of the big things holding HURD back, but it would be a huge deal of work to replace it at this point. It may very well require more manpower than is at the team's disposal.

  • (Score: 0) by Anonymous Coward on Sunday August 03 2014, @08:27AM

    by Anonymous Coward on Sunday August 03 2014, @08:27AM (#76861)

    The possibly most encouraging lesson from the project, other than that it succeeded
    at all, is the cost: our analysis of the development and verification effort shows that,
    with the right approach, formally verified software is actually less expensive than tradi-
    tionally engineered "high-assurance" software, yet provides much stronger assurance
    than what is possible with traditional software-engineering approaches.

    -- https://www.nicta.com.au/pub?doc=7371 [nicta.com.au] (PDF)

    • (Score: 2, Interesting) by tonyPick on Sunday August 03 2014, @12:09PM

      by tonyPick (1237) on Sunday August 03 2014, @12:09PM (#76881) Homepage Journal

      Although, from the link you provided (which is the same as the published http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf [sigops.org])

      "The proof is constructed and checked in Isabelle/HOL and comprises over 200,000 lines of proof script to verify 6,500 lines of C."

      And

      "The effort for proving the correctness of seL4 is significantly higher than developing the kernel in the first place, in total about 20 py" (py = person years)

      This is actually an order of magnitude above the kernel development effort (2py). They *think* this might come down and...

      ...reduce this figure to 6 py, for a total (kernel plus proof) of 8 py.This is only twice the SLOCCount
      estimate for a traditionally-engineered system with no assurance.

      "Only" twice? This is some new usage of the word "Only" which I haven't previously encountered. From an engineering perspective; that's not necessarily a great tradeoff for a proof which is only accurate for a single platform, within an optimistic set of assumptions (no HW errata? Ha!) and provided that the "30x the size" proof script is good, and also will need continuous reworking on updates ("The cost of change" section).

      Which isn't to say it's not a great thing to have, but I'm not seeing a solid comparison of that cost versus putting the time & effort into integration and module testing, static analysis, peer review and a host of other validation efforts (there's a bit about the "standard industry" and EAL6/7 costs, but not much else detail wise).

      It'd be interesting if the paper did a comparison of various validation methods in terms of time spent/defects uncovered/defects not uncovered, but it doesn't do that, so it's hard to say it's a "better" choice from this result and I'm finding the conclusion to be a bit of a stretch outside a fairly narrow set of implementations. (Although you might be able to use these numbers to figure something more general out). Overall - interesting, but "Science > engineering"? Nah.

      • (Score: 3, Insightful) by cafebabe on Sunday August 03 2014, @12:45PM

        by cafebabe (894) on Sunday August 03 2014, @12:45PM (#76887) Journal

        Program testing can be used to show the presence of bugs, but never to show their absence. -- Edsger W. Dijkstra

        Proving absence of bugs (with assumptions) is a big deal even if it takes 10 times more effort than writing the code. And proving a whole kernel is quite impressive. Certain classes of bugs will be absent even if some bugs remain.

        --
        1702845791×2
        • (Score: 2, Interesting) by tonyPick on Sunday August 03 2014, @02:15PM

          by tonyPick (1237) on Sunday August 03 2014, @02:15PM (#76900) Homepage Journal

          Completely agree; it is an impressive achievement.

          However my interest is that: from a practical perspective of writing software many (most?) of us will be trading finite time and effort for (some given metric of) quality in (non-safety critical) applications.

          This approach has proven we're bug free[1], and no other approach will give you that guarantee, but if we can take 10% of the time/effort and expect to nail down 99% of the defects, and catch some additional practical issues this approach won't, that may be a good trade with the resources available for some cases.

          Sure if you're doing safety critical then this formal methods are what you want (and would/should be prepared to pay for) but many of us aren't and I'd like to know how the state of the art of this approach and the associated tooling compares to what else is out there before declaring this approach a "winner". (and this may exist, I just haven't chased it).

          [1] Actually, being nitpicky, I might be tempted to argue this method has only shown the agreement of the code with the formal proof script on a theoretical platform. Or to steal a quote "A formal proof can be used to show the agreement of the code with the proof, but never the absence of bugs." -- Me. Just Now.

          • (Score: 2) by cafebabe on Sunday August 03 2014, @03:45PM

            by cafebabe (894) on Sunday August 03 2014, @03:45PM (#76917) Journal

            While this is an impressive achievement, it isn't (yet) a silver bullet which will solve all programming problems. However, it gives us another tier between cowboy coding and perfection. If your project is mission critical and has the resources, it is now possible to expend extra effort to shake out bugs not found with unit testing, integration testing, fuzz testing, stress testing, beta testing or other tests.

            Even though verification is a laborious process and won't find many bugs, it is an advance on productivity. 20 person years to verify 6,500 lines of C is significantly more productive than the NASA shuttle flight guidance system in which programmers were contributing four lines of code per year with bugs [fastcompany.com]. And the verification approach is expected to exceed 1,000 lines per year in the near future.

            With this advance, verification may yet become widespread. In a culture of "something-must-be-done, think of the hackers/terrorists/paedophiles/rapists!!!1!" we may find that the falling cost of verification becomes a point of litigation. Specifically, failure to perform verification (or use a language suitable for verification) is a matter of professional negligence.

            Regarding flaws in a formal proof system, we may encounter the problem that any practically tractable set of axioms in a proof system may be inconsistent [wikipedia.org].

            --
            1702845791×2
            • (Score: 1) by tonyPick on Sunday August 03 2014, @07:08PM

              by tonyPick (1237) on Sunday August 03 2014, @07:08PM (#76945) Homepage Journal

              Well, the further away from Cowboy Coding the better, so that gets a +1 "hell yes" from me. (Although with the clear rise of crimes in the name of agile I suspect we're in a minority there)

              However as we both agree this isn't a silver bullet (TINSB), and so whilst I would also agree that at the high end of the reliability requirements game this *is* shown as a definite improvement the key thing is, I think, the phrase:

              If your project is mission critical and has the resources, it is now possible to expend extra effort to shake out bugs not found with unit testing, integration testing, fuzz testing, stress testing, beta testing or other tests.

              I think that, as a jobbing computer typist, the key questions for me then are: "How much effort? How many and what type of bugs? What issues did it miss, and what did it uniquely identify? What other techniques complement this well?".

              If you can afford to do everything then great, but most of us outside the critical systems sector (for schedule or resource reasons) can't, so for the approach to become widespread and improve code quality generally then the question is what do I do this instead of, and how do we quantify when is it a net win? Where might it be useful outside the mission critical space and can/will it help us all build better software generally?

              Since this case had an opportunity to do that, reviewing a practical scale system in a controlled setting, and give us some concrete comparison metrics against alternate techniques, then the large overhead caveats, given the OP "Science wins, Yay!" post & extract was a fairly disappointing read (It actually reminded me slightly of the points made in Greg Wilson's excellent "What We Actually Know..." talk at http://vimeo.com/9270320 [vimeo.com]). So whilst I'll spin up & play with the Isabelle/HOL tool for a bit, it's unlikely to make it into the day job as a result.

          • (Score: 0) by Anonymous Coward on Sunday August 03 2014, @05:32PM

            by Anonymous Coward on Sunday August 03 2014, @05:32PM (#76929)

            However my interest is that: from a practical perspective of writing software many (most?) of us will be trading finite time and effort for (some given metric of) quality in (non-safety critical) applications.

            Think of it as full-employment for developers even in the face of 3rd world countries flooding the labor market. A tedious, boring as hell employment, but a job's a job.

      • (Score: 2) by maxwell demon on Sunday August 03 2014, @04:53PM

        by maxwell demon (1608) on Sunday August 03 2014, @04:53PM (#76922) Journal

        Did they also prove the correctness of the proof script?

        Anyway, the whole point of a microkernel is to minimize the code it consists of, by minimizing its responsibilities. Which also means you minimize the future changes that will be necessary for that code.

        --
        The Tao of math: The numbers you can count are not the real numbers.
        • (Score: 0) by Anonymous Coward on Sunday August 03 2014, @06:03PM

          by Anonymous Coward on Sunday August 03 2014, @06:03PM (#76937)

          The old rule of thumb is that the proof is just as complex as the code, so just as likely to contain errors. That's why people have a hard time getting enthusiastic about "proofs". Has something magically changed recently?

  • (Score: 1) by cpghost on Sunday August 03 2014, @07:31PM

    by cpghost (4591) on Sunday August 03 2014, @07:31PM (#76951) Homepage

    This is awesome! I've used L4Ka::Pistachio [l4ka.org] once, and I really liked it. A formally verified kernel is even better!

    --
    Cordula's Web. http://www.cordula.ws/
  • (Score: 0) by Anonymous Coward on Monday August 04 2014, @05:24PM

    by Anonymous Coward on Monday August 04 2014, @05:24PM (#77280)

    Interesting to watch the next generation of concepts in system design meet real world integration.