Paper: undermine memory isolation in Fiasco OC covert channels

[Gernot Heiser]

> On 11 Dec 2014, at 2:34 , Marcus Völp <voelp at os.inf.tu-dresden.de> 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 (http://sel4.systems/) is specifically designed for strict isolation, and has a formal proof of confidentiality that rules out covert storage channels (see http://ssrg.nicta.com.au/publications/nictaabstracts/Murray_MBGBSLGK_13.abstract.pml). 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 (http://ssrg.nicta.com.au/publications/nictaabstracts/Cock_GMH_14.abstract.pml). 

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

Gernot