I tried to read the article, and know what all the words mean (sel4, enclaves, virtualization primitives, etc.).
It all seems very complicated and error prone, but I couldn’t figure out what the attack model is, or what the security objectives are.
Eg, what sorts of things run in exclaves, and under what circumstances will a persistent kernel level compromise on my laptop protect those things?
I could imagine a passkey implementation with some extensions that allow securely presenting what the user is consenting to and how ("enter your payments PIN or password now to confirm a payment of $x to merchant y").
It's of course even better to do that in tamper-proof security coprocessors such as Apple's secure enclave, but TEEs have the big advantage of having access to much more memory and faster processing, which allows doing more complicated things there more easily.
They can also always lean on the secure hardware for actual key management, but handle more complex user interface operations in an environment that's still more secure than the main OS.
Android has supported something just like that years ago with "protected confirmation" [1], but unfortunately it's only available on Pixel phones and hasn't really been picked up by app developers as a result; the situation for Apple is of course very different, so I have some hopes that if they launch something comparable it could actually see some adoption.
[1] https://android-developers.googleblog.com/2018/10/android-pr...
Apple is already using the secure enclave for key derivation, PIN/password rate limiting etc. (that’s what it’s for), but my point is that there’s currently a gap in that you can often not really know if you are actually talking to the secure enclave or OS-level malware.
In order to do those things I have to actually steal his laptop. Which would be obvious to him. It also implicates me.
If I could just remotely install a driver I don't need to worry about any of that and I can steal remotely and anonymously.
(Though I’m not convinced that will actually work on modern apple devices, where the led is pixels that run through the compositor — I guess the video driver stack and window managers are also exclaves in this world?)
Once you have that, you can take the idea further: Displaying an indicator that confirms that all your keystrokes are going to an exclave validating your password, for example.
The much-hated touch bar actually enabled just that, for Apple Pay payments, as far as I remember: It could display something like "touch to confirm payment of $x" on its own screen in a way that was impossible to manipulate from macOS – now here's an opportunity to bring that level of security back without requiring a dedicated display or taking away people's beloved function keys.
I would expect that to mean they're not included in screenshots so I'm curious now whether that's true for the iPhone 16.