First, it depends on how you use it. L4 is pretty close to a "libOS". You can built sandboxes on it, or you can build something more like a monolithic OS on it.

Second, in IoT devices, sandboxing is a lot less interesting, because there aren't that many use cases for sandboxed sensor inputs (you're not RFing or button-pushing whole PDF documents).

I like L4! A lot! But I would be very wary of an IoT device claiming to have inherited security from it.

Are selL4 capabilities transferable?

Yes. See the manual or the tutorials.

Plese correct any/my minunderstanding here: doesn't that imply that flaws in the capability holder can obviate the "isolation boundary" guarantees? (For example, if app x has capability to address a certain memory block and then hands that off to another application.)

That's not what isolation is meant here: if there is a connection between applications that allows cap transfer, they aren't isolated at the cap level. See www.nicta.com.au/pub?doc=7371 for more details, page 35 ("Authority Confinement and Integrity"). If there is any shared memory or potential for shared memory via the vspace caps, there can still be info flows (see page 38, "Confidentiality: Information-flow security").

The theorems are somewhat technical, but your intuition is correct.

Thanks.

Skimming that, I got that (a) PHigh -> PLow via overt channels will be degraded, and that (b) seL4 reduces the attack surface to "covert channels" only which seem to be confined to H/W "platform" concerns.

There are more papers coming out soon about eliminating covert channels at the design/kernel level!