Slashdot Mirror

← Back to Stories (view on slashdot.org)

seL4 Verified Microkernel Now Open Source

Posted by Unknown on from the formal-verification-for-the-rest-of-us dept.

Back in 2009, OKLabs/NICTA announced the first formally verified microkernel, seL4 (a member of the L4 family). Alas, it was proprietary software. Today, that's no longer the case: seL4 has been released under the GPLv2 (only, no "or later versions clause" unfortunately). An anonymous reader writes OSnews is reporting that the formally verified sel4 microkernel is now open source: "General Dynamics C4 Systems and NICTA are pleased to announce the open sourcing of seL4, the world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement. It is still the world's most highly assured OS." Source is over at Github. It supports ARM and x86 (including the popular Beaglebone ARM board). If you have an x86 with the VT-x and Extended Page Table extensions you can even run Linux atop seL4 (and the seL4 website is served by Linux on seL4).

16 of 82 comments (clear)

  1. Unfortunately? by ichthus · · Score: 2

    (only, no "or later versions clause" unfortunately)

    You mean, fortunately. Now, it's more likely to actually be used.

    --
    sig: sauer
    1. Re:Unfortunately? by tlhIngan · · Score: 2, Insightful

      How does the "or later" clause hinder use? Licensing under GPLv3 might have (I'm not going to argue that either way), but what does the "or later" clause matter?

      Because you cannot mix v2-only code with v3/v3+ code. It's actually incompatible - v3 puts additional "restrictions" (from v2's perspective) on the code, making it incompatible (e.g., anti-TiVoization, etc).

      So this means all code in that kernel must be either v2 or v2+ (which means the "+" disappears).

      For an embedded systems, they typically want GPLv2 or v2+, avoiding v3 as much as possible. "or later" can hinder since if you're not careful, you might accidentally include v3 code (especially if you pull from an upstream source) when you don't want to. v2-only makes that a license violation, while v2+ turns into v3/v3+. One should be careful when pulling patches to make sure the codebase doesn't unexpectedly turn into v3.

    2. Re:Unfortunately? by vux984 · · Score: 2

      If "GPLv2 only" is silly, then you might want to alert all the Linux kernel developers.

      Your kidding right? Alert them of what? Something they all already know?

      As the kernel has no centralized copyright authority; the license is stuck where it is regardless of what anyone contributing to it wants or doesn't want.

      Linus has been quoted saying he doesn't care for GPLv3 himself, and has no plans to change the kernel over; which is fine...(especialyl as its would be a fuckton of work -- due to each contributor to the kernel ever all having to either agree to the change or have their contribution pulled out and recoded from scratch). However it doesn't really answer the question of whether Linus actually objects to "GPLv2 or later" -- since it doesn't put any additional constraints on him; or anyone else contributing to the kernel -- the only upshot is that someone somewhere downstream might at some point create a gplv3+ distro based on the kernel. I'm really not sure Linus cares about that; if he doesn't care about Tivoization, what does he care if RMS and the FSF put together a pure gplv3 distro?

      To me, at least, the choice of GPLv2 for the kernel instead of GPLv2 or later seems like, an oversight at best, that really can't be fixed now. After all, the kernel was one of the earlier works to use the GPL; it was still pretty new at the time. And Linus was not making a statement about Tivoization or GPLv3 or anything else when he didn't include the "or later" clause.

    3. Re:Unfortunately? by ichthus · · Score: 2

      I made a statement about GPLv2 being more conducive than its successors to project adoption, and you obviously disagree with this statement. Because of this -- because your opinion differs, I'm trolling? You need to go to wikipedia and learn.

      --
      sig: sauer
    4. Re:Unfortunately? by DamnOregonian · · Score: 2

      I have licensed GPL code (some of it Linux kernel code). I specifically didn't care about the idea of tivoization, and was even running a tivoized device that I developed it for (cell phone).

      I have a distaste for the practice, to be sure, but for me the selection of GPL licensing even where I'm not really required to is more about just making sure that improvements or ports of the code make it back. Companies that tivoize are shit-bags. They're also more likely to give something back, though, and that's better than nothing. I'd prefer not to limit their rights for how they use my code. That's more about morality, and they can deal with the consequences of their immorality without me enforcing it upon them. My improved comes back, that's good enough for me.

    5. Re:Unfortunately? by vux984 · · Score: 2

      GPLv2 is purely about code openness and code contribution but not about FSF ideals.

      Not according to the people who actually WROTE the GPLv2. You made a good point about *some* of the people who chose to use it, but that is not what the GPLv2 was written FOR.

  2. More info by Enry · · Score: 4, Informative

    http://sel4.systems/FAQ/

    Is it really that hard to give more background information?

  3. Knuth said it best by Anonymous Coward · · Score: 2, Informative

    It may have been proven correct, but lets wait and see until after it's actually been used if it really is.

    (Knuth said (paraphrased): be aware of bugs in the above code. I have only proved it to be correct; I have not tried it.)

    1. Re:Knuth said it best by Beck_Neard · · Score: 2

      Well, 'proven correct' assumes that the proof itself is correct (verification), that the proof actually proves the correct thing (validation), and that the underlying system actually conforms to its formal specification (another thing that's hard to verify - formally-verified CPU design anyone?). These people seem to have done their homework so I'll be looking at this more closely, but based on experience it's pretty much guaranteed that there's going to be some unconsidered vulnerability somewhere.

      --
      A fool and his hard drive are soon parted.
  4. A good step forward... by ndykman · · Score: 3, Interesting

    I feel an explaination may help. This project is based on a formal specification (in Isabelle/HOL) about what should be true about the microkernel. This specification rules out things like buffer overflows, null pointer dereferences and other properties by recasting these ideas in terms of higher order logic and uses automatic theorem proving tools to verify the proofs and that implementations match the specification.

    There's even a binary verified version for ARM, so you don't even have to trust that your compiler works (but, there is progress in verified compilers, so hopefully an x86_64 version is on the way). The value in this is in using the tool chain and creating new, formally specified abstractions and implementing them in an verified manner to implement more secure, robust programs on top of this kernel. Of course, the microkernel makes assumptions about the hardware, boot loader, but formal verification is used more often in hardware, and you have to trust something at some point.

    This opens a whole set of possibilities to the community as a whole. As a random example, you could formalize the Arduino language (or a kernel for that language) and create a verified version of that system that runs on this microkernel. This would be a big effort, but you could do it.

    Overall, this is a positive step in lower the costs of verified co-designed systems and I hope it attracts more interest in software formal verification.

  5. Re:You can't choose forever. Once v3 touches it, g by Immerman · · Score: 2, Informative

    Yes, it does mean that any code including v3 code can only be legally licensed as v3 - but there's nothing stopping you from later extracting the offending code and reverting to v2+. You don't magically change the 2+ license under which you gained rights to the other code, you just only have the option of redistributing it under v3 so long as any v3-only code is included. So long as you make sure all contributions made in the interim are made under v2+ you don't have a problem (i.e. v3-only licensing can only spread if you let it).

    --
    --- Most topics have many sides worth arguing, allow me to take one opposite you.
  6. Proof by manu0601 · · Score: 2

    While proved software is much better than unproved software, this is not the end of security holes: The proof assumes hardware and compiler behave as specified, which lets a lot of attack surface.

    At least it raises the bar much higher.

    1. Re:Proof by flux · · Score: 2

      While there have been some Linux bugs due to the compiler, I can't really recall hardware problems that have caused security problems â" unless you already have physical access, and then all bets are off.

      The compiler issue could be addressed by using a certified compiler, such as this: http://compcert.inria.fr/ . Sadly CompCert is not FOSS.

    2. Re:Proof by jones_supa · · Score: 2

      Sadly CompCert is not FOSS.

      To me it looks like FOSS. The source code is available to download and it allows to choose between INRIA Non-Commercial License and GNU GPLv2.

  7. What exactly is the point? by Half-pint+HAL · · Score: 2

    Surely a formally-proven OS doesn't want a traditional open-source license, because if you let people tinker, what you will end up with is forking... into unproven versions. And suddenly, the world's first formally-proven microkernel is just a plain old microkernel again.

    OK, so maybe tinkering is alright as a personal hobby, but it risks the ecosystem.

    --
    Got them moderator blues I blieve I walk out the do', With these mod-points I been gettin', I 'most never post no mo'
    1. Re:What exactly is the point? by mr_mischief · · Score: 2

      It allows others to borrow the code into their GPLv2 projects. It also allows others to make modifications which are not proven, but potentially those could be audited and proven, too.