On 11 Dec 2014, at 2:34 , Marcus Völp voelp@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.abst...). 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.pm...).
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