Aw: Re: Re: Re: Re: seL4 is open source now

This is merely a historical archive of years 2008-2021, before the migration to mailman3.

A maintained and still updated list archive can be found at https://lists.osmocom.org/hyperkitty/list/baseband-devel@lists.osmocom.org/.

mark.neuhaus at email.de mark.neuhaus at email.de
Tue Aug 5 09:17:21 UTC 2014


The kernel comes with a hypervisor (under BSD on Githu, too) 
and you can run Linux in one virtual environment 
(see http://l4linux.org/) and for example an GSM stack in 
another virtual environment. So you can think of that kernel
as a kind of virtual machine that seperates the hardware  

This way all virtual systems are prooven separated and I think 
that is what the merkel-phone does.

owever NICTA is actually going much further. Thei are working 
on a zero-bug (verified file system) and much more.

This kind of programming is entirely different from common
way to write a program. (YOU don't write the program, but you
write a proof in Coq or ISABEL ect and from this proof a 
programm can be derived automatically)  

 

> Gesendet: Dienstag, 05. August 2014 um 10:50 Uhr
> Von: "Sebastien Lorquet" <sebastien at lorquet.fr>
> An: mark.neuhaus at email.de
> Betreff: Re: Aw: Re:  Re:  Re: seL4 is open source now
>
> Hello,
> 
> Reading through the se4l FAQ at http://sel4.systems/FAQ/ , I'm reading this:
> 
> 
> Unique about seL4 is its unprecedented degree of assurance, achieved through
> formal verification. Specifically, the ARM version of seL4 is the first (and
> still only) general-purpose OS kernel with a full code-level functional
> correctness proof, meaning a mathematical proof that the implementation (written
> in C) adheres to its specification. In short, the implementation is proved to be
> bug-free (see below). This also implies a number of other properties, such as
> freedom from buffer overflows, null pointer exceptions, use-after-free, etc.
> 
> 
> Okay with that. But also:
> 
> 
> There is a further proof that the binary code which executes on the hardware is
> a correct translation of the C code. This means that the compiler does not have
> to be trusted, and extends the functional correctness property to the binary.
> 
> 
> So that is very cool, even the binary result is proved, not only the source code !
> 
> The only thing that bothers me is: what can I do with this cool software? It
> seems that little can be done without a set of userspace servers, so I guess we
> have to wait until some open source community provides useful software to run
> with this microkernel.
> 
> Best regards,
> 
> Sébastien Lorquet
> 
> Le 02/08/2014 12:49, mark.neuhaus at email.de a écrit :
> > 
> >> My idea is that at some point, the developers working at xda-developers
> >> (android phone hackers) will get enough knowledge of their baseband
> >> chips so that something can be done with osmocom. But this is only my
> >> opinion!
> > 
> > Yes lets hope. The calypso is just to outdated to be interesting
> > for anything 'useable' beyond pure hacking-fun.
> > 
>




More information about the baseband-devel mailing list