[Cryptography] Security proofs prove non-failproof

[Peter Gutmann]

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.

Peter.