seL4 Verified Microkernel Now Open Source

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

Comments

Unfortunately?

[ichthus]

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

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

Re:Unfortunately?

[Urkki]

(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:Unfortunately?

[mrchaotica]

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:Unfortunately?

[Anonymous Coward]

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:Unfortunately?

[tlhIngan]

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.

Re:Unfortunately?

[mx b]

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"?

Re:Unfortunately?

[vux984]

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 mixed with GPLv3 which honestly... is pretty silly.

Re:Unfortunately?

[jcochran]

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:Unfortunately?

[exomondo]

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. 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:Unfortunately?

[exomondo]

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 licensed under GPLv2 and use it under those terms just as you would any GPLv2 project.

Re:Unfortunately?

[vux984]

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.

Re:Unfortunately?

[vux984]

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

"Specifically, free software means users have the four essential freedoms: (0) to run the program, (1) to study and change the program in source code form, (2) to redistribute exact copies, and (3) to distribute modified versions."

Tivoization of GPL code preserves those 4 rights, but withholds the implicit desire of GPL users to be able to exercise those rights on the hardware the software is running on.

Tivoization is a manifestation of "what good is your right to a phone call, if we take away your ability to speak".

When the GPL2 was written no one had conceived that you might receive GPL code installed on a device, be allowed to run it, be allowed to change it, be allowed to redistribute it... but NOT be allowed to run the changed software on the original device.

It was a loophole that was implicitly intended by the GPLv2, but not made explicit. The GPLv3 attempts to close the loophole.

And as an aside, the AGPL3 is mean to meant to close another loophole that wasn't originally conceived of... developers would use GPL code, and distribute only access to the code running remotely rather than copies of the code itself, thereby exempting them from the need to share the source.

Re:Unfortunately?

[Immerman]

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:Unfortunately?

[exomondo]

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) subscribes to the FSF ideology, in fact some of the most prominent ones (Linux for example) explicitly do not.

Re:Unfortunately?

[ichthus]

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.

Re:Unfortunately?

[exomondo]

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

Re:Unfortunately?

[DeVilla]

... 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:Unfortunately?

[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 nature and breaks if changed, eg libpng/zlib should be using a zlib or bsd style license that stipulates you can take the source, but you can't release anything misrepresenting. eg I can't take zlib, compile it, and call it "myzlib, pay me 20$ to use", now if I make changes to it that alter the functionality, I can't call it zlib, nor can I redistribute the source code under a new license, stripping all the previous license data out.)
  WHICH BY THE WAY, GPL-FREEDOMITES TEND TO DO... "hey look this file doesn't have a license, let's GPL it"
b) consider the political statement that is made by picking that license. 90% of the time, you don't want the GPL unless you philosophically agree with it. The remaining 10% of the time you want the GPL because you know other people are going to rip off the project, and if they're going to rip it off, they better share what they do with it.

In the case of things like the iPhone development where the GPL basically prevents you from using the software entirely, yes, you are totally shooting yourself in the foot by picking the GPL.

In most cases, people don't care what the license is, and aren't going to use it as a battering ram against someone unless that person has their hand too deep into the cookie jar. Case in point libvorbis is better off as a BSD license because it would encourage adoption, while FFMPEG is better off as GPL/LGPL to prevent people from ripping off the code and putting it in their own projects. There are several hundred software units out there that do "convert to flash" or "convert to h264" and most of them just straight compile ffmpeg and pipe it using a bridge library so they never have to show the source code of their software.

The point of a software license is to explicitly control what users do with it, and if that license is too tightly enforced, you hinder adoption, hence how Oracle has pretty much destroyed any chance in hell of Java being useful since JDK1.4, and that started with Microsoft. Anyone who adopts Java, has no gaurantee their software will work in the next version, hence why I said it's a poor choice now. Microsoft on the other hand embraced the Mono project and thus we have a useable language that can be compiled to native code on all platforms.

Where you probably want to avoid the GPL is with drivers. Yes it might be useful to be GPL, if the hardware is dead/dying, but a lot of vendors need to keep their cards close to their chests, otherwise they will leak hardware specifics that competitors can use.

Re:Unfortunately?

[vux984]

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:Unfortunately?

[vux984]

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 accepted as "by design".

