Paper: undermine memory isolation in Fiasco OC covert channels
Hi, 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. (Could a system built on Fiasco be hardened against such an attack be adding access control for UDP ports)?? http://eprint.iacr.org/2014/984.pdf
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. 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: http://os.inf.tu-dresden.de/papers_ps/voelp_phd.pdf
(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. 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.
be adding access control for UDP ports)??
I don't see how access control for UDP Ports helps? Currently, we don't have funding for high security work, but please feel free to discuss your requirements and ideas on this list or more privately. Best regards Marcus Völp -- Dr.-Ing. Marcus Völp Technische Universität Dresden Computer Science, Institute for Systems Architecture Operating Systems 01062 Dresden, Germany Phone: +49 (351) 463-38350 Fax: +49 (351) 463-38284 E-Mail: voelp@os.inf.tu-dresden.de
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
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
Am 23.12.2014 um 06:22 schrieb Gernot Heiser:
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:
http://os.inf.tu-dresden.de/papers_ps/voelp_phd.pdf I believe your thesis talks about timing channels. The type system in Chapter 4 checks for the absense of storage channels and then converts out remaining timing leaks.
Marcus
participants (3)
-
Gernot Heiser -
Marcus Völp -
teclis High Elf