Slashdot Mirror
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).
You mean, fortunately. Now, it's more likely to actually be used.
sig: sauer
http://sel4.systems/FAQ/
Is it really that hard to give more background information?
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.
In humans, defecation may occur (depending on the individual and the circumstances) from once every two or three days to several times a day. Extensive hardening of the feces may cause prolonged interruption in the routine and is called constipation.
Human fecal matter varies significantly in appearance, depending on diet and health. Normally it is semisolid, with a mucus coating. Its brown coloration comes from a combination of bile and bilirubin, which comes from dead red blood cells.
In newborn babies, fecal matter is initially yellow/green after the meconium. This coloration comes from the presence of bile alone. In time, as the body starts expelling bilirubin from dead red blood cells, it acquires its familiar brown appearance, unless the baby is breast feeding, in which case it remains soft, pale yellowish, and not completely malodorous until the baby begins to eat significant amounts of other food.
Throughout the life of an ordinary human, one may experience many types of feces. A "green" stool is from rapid transit of feces through the intestines (or the consumption of certain blue or green food dyes in quantity), and "clay-like" appearance to the feces is the result of a lack of bilirubin.
Bile overload is very rare, and not a health threat. Problems as simple as serious diarrhea can cause blood in one's stool. Black stools caused by blood usually indicate a problem in the intestines (the black is digested blood), whereas red streaks of blood in stool are usually caused by bleeding in the rectum or anus.
Food may sometimes make an appearance in the feces. Common undigested foods found in human feces are seeds, nuts, corn and beans, mainly because of their high dietary fiber content. Beets may turn feces different hues of red. Artificial food coloring in some processed foods such as highly colorful packaged breakfast cereals can also cause unusual feces coloring if eaten in sufficient quantities.
Clinical laboratory examination of feces, usually termed as stool examination or stool test, is done for the sake of diagnosis, for example, to detect presence of parasites such as pinworms and/or their eggs (ova) or to detect disease spreading bacteria. A stool culture — the controlled growth of microbial organisms in culture media under laboratory conditions — is sometimes performed to identify specific pathogens in stool. The stool guaiac test (or guaiac fecal occult blood test) is done to detect the presence of blood in stool that is not apparent to the unaided eye. Fecal bacteriotherapy — also known as a fecal transplant — is a medical procedure wherein fecal bacteria are transplanted from a healthy individual into a patient.
Human feces collected for a specific practical use, such as for fertilizer, is known as night soil.
The distinctive odor of feces is due to bacterial action. Gut flora produce compounds such as indole, skatole, and thiols (sulfur-containing compounds), as well as the inorganic gas hydrogen sulfide. These are the same compounds that are responsible for the odor of flatulence. Consumption of foods with spices may result in the spices being undigested and adding to the odor of feces. The perceived bad odor of feces has been hypothesized to be a deterrent for humans, as consuming or touching it may result in sickness or infection. Human perception of the odor may be contrasted by a non-human animal's perception of it; for example, an animal that eats feces may be attracted to its odor.
Feces elicits varying degrees of disgust — one of the basic human emotions — in all human cultures. Disgust is experienced primarily in relation to the sense of taste (either perceived or imagined), and secondarily to anything which causes a similar feeling by sense of smell, touch, or vision. As such, human feces is regarded as something to be avoided diligently: expelled in private and disposed of immediately and without trace. It is often considered an unacceptable topic in polite conversat
Wait for them to f**k with it until they can reconnoiter anything on L4 systems. My money is on a bunch of wholly useless features which will be added in the next few months.
"World's First Formally-Proven OS Kernel" running on completely unverified hardware.
Close to useless.
> 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 the entire project be released _only_ as GPL3. It can no longer be used under GPL2.
The reason for that is that the new contribution that is GPL3 licensed wasn't licensed under GPL2. Since that bit isn't licensed under 2, the whole package can't be distributed under 2.
The wording in GPL3 is unclear in such a way that it could pose a very significant risk to people who aren't even remotely involved in open source at all. Whether that wording is merely stupid or devious, who knows. The problem was pointed out before the license was approved, and the wording wasn't changed, so perhaps Stallman actually did intend to leave the threat there, while claiming the threat didn't exist.
Don't tell the HURD people -- they'll change which microkernel they're building around, again.
"They redundantly repeated themselves over and over again incessantly without end ad infinitum" -- ibid.
Who else thinks that it's only a matter of time before the first vulnerability is found?
A fool and his hard drive are soon parted.
whats the difference between tivoized code and non-tivoized code? i read the page on tivoization and it doesnt seem to make any difference in terms of the code.
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.)
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.
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.
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.
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.
So, this is basically shared source.
Making something explicitly GPLv2, when that license has known problems that have been fixed in GPLv3, is a clear hint that someone has an agenda.
Take a look at the differences:
1. Tivoization. A possible loop hole (that was never tested in court) allows people to lock the binary away behind a signature, even though the GPLv2 explicitly requires everything needed to build the binary. So, the company behind this wants to sell it in closed devices? Nope, the copyright owner can do anything, including putting the same code under different licenses. They wouldn't need this.
2. Patents. GPLv3 requires that you give the license to any patents along with the code. If you have the code, but no patent license, you can look at the code all you want, but you cannot distribute it without a patent license. Basically what you get in this case is Shared Source, as Microsoft called their "read-only open source" idea.
With this trap, nope, I won't be touching this.
Now, some might be thinking "but doesn't that mean you won't be using Linux"? Nope, that's a different case. While the dangers of GPLv2 is still there, it was not deliberately chosen to allow Linus to patent the thing. It was chosen because we didn't have anything better at the time. When the GPLv3 was created, Linux included code from thousands of people, and changing the license had become impossible. It's stuck there. Yes, they could have chosen "or any later version" from the start, but that does have its own problems. That would basically allow the FSF to change the license. Imagine the FSF being bought out by Apple... Suddenly the GPLvX would state "all rights reserved Apple Corp". So, Linux is GPLv2 because its stuck there, not for some nefarious reasons.
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'
nice troll, too bad nobody is biting :( Slashdot has really gone down hill.
Copyright (c) 1990 - 2014 Dice. All rights reserved. Use of this comment is subject to certain Terms and Conditions.
What a SCHEISS-Kommentar. They have done 50% of work and you bitch they did not 100% of the work. Like "they only brought me a wife, now I have to spend lots of effort to inseminate, boohooo".