[Cryptography] Security proofs prove non-failproof

[Ben Laurie]

On 20 February 2017 at 20:40, Perry E. Metzger <perry at piermont.com> wrote:
> 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.

My understanding is that Peter is correct, and none of them run seL4.
Its a popular misconception.

OTOH, I think formal methods really are becoming useful.