The assumptions the proof makes are pretty clearly listed: https://sel4.systems/Verification/assumptions.html

The one covering side channels is pretty honest:

Information side-channels: this assumption applies to the confidentiality proof only and is not present for functional correctness or integrity. The assumption is that the binary-level model of the hardware captures all relevant information channels. We know this not to be the case. This is not a problem for the validity of the confidentiality proof, but means that its conclusion (that secrets do not leak) holds only for the channels visible in the model. This is a standard situation in information flow proofs: they can never be absolute. As mentioned above, in practice the proof covers all in-kernel storage channels but does not cover timing channels.

So the proof won't be invalidated at it does not cover that particular threat.

Now the question is how useful the is a proof not covering side channels? I'd say pretty useful and it doesn't mean they don't have counter measures for to counter their exploitation, nor that they are not effective, just that a proof of efficiency is out of reach for now.

That's a bit unfair. Any side–channel attack that invalidates seL4 security guarantees —assuming the proofs are valid— also invalidates any other imaginable OS'.

We're in the philosophical territory of tasking infallible beings with stopping their own flawless creations.

I don't think a side channel attack against L4 would be particularly useful - the kernel's tiny, and doesn't really do much other than scheduling, IPC and capabilities. Anything you might want to learn lives in other processes.

That said, the big caveat of the whole thing, is that by pushing stuff traditionally considered to be sensitive to user space doesn't solve security or stability, it makes it other people's problem. There's no reason you couldn't do a side channel (or a different kind of) attack against a process that hosts the filesystem.

Side channel timing attacks are micro architectural. The SeL4 security proofs are architectural.

Although, there is ongoing research regarding time protection (https://trustworthy.systems/projects/timeprotection/) which prevents exactly timing channels. Including proofs of seL4 providing time protection.

Are timing (over network) attacks, physical access, etc. typically excluded from research like this for being “out of scope”, so to speak? I’m not familiar.

There's another can of worms that are rowhammer-esque attacks.

you are missing the point

just because something isn't perfect and handles everything you can come up with doesn't mean it isn't still very very useful

nothing in nature is truly perfect and down-talking grate but not perfect things will just make us stuck in a pretty shitty world which never improves because no improvement by itself "perfectly/fully" solves whatever problem set you are looking at