zlacker

> there's no attack that will allow one seL4 process to write to the memory of another seL4 process it hasn't been granted write access to. Not for US$1B, not for US$1T, not for US$1000T.

Nitpick: for only about US$1M (give or take a order of magnitude or two depending on location), the process (assuming network access) can hire a assassin to kill you, pull up a shell on your computer, and give the process whatever priviledges it wants.

>>a13692+(OP)
Normally it wouldn't have network access, but that's an excellent point—generalized, once programs can start having physical-world effects that loop around to affect the computer they're running on, you can no longer make such adamantium-clad guarantees. And, as Rowhammer and various passive-emission attacks show, it's not uncommon in practice for the ordinary execution of the program to have such effects.

Still, this kind of thing isn't always applicable. If the seL4 kernel in question is on orbit, or running on a computer at an unknown location, or in a submarine, or in a drone in flight, the assassin can't in practice sit down at the console. And if it's running on something like the Secure Enclave chip in an iPhone, or a permissive action link, physical access may be impractically difficult regardless of who you kill.