seL4 Verified Microkernel Now Open Source 82
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).
Unfortunately? (Score:3)
You mean, fortunately. Now, it's more likely to actually be used.
Re: (Score:2)
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:2)
Party D uses Party A's code, but locks it up a la TiVo.
Party E uses Party C's version instead of Party D's version because Party E gets more rights that way. (Party F, G, H, etc. ad infinitum keep more rights that way, too.... and that's the important part!)
Re: (Score:1)
Party D uses Party A's code, but locks it up a la TiVo.
Party A expressed their opinion about this scenario when they chose the license. GPL v2 Only means they don't want to prevent it.
You may disagree with Party A's choice, but your opinion doesn't matter. Party A wrote the code, and they get to decide.
Re: (Score:2)
Party A expressed their opinion about this scenario when they chose the license. GPL v2 Only means they don't want to prevent it.
Selecting GPLv2 or later ALSO allows for downstream Tivoization of your code. So choosing "GPLv2 only" OR "GPLv2 or later" makes no difference to Tivoization.
The only difference between "GPLv2 only" or "GPLv2 or later" is the or later can be mixed with GPLv3 or later, while GPLv2 only.
So the ONLY statement anyone picking "GPLv2 only" is making, is that they don't want their code
Re: (Score:2)
So the ONLY statement anyone picking "GPLv2 only" is making, is that they don't want their code mixed with GPLv3 which honestly... is pretty silly.
If "GPLv2 only" is silly, then you might want to alert all the Linux kernel developers. After all, the code in the Linux kernel is GPLv2, not GPLv2+.....
Re: (Score:3)
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
Re: (Score:2)
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?
He does care about that because the whole reason he chose the GPLv2 was because it was about "tit for tat", offering up the source in exchange for any modifications to be contributed back. If somebody created a GPLv3-licensed derivative then changes to that could not be contributed back to the GPLv2 kernel. What he cares about is the code, he doesn't care about Tivoization because that has nothing to do with the code and whether or not their changes can be incorporated into the mainline and distributed if d
Re: (Score:2)
Ok, that's a good point.
Re: (Score:2)
Selecting GPLv2 or later ALSO allows for downstream Tivoization of your code.
So don't buy a TiVo then. "Tivoization of your code" is nonsense because Tivoization doesn't have anything to do with the code, in fact you can get the code here [tivo.com] licensed under GPLv2 and use it under those terms just as you would any GPLv2 project.
Re: (Score:2)
So don't buy a TiVo then. "Tivoization of your code" is nonsense because Tivoization doesn't have anything to do with the code, in fact you can get the code here licensed under GPLv2 and use it under those terms just as you would any GPLv2 project.
Read the preamble to the GPLv2 or the philosophy of the FSF. Tivoization is a legal end run around the philosophical purpose the license.
https://www.gnu.org/philosophy... [gnu.org]
"Specifically, free software means users have the four essential freedoms: (0) to run the prog
Re: (Score:2)
Read the preamble to the GPLv2 or the philosophy of the FSF. Tivoization is a legal end run around the philosophical purpose the license.
I have read it, I also understand it. It is nothing to do with the code. If you use the code Tivo provides but you don't own a Tivo then Tivoization has no impact on you because it is nothing to do with the code whatsoever.
Tivoization is a manifestation of "what good is your right to a phone call, if we take away your ability to speak".
Wrong, I don't need a Tivo to use their code.
It was a loophole that was implicitly intended by the GPLv2, but not made explicit. The GPLv3 attempts to close the loophole.
A loophole that clearly many authors wanted and have accepted as "by design". If the GPLv2 license didn't provide then some other license would and authors would be using that instead. Not everybody who uses the GPLv2 (or any FSF license) subsc
Re: (Score:2)
Wrong, I don't need a Tivo to use their code.
That is beside the point. This isn't about *you*.
This is about the 99.99% of people who use Tivo code, use it on a Tivo, and as a result they are denied the particular freedoms the original authors of the code it is licensed under intended for them to have.
Granted 98% of them don't care about the license or about changing the code. But the authors of the original code AND the license cared a great deal about it.
A loophole that clearly many authors wanted and have
Re: (Score:2)
This is about the 99.99% of people who use Tivo code, use it on a Tivo, and as a result they are denied the particular freedoms the original authors of the code it is licensed under intended for them to have.
Wrong, you simply do not understand the license and are implying things that are not there. It has been made very clear multiple times, here [lkml.org] is just one example, that the use of the GPLv2 is purely about code openness and code contribution but not about FSF ideals.
If you believe otherwise then demonstrate where the original Linux kernel author actively intended the recipients of the code to have the freedoms that are not granted by the GPLv2, but you won't because Linus never intended that, it's yet another
Re: (Score:3)
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 b
Re: (Score:3)
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.
Re: (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.
No I said that in this context the use of the GPLv2 is purely about code openness and code contribution but not about FSF ideals, obviously by "this context" I mean Tivo and who used Linux and thus the one using the GPLv2 is Linus. What the authors of the GPL intended is irrelevant, the only thing that matters is what they actually wrote.
Moreover on your request for specific examples of Linus endorsing Tivoization [lkml.org]:
"I think Tivoization is *good*."
"What Tivo did is *good* in my opinion!"
It doesn't get much
Re: (Score:2)
What the authors of the GPL intended is irrelevant, the only thing that matters is what they actually wrote.
Spoken like a true sociopath.
As for Linus' endorsement of tivoization; I've read the thread -- he's satisfied that Tivo followed the rules and contributed the code back. Yes, he writes that "tivoization is good" but that seems strictly within the context of that particular argument about tit-for-tat code especially with someone who was clearly arguing the FSF case, which Linus has repeatedly rebuffed.
Re: (Score:2)
What the authors of the GPL intended is irrelevant, the only thing that matters is what they actually wrote.
Spoken like a true sociopath.
So now you're just resorting to ad hominem attacks because you don't like the facts. We know for a fact that what they intended doesn't matter because they didn't write that and if they did write that the license would have gone beyond simple "tit for tat" and would not have been chosen for the Linux kernel.
As for Linus' endorsement of tivoization; I've read the thread -- he's satisfied that Tivo followed the rules and contributed the code back.
Because as he has made clear many many times that's all that matters, what the authors of the GPLv2 think about that or what you think they intended the license for has no relevance whatsoever.
In any case I remain unconvinced that Linus considered the Tivoization scenario when he selected the license, or that he really consciously desired specifically to enable it.
So? Clearl
Re: (Score:2)
I'm just pointing out that you are acting like a sociopath. A license (contract) is supposed to be a "meeting of minds"; perverting the intention of the contract terms is a sociopathic thing to do. Not ad hominem -- merely an observation.
Because as he has made clear many many times that's all that matters, what the authors of the GPLv2 think about that or what you think they intended the license for has no relevance whatsoever.
To whom?
So? Clearly the authors of the GPLv2 didn't consider it either or they di
Re: (Score:2)
I'm just pointing out that you are acting like a sociopath.
Which is false, by definition.
A license (contract) is supposed to be a "meeting of minds"; perverting the intention of the contract terms is a sociopathic thing to do.
Again, false. Prove to me how tivoization is a perversion of the contract terms. The "meeting of minds" in this case is the author of Linux and the user of Linux, that fact that you think the author of the GPL has anything to do with it demonstrates you have no idea about contracts whatsoever, so don't pretend to be able to discuss them.
To whom?
To whom what? Linus has made it clear to anybody who has bothered to ask or read his posts.
Clearly. If they didn't care theyd' never have released a GPLv3 specifically to close that loop hole in what they wrote vis-a-vis their intent. Oh wait... they did release a GPLv3. Guess they cared.
And that's why it's the GPLv3 and not v2, and you're
Re: (Score:2)
Which is exactly why this does not use V3.
To be secure you really need to have the option to lock down the hardware and only allow updating with signed modules. It is actually part of the FIPS regulations.
Re: (Score:2)
whats the difference between tivoized code and non-tivoized code
Primarily, that the (majority) of users of said code are unable to effectively exercise the rights the GPL was intended to confer upon them.
Specifically, the right to change the code. That they can copy the code to some other deivces, change it, and run it there, but not be allowed to on the original device was not the intent of the GPL, or its author.
Re: (Score:2)
Not at all - by including an "or later" clause you also open your code to being re-licensed under GPLv666: aka the "Stallman is dead and Microsoft now has unrestricted rights to all your code" edition.
Re: (Score:2)
Not at all - by including an "or later" clause you also open your code to being re-licensed under GPLv666
Maybe. It'll still be available under GPLv2 though.
Re: (Score:2)
That is true - but not everyone want to give their code away to whoever happens to hijack the license.
Re: (Score:2)
Party D uses Party A's code, but locks it up a la TiVo.
False, the code is not "locked up", in fact TiVo's modified code is available right here [tivo.com]. If what you mean is that you cannot replace the code running on a TiVo device with your own modified code then say that, because what you said is completely untrue.
Re: (Score:3, Insightful)
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
Re: (Score:2)
You can't choose forever. Once v3 touches it, gone (Score:1)
> 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)
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
contributions on top, etc scare me. Once you know (Score:2)
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
Re: (Score:2)
... 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??!?
Re: (Score:1)
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
Re: (Score:2)
[...] 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.
Re: (Score:2)
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.
Re: (Score:2)
To quote myself:
So far I have seen only vague accusations.
Re: (Score:3)
More info (Score:5, Informative)
http://sel4.systems/FAQ/ [sel4.systems]
Is it really that hard to give more background information?
Re: (Score:2)
fuck whoever decided that having a .systems TLD was a good idea.
it just aint right i tells ya.
Re: (Score:2)
BSD 2 Clause as well (Score:1)
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 HURD (Score:2)
Don't tell the HURD people -- they'll change which microkernel they're building around, again.
Re: (Score:2)
I think they already tried and failed to port to L4, giving up because HURD was too mach-specific.
I like this idea, but (Score:2)
Who else thinks that it's only a matter of time before the first vulnerability is found?
Knuth said it best (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.)
Re: (Score:3)
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 good step forward... (Score:4, 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.
Proof (Score:3)
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.
Re: (Score:3)
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.
Re: (Score:3)
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.
Re: (Score:2)
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.
Re: (Score:2)
Shared Source (Score:1)
What exactly is the point? (Score:3)
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.
Re: (Score:3)
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.