Absolutlely not an outcome the authors of the license wanted. And I'm skeptical you can find any developers who expressly WANTED the GPL for tivoization... i mean if you want that, then use the BSD or something. There are lots of perfectly suitable licenses for that use.

What realistic scenario can you put forth where the developer actively wants to license their code under the GPL and simultaneously doesn't want people to be able to modify the code they received to run on on the equipment the code is installed on?

Seriously. Find one.

And no, Tivo itself doesn't count, they didn't author original code and actively select the GPL... they merely took the GPL code that was out there because it was out there and used it, and ran a legal end run around the authors intentions.

Not everybody who uses the GPLv2 (or any FSF license) subscribes to the FSF ideology,

There does have to be a fairly substantial overlap with FSF ideology though, otherwise you'd pick something else, like BSD.

in fact some of the most prominent ones (Linux for example) explicitly do not.

By "Linux" I assume you mean Linus? And while its clear he disagrees with the FSF on some key points, you'd be hard pressed to demonstrate that he actively approves of Tivoization. At best I'd say he doesn't like the GPLv3's method of trying to prevent it. But I could be mistaken. I'm not Linus.

Re:Unfortunately?

[vux984]

Ok, that's a good point.

Re:Unfortunately?

[exomondo]

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 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 false inference you are making.

Absolutlely not an outcome the authors of the license wanted.

The authors of code that use it.

i mean if you want that, then use the BSD or something.

So not only do you not understand the GPL license but you also don't understand the BSD license. The BSD license does not require code contributions back, it does not require you to release your modifications like the GPL does. That is why the GPL was chosen over the BSD for the Linux kernel.

What realistic scenario can you put forth where the developer actively wants to license their code under the GPL and simultaneously doesn't want people to be able to modify the code they received to run on on the equipment the code is installed on?

The Linux kernel! Explicitly does not care about FSF freedom ideals and only cares about the code, that's why they use the GPLv2 and why the GPLv3 is incompatible with the ideals of the kernel developers.

By "Linux" I assume you mean Linus? And while its clear he disagrees with the FSF on some key points, you'd be hard pressed to demonstrate that he actively approves of Tivoization.

Tivoization is fine according to Linus because it is about source code and not anything else:
I personally have always been very clear about this: Linux is "Open Source". It was never a FSF project, and it was always about giving source code back and keeping it open, not about anything else.

Re:Unfortunately?

[DamnOregonian]

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.

Re:Unfortunately?

[vux984]

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:Unfortunately?

[exomondo]

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:
"I think Tivoization is *good*."
"What Tivo did is *good* in my opinion!"

It doesn't get much more unequivocal than that, he does actively approve of Tivoization.

Re:Unfortunately?

[vux984]

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.

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.

My read on it that his take on it is ragmatic, that it's happened, that it hasn't been "bad for the linux kernel", and that gplv3 is a worse "solution".

Re:Unfortunately?

[LWATCDR]

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:Unfortunately?

[silanea]

[...] 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:Unfortunately?

[Immerman]

That is true - but not everyone want to give their code away to whoever happens to hijack the license.

Re:Unfortunately?

[HornWumpus]

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:Unfortunately?

[exomondo]

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? Clearly the authors of the GPLv2 didn't consider it either or they didn't care about Tivoization at all. The license did explicitly what Linus wanted and nothing more, if the license explicitly placed restrictions on the use of the code outside of contributing it back then the GPLv2 would not have been used because Linus has made clear many times that it is about "tit for tat" and nothing more.

So what I'm trying to understand now is what your point is? We know "tivoization of code" is a misnomer and makes no sense because tivoization has nothing to do with the code, we know that Linus approves of Tivoization and we know that any project that doesn't can switch to GPLv3 to prevent it. So what is your point?

Re:Unfortunately?

[vux984]

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 didn't care about Tivoization at all.

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.

if the license explicitly placed restrictions on the use of the code outside of contributing it back then the GPLv2 would not have been used because Linus has made clear many times that it is about "tit for tat" and nothing more.

Its impossible to say what Linus would have done at 22 years old in 1992 if the GPL had been slightly differently worded. Whether he'd have cared about an anti-tivoization clause at the time... you'll maybe recall that Linux 0.01 through 0.11 was released under a license that forbade commercial use in 1991.

