posted by
janrinok
on Sunday August 03 2014, @03:15AM
from the verified-if-assumptions-are-correct dept.
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.
Formally Verified Microkernel seL4 Open Sourced
|
Log In/Create an Account
| Top
| 15 comments
| Search Discussion
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
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
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
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
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
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
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])
And
This is actually an order of magnitude above the kernel development effort (2py). They *think* this might come down and...
"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
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
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
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
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:
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
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
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
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
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
Interesting to watch the next generation of concepts in system design meet real world integration.