3 ms·

But it does give you a proven isolation boundary. We've been arguing for software sandboxes for ages, but their impact has been lessened since our OSs fall pret

by Eridrus 10y ago

But it does give you a proven isolation boundary. We've been arguing for software sandboxes for ages, but their impact has been lessened since our OSs fall pretty readily to skilled adversaries. As a computing industry we've put our trust in VMs as another isolation boundary, but the regular advisories from Xen show that this isn't really as solid boundary as we would like.

eternalban 10y ago
Are selL4 capabilities transferable?
- cmrx64 10y ago
  Yes. See the manual or the tutorials.
  - eternalban 10y ago
    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.)
    - cmrx64 10y ago
      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.
      - eternalban 10y ago
        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.
        cmrx64 10y ago
        There are more papers coming out soon about eliminating covert channels at the design/kernel level!
tptacek 10y ago
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.

by Eridrus 10y ago

eternalban 10y ago

Are selL4 capabilities transferable?

cmrx64 10y ago
Yes. See the manual or the tutorials.
- eternalban 10y ago
  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.)
  - cmrx64 10y ago
    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.
    - eternalban 10y ago
      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.
      - cmrx64 10y ago
        There are more papers coming out soon about eliminating covert channels at the design/kernel level!

tptacek 10y ago

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.