[Cryptography] Security proofs prove non-failproof

[Perry E. Metzger]

On Mon, 20 Feb 2017 14:26:38 +0000
Peter Gutmann <pgut001 at cs.auckland.ac.nz> wrote:

> Perry E. Metzger <perry at piermont.com> writes:
> 
> >seL4 is used in millions of baseband controllers in mobile phones
> >(to name one example) but I'll agree that overall, penetration of
> >these tools isn't so great *yet* compared to everything else out
> >there.  
> 
> I thought that was OKL4, as in "the OKL4 that Ralf-Philipp Weinmann
> hacked five years ago, allowing him to seize control of the whole
> phone via the baseband".  And from memory he actually exploited OKL4
> via a privesc, rather than going for the multi-megabytes of insecure
> gunk running on top of the kernel, which are even more exploitable.

I don't know a great deal about this specific topic, but my
understanding is that some run seL4. It would not surprise me if others
did not.

Perry