I have now read the TUB paper, and feel I have to correct a number of the statements Marcus has made in this regard.
On 11 Dec 2014, at 2:34 , Marcus Völp voelp@os.inf.tu-dresden.de wrote:
Hi,
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.
As I already pointed out, seL4 *has* been designed for isolation from the ground up, and has a formal non-interference proof (which applies to the binary, not just a model) that the kernel provides freedom from storage channels.
In my thesis in 2011, I already identified several timing channels in the mapping-tree interface and in act Michael Peter should know this work:
I believe your thesis talks about timing channels.
It is generally accepted in the research community that it is impossible to rule out timing channels completely. (Although seL4 has at least an analysis of some of the more obvious ones, including an evaluation of how they can be reduced, see http://ssrg.nicta.com.au/publications/nictaabstracts/Cock_GMH_14.abstract.pm....)
However, the TUB paper is about *storage* channels. These are in general easier to deal with, and the above mentioned proof shows that seL4 is free of them (see also http://ssrg.nicta.com.au/publications/nictaabstracts/Murray_MBGBSLGK_13.abst...). Arguing that Fiasco’s storage channels are an old hat because the presence of timing channels has been noted before is somewhat misleading.
(Could a system built on Fiasco be hardened against such an attack
Nevertheless, it should be possible to construct compartments in such a way that they do not allocate from the same quotas or share resources by mapping from within the compartments. The setup would be to partition the system directly on top of Sigma0 and to bootstrap one L4Re instance per compartment, not allowing for shared channels over which objects could be mapped. Fiasco OC offers the means to establish such channels and to confine the compartments, but it has no support (and never claimed to have) for covert-channel free cross compartment mappings.
I suspect Marcus had not read the TUB paper when he wrote this. The Berlin folks didn’t use cross-partition mappings (which would indeed be a nonsensical thing to do) or allocation from the same quota. Instead they showed that through specific sequences of memory allocation and de-allocation *within* one partition (quota), they could - mount denial-of-service attacks against other partitions - leak information to other partitions.
To my understanding, this is what the quotas are designed to prevent. The TUB paper shows that they fail to provide the isolation for which they were designed.
You can find more analysis on my blog (http://microkerneldude.wordpress.com/).
Gernot