Hacker News Reader

Granted that details are not there yet (but from previous work done by the author one can guess), would a formally proven OS like seL4 have prevented this? seL4 is somewhat weak on HW support but the functionality required in the secure domain doesn't do much I/O anyway.

View on HN

FWIW, formal verification requires a complete and exact spec - the TZ kernel is very complex and interacts with nearly all the peripherals on the SoC, it doesn't just manage QSEE applications. I think creating a spec for something like that would be really hard.

The whole point of using seL4 is that you can use it to provide guaranteed isolation. If you were to use seL4 it would be so that you could write those drivers in user mode and so that a bug in one would not let you extract crypto keys in another.

Reply on news.ycombinator.com