He switched to the GPL in 1992. Your indulging in some serious mythologizing to even suggest he had such an extremely nuanced understanding and appreciation for a license that had only been around for a couple years. (GPL v1 was released in 89), and GPLv2 was barely 6 months old when Linus adopted it.

You are saying the same person that you argue thought tivoization was a good thing when he selected GPL was against any commercial use at all just a few months earlier? That doesn't add up. Unless maybe, just maybe Linus' stance on the license has evolved and become a lot more nuanced over the last 20+ years.

So what is your point?

1) That Linus in 2007 isn't really the same kid that picked GPLv2 for his experimental kernel project in 1992.

2) That Linus in 1992 wasn't really making pro-tivoization arguments in 1992 when he selected that license.

Re:Unfortunately?

[exomondo]

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 free to use v3 if you want in your software, v2 is used for the kernel whether you like it or not.

Its impossible to say what Linus would have done at 22 years old in 1992 if the GPL had been slightly differently worded.

If it were v3 it would not have been "tit for tat" and by definition would not have fit Linus' principles.

You are saying the same person that you argue thought tivoization was a good thing when he selected GPL was against any commercial use at all just a few months earlier? That doesn't add up.

Now you've gone full retard, he made the change because he wanted to change, if he didn't want commercial use then he wouldn't have selected the GPLv2.

1) That Linus in 2007 isn't really the same kid that picked GPLv2 for his experimental kernel project in 1992.

Which is obvious and irrelevant, it makes no difference to anything whatsoever.

2) That Linus in 1992 wasn't really making pro-tivoization arguments in 1992 when he selected that license.

Tivo didn't even exist then so you're just stating the obvious.

Ultimately you have no point, don't understand the GPL, don't understand what a contract is and instead of getting educated you decide to call me a sociopath as an excuse for your own mental limitations.

The GPLv2 exists to protect the 4 freedoms, that is its goal, if you think it is supposed to do more then you just fail to understand it.

Re:Unfortunately?

[silanea]

To quote myself:

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

So far I have seen only vague accusations.

More info

[Enry]

http://sel4.systems/FAQ/

Is it really that hard to give more background information?

Re:More info

[lemur3]

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

it just aint right i tells ya.

Re:More info

[jones_supa]

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.

BSD 2 Clause as well

[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 HURD

[Carnildo]

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

Re:Don't tell HURD

[ChunderDownunder]

I think they already tried and failed to port to L4, giving up because HURD was too mach-specific.

I like this idea, but

[Beck_Neard]

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

Knuth said it best

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

Re:Knuth said it best

[Beck_Neard]

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

[ndykman]

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.

Re:You can't choose forever. Once v3 touches it, g

[Immerman]

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

Proof

[manu0601]

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:Proof

[flux]

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.

Re:Proof

[jones_supa]

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:Proof

[HornWumpus]

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.

contributions on top, etc scare me. Once you know

[raymorris]

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 scratch, they start by making a copy of the existing authentication module and replacing the "guts", the actual authentication function, with some other type. That second authentication module would be a derivative work of the first, and therefore gpl3. The project maintainers have no way of knowing how the author went about writing it, though, so they don't know if it's gpl3 or not.

My primary 8-5 job is maintaining and enhancing a gpl3 project called Moodle. I appreciate what the licence APPEARS to say, but I'm always nervous about what it DOES say. I'm careful to only contribute or distribute under my personal name, never hosting a copy of the source on my employer's servers. When I get an email at work asking for a copy of a module I wrote, or some help with something, I reply from my personal email address in order to protect my employers IP by avoiding any indication that the organization is distributing. Even with that, I also have to watch the entire project for anything that might infringe on my personally held UP because if someone puts infringing code on the project github I'll arguably lose my rights.

Re:whats the difference?

[vux984]

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.

What exactly is the point?

[Half-pint HAL]

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:What exactly is the point?

[mr_mischief]

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.

Re:Shared Source

[Half-pint HAL]

A trap? Not really. From the developer's point of view, they'll still be able to get access to any changes to code on their terms, even if it is "tivoised". They can incorporate them into their code base without worrying too much about which hardware devices will or won't work - Somebody Else's Problem. They're interested in the code, not in "right to do whatever you want with your devices."

Shared Source

[slashdice]

nice troll, too bad nobody is biting :( Slashdot has really gone down hill.