Forgot your password?
typodupeerror
Open Source Operating Systems Programming

seL4 Verified Microkernel Now Open Source 82

Posted by Unknown Lamer
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).
This discussion has been archived. No new comments can be posted.

seL4 Verified Microkernel Now Open Source

Comments Filter:
  • by ichthus (72442) on Tuesday July 29, 2014 @05:09PM (#47560865) Homepage

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

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

    • by Urkki (668283)

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

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

      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?

      • Re: (Score:3, Insightful)

        by tlhIngan (30335)

        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 GPL

        • by mx+b (2078162)
          But the clause in the statement of the GPLv2/3 is "or (at your option), any later version". There is nothing forcing someone to use v3 if it is released as v2+ -- you pick 2 or 3 based on your project since it is your option. I believe this is what GP was asking -- since you can choose forever, everyone can pick, how does it hurt anything to have "v2 or later at your option"?
          • > since you can choose forever, everyone can pick
            You cant choose forever. As soon as someone touches it with v3, it's v3 and you can't get it back.
            The most common and easiest case where that happens if that someone integrates some other GPL code into the GPL project.
            The contributor didn't realize that GPL(2) and GPL(3) are two very different things. The code integrated / copy-pasted from elsewhere was GPL3. If not caught and removed immediately, the presence of ANY GPL3 code, just one line, requires that

            • Re: (Score:3, Informative)

              by Immerman (2627577)

              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

              • True, theoretically once you know about it, you should be untangle any GPL3 code and any contributions on top of that GPL3, and any other code that borrowed from the GPL3 code. As an example of what I'm thinking of, suppose you have something modular like WordPress or Apache. Someone contributes an authentication module that includes gpl3 code. Because it includes GPL3 code, the whole module is gpl3. Someone else writes a different type of authentication module and rather than writing boring parts from s

          • by DeVilla (4563)

            ... how does it hurt anything to have "v2 or later at your option"?

            Because, if you "accidentally include v3 code" you'll only be violating one license instead of two. ....wait??!?

      • by Anonymous Coward

        Because the GPL has a certain non-free philosophy attached to it that a BSD license doesn't impose.

        If you release under GPLv2, you have to share the code and your modifications (which is fine by me in most cases) but you can't hide your changes, nor are you obligated to license everyone who uses your code/changes to your patents, which is why the GPL3 is evil and not free.

        Everyone should, when they decide on a license
        a) consider the ramifications of the license family (most software that is utilitarian in n

        • by silanea (1241518)

          [...] WHICH BY THE WAY, GPL-FREEDOMITES TEND TO DO... "hey look this file doesn't have a license, let's GPL it" [...]

          If a file does not have a license the "freedomites" fall back to default copyright, which in most cases translates to "DO NOT TOUCH!". Could you kindly point out examples where people who advocate usage of the GPL have deliberately taken third-party code with no license attached and released it under the terms of the GPL? Usually it is the other way around: People take GPL'd code and re-release it in closed source software.

          • They do it to BSD code all the time. They often follow up by finding a copy somewhere in the wild and jumping up and down yelling 'Evil! Evil!' until someone points out that the code is actually BSD code that was included in a GPL project.

            • by silanea (1241518)

              To quote myself:

              [...] Could you kindly point out examples [...]

              So far I have seen only vague accusations.

  • More info (Score:5, Informative)

    by Enry (630) <enry@wayga.FORTRANnet minus language> on Tuesday July 29, 2014 @05:20PM (#47560969) Journal

    http://sel4.systems/FAQ/ [sel4.systems]

    Is it really that hard to give more background information?

    • by lemur3 (997863)

      fuck whoever decided that having a .systems TLD was a good idea.

      it just aint right i tells ya.

      • Handing out TLDs is no more about being proper but giving tools for various fancy names and word plays. Remember to register your .fish domain today.
  • by Anonymous Coward

    What's being released?

    It includes all of the kernel's source code, all the proofs, plus other code and proofs useful for building highly trustworthy systems. All is under standard open-source licensing terms — either GPL version 2, or the 2-clause BSD licence.

    Directly from the website. Not bothered enough to see what bits are BSD 2 Clause though.

  • Don't tell the HURD people -- they'll change which microkernel they're building around, again.

  • Who else thinks that it's only a matter of time before the first vulnerability is found?

    • Knuth said it best (Score:2, Informative)

      by Anonymous Coward

      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.)

      • 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.

  • by ndykman (659315) on Tuesday July 29, 2014 @08:13PM (#47562117)

    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.

  • by manu0601 (2221348) on Tuesday July 29, 2014 @09:31PM (#47562629)

    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.

    • by flux (5274)

      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/ [inria.fr] . Sadly CompCert is not FOSS.

      • 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.

      • Intel x86 systems management mode (SMM). If you can beat the processor into this mode all protected memory is off. You own it all, like DOS/MacOS prior to X.

        This is also the mode that motherboard manufacturers put the CPU in, to hide the fact that they are using the processor to save money on hardware.

        Undocumented OP codes are a bitch.

  • by Half-pint HAL (718102) on Wednesday July 30, 2014 @08:11AM (#47564715)

    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.

    • 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.

Are we running light with overbyte?

Working...