back to reddit friend
SeL4 gets formal verification on x64
Liam White
Jonathan Morales
do you mean the blobs would be unprivileged and can't access side channels, or are you just retarded?
Joseph Bell
Why? What's so wrong about the BSD systems?
Bentley Foster
You really have to go back you half chan POS.
Levi Lopez
BLOBs can be constructed such that they can be proven to only do certain things without access to the source code.
Lincoln Davis
They don't do it because of the 60 million line problem.
openhub.net
openhub.net
openhub.net
openhub.net
openhub.net
First of all, memory for PCs (and soon for workstations)runs for about $30/MB, and 8 additional MB take care of bothX and GNU Emacs.In addition, I won't say much about X, which I dislike,although if I'm not mistaken most of the bloat has occurredbecause of vendor requests. X 10 was much leaner, andprovided more than sufficient functionality as far as I'mconcerned.With respect to Emacs, may I remind you that the originalversion ran on ITS on a PDP-10, whose address space was 1moby, i.e. 256 thousand 36-bit words (that's a little over 1Mbyte). It had plenty of space to contain many large files,and the actual program was a not-too-large fraction of thatspace.
Juan Adams
The main attraction of seL4 is the strict isolation of programs it provides, the kernel is formally proven to only allow programs to access memory regions they have been allocated (either memory allocated specifically for that program or memory allocated as a shared buffer between it and another program).
Say you have two programs and a DMA capable peripheral device
You also have four memory regions managed by seL4
The IOMMU on the processor is configured to not allow C to access anything other than 3, from the perspective of C the only memory in the system is 3.
When A wants to have C display something it writes data to the shared memory region 3 and informs B that there is something to display. B then looks at the data in 3 and informs C what it needs to do by sending a message to it by writing to 4. C, having received instructions from B, uses its DMA engines to access 3 and copy the data to itself and then do what it needs to do to display what A wanted on the screen.
Why it doesn't matter if B is a binary blob is because it has no privileges, unlike with monolithic and hybrid kernel architectures which have device drivers run in privileged mode (and can therefore access any region of memory it wishes) it can only access what it needs in order to perform its task of controlling the GPU. To complement this the IOMMU is setup to only allow C to access the memory it needs, B can't use the DMA engines of C to bypass the restrictions imposed on it by seL4 (this isn't something which is practical in monolithic and hybrid kernel architectures).
And whats really frustrating with the Linux kernel is that much of that code is there to provide backwards compatibility to hardware and software from 20 years ago, there is also code bloat because its all written in C rather than languages which have native support for things like OO. If a group of developers were to rewite Linux in C++ and only support current generation hardware then I suspect the result would be somewhere around 4 million lines of code.
Gavin Kelly
install gentoo
Joseph Green
I guess counting 20 years as "recent" is very convenient, so you can pretend Linux is a recent project and still hope it will go somewhere.
And what ivory tower devs fail to see is the repercussion of breaking backwards compatibility: people lose the reasons they had to use your stuff.
And this is why you'll never accomplish anything.
Landon Perez
Breaking backwards compatibility isn't a big problem for those of us who believe in software freedom. Whatever a developer chooses for a specific program, the user will always have the freedom to change it to fit as required for the user.