L4 microkernels: The lessons from 20 years of research and deployment

Re:L4 microkernels: The lessons from 20 years of research an... by eternalban on Tuesday September 20, 2016 @12:26PM (#12540749)

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.)

[ Parent | on HN ]

Re:L4 microkernels: The lessons from 20 years of research an... by cmrx64 on Tuesday September 20, 2016 @12:50PM (#12540954)

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.

[ Parent | on HN ]

Re:L4 microkernels: The lessons from 20 years of research an... by eternalban on Tuesday September 20, 2016 @01:16PM (#12541153)

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.

[ Parent | on HN ]

Re:L4 microkernels: The lessons from 20 years of research an... by cmrx64 on Tuesday September 20, 2016 @01:50PM (#12541527)

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

[ Parent | on HN ]