seL4 is the world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement.
This project is a mathematically-verified bug-free microkernel system that supports x86 and ARM, and aims to be general-purpose.
Website:
sel4.systems
Whitepaper:
sel4.systems
Genode OS, an OS framework that supports seL4 and other kernels:
genode.org
seL4 is already being used and researched by the military for avionics and helmet displays.
Other urls found in this thread:
qualcomm.com
cavium.com
wiki.sel4.systems
genode.org
rumpkernel.org
hack.org
genode.org
genode.org
genode.org
fixup.fi
pcworld.com
gnu.org
twitter.com
Daily reminder that formal verification only proves the relationship of a model to an implementation and that it is not proof that the model has anything to do with reality / accurately deals with threats.
it doesn't have any proofs for x86 you fucking shill fuck off. you've been posting this all day on g too.
yeah.. ok
x86 is so fucking complicated if they could not possibly model it correctly. The "proof" would be meaningless.
There was actually already a bug in one of the unverified parts that had to be fixed. It's still a good choice if you need it but if you post here you don't.
...
Is it webscale?
wat
wiki.sel4.systems
TL;DR: They mathematically verify that there's no buffer overflows, null pointer exceptions, etc, ensure that the binary is correctly compiled (immune to the theoretical Ken Thompson Hack), and are far more thorough with their verification process than any other general-purpose OS kernel.
wrong. RISC-V is the future
Good point.
but ARM is the immediate future
also, even if RISC-V does surpass ARM at some point, and seL4 does not get a port to it, Genode OS will still be important, as a set of drivers and utilities that can be used across multiple microkernels.
genode.org
Will Hurd use this now?
I think I remember seeing something about them considering it, but seeing as how HURD moves at a snail's pace, who knows what they'll end up doing
Nobody in the Hurd team is actively working on porting Hurd to L4. They've done evaluations in the past and decided they'd rather continue with Mach.
HURD is a piece of nearly-abandoned trash at this point. I have no idea why anyone cares about it
I love the potential of the Hurd. The flexibility of the Mach translator system is unparalleled to any system we have today. If your hardware is supported, then you can actually run Hurd today in the command line and with difficulty through Gnome 3. What they're doing at the moment is implementing a rump kernel* so that Hurd can finally get more drivers working than the ancient drivers that exist.
The HURD is never going to be released using Mach, much less anything else, but the paradigm of microkernel+dmd+guix is pretty awesome.
GNU DMD has been renamed to GNU Shepherd.
What a hack. The Unix Hater was right.
Just begging for a Trump Kernel fork
If you haven't tried the new 2018.02 release of Genode it's actually really cool. There's almost complete hardware support for various Thinkpads, including a work-in-progress 3D driver for Intel iGPUs. The Genode package binaries themselves are identical across microkernels now, so once a driver works on NOVA or base-hw it'll work on seL4.
genode.org
genode.org
genode.org
I think this makes a lot of sense. Everything used to be usable with less code. Drivers are more bloated now even though the hardware does a lot more work and could present a simpler interface to the computer.
you stupid neckbeard wannabes are so dense you think some type of backdoor has to be called a "Ken Thompson Hack" because you're too stupid to realize where backdoors can exist until some famous guy says explains it for you
not sure whether
or
Genode uses rump kernel versions of Linux, OpenBSD, and NetBSD for much of its driver support.
The author forgets how staggeringly incompetent OEMs are, and fails to recognize the added ability for (((software differentiation))) of products. Keeping drivers on the main CPU is entirely worth it for kneecapping peripheral manufacturers' ability to do chinky/kikey bullshit alone.
By the time RISC-V is matured, no normie will even want to own a general-purpose computing device anymore, they'll be perfectly happy with botnet terminal devices. Heck, those botnet terminal devices will come built-in with anything else anyway as part of the """internet or things""", so worrying about even that will be completely superfluous. Actual computing will be restricted to the military, gubmint, and biggest corporations who operate """cloud""".
Has this anything at all to do with SELoonix (aka _NSAKEYLoonix)?
No
Microkernels written in C aren't a solution. I wouldn't want to use seL4 because it doesn't improve the user's quality of life. On a Lisp machine, Go and scripting languages would do everything worse than the OS already does, so there's no point. On UNIX, Go and scripting languages are huge projects with a ton of code because the only common language is C and everything else has to be done from scratch. Besides making things a lot easier, Lisp machines improved the quality of languages too. Fortran and Pascal on Lisp machines had bignum integers and used the same arrays and functions as Lisp so you didn't need an FFI. The machine had bounds checking, so there were no buffer overflows, and you could change the code and data and continue whenever there was an error. Multics had that kind of debugging too.
Try the case where the interpreter specified on the #! line is *itself* implemented by an interpreted script. Now if a reasonable person were implementing this, it would just work. Recursion is a concept understood by most 18-year-old CS majors. Apparently this notion escaped the notice of the BSD/SunOS guys, because on my Unix, one level is all you get.You Just Don't Understand. Writing Code To Run InsideKernels Is A Hard Problem. (That's why we havemicrokernels; so you can have programmers of average abilitywriting system software and not necessarily crashingeverything when it breaks.) You can't just allow unboundedrecursion inside the Kernel. You might overflow your Kernelstack which is of course set at some small wired in constantin keeping with unix tradition (Simple!). And of course, NoOne Would Ever Want To Specify Another Shell Script In The#! Line.I have a machine named EXXON-VALDEZ on my desk. This wasfrom when I nominally worked in fault tolerant computing; Ifigured it would be good karma to name the machine after ahuge disaster as a precautionary measure. (I'm quitesuperstitious in strange ways.) Now the hardware has beenreplaced and I'm about to name the machine something else.I'm thinking of the name MBUF. I suppose it wouldn't besuch a big change; the machine would still be named after ahuge disaster...
Lisp machines turned out to be such a catastrophic dead end that quarter century old quips from the Unix Haters' Handbook are still the most recent complaints they have, even if most of the problems expressed in ugh.pdf were fixed by GNU/Linux and the BSDs later.
Keep dreaming denialist
No normie will ever using it
Stop caring about what normalfags do. The only thing they are good at is ruining things that are actually good.
Normalfags do what the corporations want them to, if that is RISCV in consumer produts so it shall be, almost all of them will not even know it.
PC OEMs are already looking into RISCV for better microcontrollers and peripheral chips. Windows and ESXi keep them tied to x86 CPUs for the foreseeable future.
They will never use arm laptops either, o wait chromebooks are a thing.
Are they?
Is anyone except for shitty public schools really using them?
I know tons of rando normies that use chromebooks, most of them are college students.
Chromebooks are actually one of the most secure laptops on the market. It's sad that from that secure device, they require you to run Botnet OS.
Reminder that it's BSD-licensed so no freedoms whatsoever.
It's funny that 20 years later, the threat of browsers reducing Windows to a poorly debugged set of device drivers was true... but then Linux existed with the ability to write or improve your own device drivers, so that got used as the base for ChromeOS instead.
meme machine
Atleast it has more freedom than GPL
Ah yes, the freedom to restrict freedom. Reminder that your freedom ends where someone else's freedom starts.
So is anyone actually using Genode? Security is nice and all, but so is usability. What problems are there for you? In what ways is the experience more or less enjoyable than GNU/Linux or *BSD? Do the repos come with everything you need? Or do you have to rely on Linux jails for most things?
Which is why no one else has a right to source code
freedom ain't free
the tree of liberty and freedom gotta be littered with the blood of Patriots
If I have 10 apples, and I give you 1 apple, I have not infringed on any of your freedom.
Huh strange, is that not like the gpl restricting my freedom to use a license of my choice?
No, but it is using intellectual property laws to restrict the freedoms of others.
Why are you so dense?
It's not okay for the GPL to restrict your freedom
for your own safety and the safety of others do not question vital licensing apparatus
Why are you shilling it if its not ok? I have already stated how it restricts your freedom, and what I mentioned isn't the only way it does.
Did you not read the fucking text
Its NOT okay that the GPL restricts your freedom
this thread is about seL4
...
I'm not sure I am following these replies the same way you are, but thats fine since the same conclusion was reached in the end.
In the ideal world, BSD is the ideal license. In this world, GPL is the only viable license.
If I have 10 apples, and I give you 1 apple, I have not infringed on any of your freedom.
If I give you one apple and tell you I'll sue you if you bake it into a pie, I have infringed on your freedom.
Right so having that apple that you can now eat is somehow less free than not have an apple.
Lolberts? On my board? It's more likely than you think.
A simple-minded right-wing ideology ideally suited to those unable or unwilling to see past their own sociopathic self-regard.
...
...
How Owners Justify Their Power
Those who benefit from the current system where programs are property offer two arguments in support of their claims to own programs: the emotional argument and the economic argument.
The emotional argument goes like this: “I put my sweat, my heart, my soul into this program. It comes from me, it's mine!”
This argument does not require serious refutation. The feeling of attachment is one that programmers can cultivate when it suits them; it is not inevitable. Consider, for example, how willingly the same programmers usually sign over all rights to a large corporation for a salary; the emotional attachment mysteriously vanishes. By contrast, consider the great artists and artisans of medieval times, who didn't even sign their names to their work. To them, the name of the artist was not important. What mattered was that the work was done—and the purpose it would serve. This view prevailed for hundreds of years.
The economic argument goes like this: “I want to get rich (usually described inaccurately as ‘making a living’), and if you don't allow me to get rich by programming, then I won't program. Everyone else is like me, so nobody will ever program. And then you'll be stuck with no programs at all!” This threat is usually veiled as friendly advice from the wise.
I'll explain later why this threat is a bluff. First I want to address an implicit assumption that is more visible in another formulation of the argument.
This formulation starts by comparing the social utility of a proprietary program with that of no program, and then concludes that proprietary software development is, on the whole, beneficial, and should be encouraged. The fallacy here is in comparing only two outcomes—proprietary software versus no software—and assuming there are no other possibilities.
Given a system of software copyright, software development is usually linked with the existence of an owner who controls the software's use. As long as this linkage exists, we are often faced with the choice of proprietary software or none. However, this linkage is not inherent or inevitable; it is a consequence of the specific social/legal policy decision that we are questioning: the decision to have owners. To formulate the choice as between proprietary software versus no software is begging the question.
Developers should have no intellectual property rights. Which is why GPL is immoral. If a developer only wants to give away a binary though, you have no right to demand anything else from them.
In an ideal world I would not care, because users would reject proprietary software so he can give out all the binaries he wants, nobody would use them. However in reality I want it to be as inconvenient as possible, because users are ignorant and the greedy developers know this and actively subvert the Free Software movement with Open Source (TM) to keep them that way in order to enrich themselves from the resulting power asymnetry.
Genode isn't ready for anyone who's not familiar with the source code and build process yet. Wait for the August or November release.
Or they don't actually care if they are tracked because in almost every other way the software is superior
I expect it is stallmans faultHis lunacy makes
the others want to overthrow the Hurd Reich
Genode has a Quake package now.
I personally believe distributing binaries is immoral. You are giving someone else an obfuscated mess that humans can not understand.
it has no proofs for x86
google botnet garbage is the future?
I don't know how my car works, still glad to have it. Between a car I cant understand and no car I am more free with the car.
Never trust anything that comes from Germany.
The metaphor would be if your car did not come with a owner's / repair manual.
All these metaphors are just meant to distract you from what matters. They are all wrong, cars are not artificially obfuscated and you could not build your own car from the materials and instruction, while everyone can compile the binary from the source on their pc. They are artificial restrictions to effectively continue owning something after you sold it, even multiple times. This is what libertarians want, the freedom to enslave you.
fine by me. we need to get off x86 ASAP
The point is exactly the same if it comes without them
Yea giving you an apple with an agreement you won't bake it into a pie is enslaving you. Sure fucking thing.
BSD cucks blown the fuck out yet again.
but one is secure and the other is not (BSD wins again)
Okay, I'll continue with your analogy. Let's say one of the belts in the engine snapped. If the car was like a binary, you would need to tell the manufacture of the car of the problem and then they consider shipping you out a new working engine. If the car was like the source, you could just replace the belt. Let's say you aren't knowledgeable about cars though. You can take your car to a mechanic to do it for you. You pay him for his time and you are off on your way.
With a binary, you are entirely dependent on the developers to make any changes to it. With source you can make changes that you see fit. If you do not know about the changes you can take them to a programmer to have him do it for you. You pay him for his time and you are off on your way.
seL4 is just a microkernel. It doesn't do much of anything. Genode is actively secure despite being a much larger system, and works better on its own kernel or NOVA than on seL4.
Which are not proven secure :^}
Well that fucking sucks, but the car was free so I now I am in the same position as before.
Neither is seL4 on x86, or even on ARM with an MMU.
...
The ONLY scenario that's verified is single core ARMv7 with the MMU turned off, so yes.
Good enough for vi, and lynx
Isn't ARM cucked?
way less than x86, but still kinda cucked (not totally free like RISC-V)