Paper: undermine memory isolation in Fiasco OC covert channels

Gernot Heiser gernot at
Wed Dec 10 22:01:45 CET 2014

> On 11 Dec 2014, at 2:34 , Marcus Völp <voelp at> wrote:
> On 12/10/2014 03:23 PM, teclis High Elf wrote:>
> These researchers from
> TU Berlin claim to be able to undermine memory
>> isolation in Fiasco OC through the use of covert channels. I'd be very
>> interested to hear the opinion of the Fiasco experts.
> the Fiasco OC interface (and probably most L4 versions) have not been
> designed for freedom of covert channels, nor has L4Re.

“Most L4 versions” is technically correct, but the implied “don’t bother looking at others” isn’t.

seL4 ( is specifically designed for strict isolation, and has a formal proof of confidentiality that rules out covert storage channels (see It is the only system around with such a proof about the actual implementation (as opposed to proving properties about a model of the system).

There’s also a fair bit of work on mechanisms for combatting timing channels is seL4 ( 

> Anyway, why would you want that for high security applications? If you
> plan to go for such a system, please have a look at the work around EROS
> by Jonathan Shapiro.

EROS doesn’t have such a proof either. And EROS seems to be quite dead, while seL4 is quite alive.

I’ll discuss details in a forthcoming blog, after reading the TUB paper in detail.


More information about the l4-hackers mailing list