Undermining Isolation through Covert Channels in the Fiasco.OC Microkernel

Michael Peter; Jan Nordholz; Matthias Petschick; Janis Danisevskis; Julian Vetter; Jean-Pierre Seifert

Paper 2014/984

Undermining Isolation through Covert Channels in the Fiasco.OC Microkernel

Michael Peter, Jan Nordholz, Matthias Petschick, Janis Danisevskis, Julian Vetter, and Jean-Pierre Seifert

Abstract

In the new age of cyberwars, system designers have come to recognize the merits of building critical systems on top of small kernels for their ability to provide strong isolation at system level. This is due to the fact that enforceable isolation is the prerequisite for any reasonable security policy. Towards this goal we examine some internals of Fiasco.OC, a microkernel of the prominent L4 family. Despite its recent success in certain highsecurity projects for governmental use, we prove that Fiasco.OC is not suited to ensure strict isolation between components meant to be separated. Unfortunately, in addition to the construction of system-wide denial of service attacks, our identified weaknesses of Fiasco.OC also allow covert channels across security perimeters with high bandwidth. We verified our results in a strong affirmative way through many practical experiments. Indeed, for all potential use cases of Fiasco.OC we implemented a full-fledged system on its respective archetypical hardware: Desktop server/workstation on AMD64 x86 CPU, Tablet on Intel Atom CPU, Smartphone on ARM Cortex A9 CPU. The measured peak channel capacities ranging from 13500 bits/s (Cortex-A9 device) to 30500 bits/s (desktop system) lay bare the feeble meaningfulness of Fiasco. OC’s isolation guarantee. This proves that Fiasco.OC cannot be used as a separation kernel within high-security areas.

Note: Minor editing.

Metadata

Available format(s): PDF
Category: Implementation
Publication info: Preprint. MINOR revision.
Keywords: Critical systems Separation Microkernel Covert Channel
Contact author(s): Jean-Pierre Seifert @ telekom de
History: 2014-12-10: revised; 2014-12-10: received; See all versions
Short URL: https://ia.cr/2014/984
License: CC BY

BibTeX

@misc{cryptoeprint:2014/984,
      author = {Michael Peter and Jan Nordholz and Matthias Petschick and Janis Danisevskis and Julian Vetter and Jean-Pierre Seifert},
      title = {Undermining Isolation through Covert Channels in the Fiasco.{OC} Microkernel},
      howpublished = {Cryptology {ePrint} Archive, Paper 2014/984},
      year = {2014},
      url = {https://eprint.iacr.org/2014/984}
}