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